New auto-configurable Makefile and release system #232

tahina-pro · 2025-09-12T18:43:51Z

TL;DR: This PR:

updates the Makefile to build EverParse together with all of its dependencies automatically, with support for customization via environment variables
creates a new push-button release system to push native Windows, MacOS and Linux binary packages into GitHub releases and a Docker image into GitHub Packages
updates the documentation accordingly

This PR subsumes #227

New Makefile

With this PR, a user just needs to type make and everything will be built: opam packages, F*, Karamel, Pulse, with Z3 automatically downloaded, and all paths set up. Under the hood:

The Makefile ~~downloads the Everest project into opt/everest (unless already present),~~ initializes an opam root in opt/opam with OCaml 5.3.0, and ~~calls opt/everest/everest opam~~ collects the opam package definitions of F*, Karamel and Pulse to install the opam package dependencies. (This ~~comes~~ inspires from Use a standalone opam root, fuse opam package build into make -C opt #227)
The user can supersede this whole step with their own opam installation (or OPAMROOT) by setting EVERPARSE_USE_OPAMROOT=1. Then, it becomes the user's responsibility to install the opam packages.
Then, the Makefile creates and includes opam-env.Makefile to properly set up the environment variables to OCaml and opam (including OCAMLPATH, PATH, etc.)
If ~~FSTAR_EXE is not set~~ EVERPARSE_USE_FSTAR_EXE is not set to 1, then the Makefile downloads F* into opt/FStar (unless already present), compiles it and sets FSTAR_EXE to opt/FStar/out/bin/fstar.exe
If the user sets ~~FSTAR_EXE~~ EVERPARSE_USE_FSTAR_EXE=1, then EVERPARSE_USE_OPAMROOT=1 is automatically set because EverCDDL has a plugin that needs to be compiled with the very same OCaml setup as the one compiling F*. (Thus, users can no longer use F* binary packages to build EverParse.)
If the user sets EVERPARSE_USE_FSTAR_EXE=1 without setting FSTAR_EXE, then FSTAR_EXE=fstar.exe by default (relying on PATH)
If ~~KRML_HOME is not set~~ EVERPARSE_USE_KRML_HOME is not set to 1, then the Makefile downloads Karamel into opt/karamel (unless already present), compiles it and sets KRML_HOME to opt/karamel
If the user sets ~~KRML_HOME, then FSTAR_EXE is required~~ EVERPARSE_USE_KRML_HOME=1, then automatically EVERPARSE_USE_FSTAR_EXE=1, because the .checked files in Karamel must match the user's F* install, and EverParse is not going to recheck Karamel in that case.
If ~~PULSE_HOME is not set~~ EVERPARSE_USE_PULSE_HOME is not set to 1, then the Makefile downloads Pulse into opt/pulse (unless already present), compiles it and sets PULSE_HOME to opt/pulse/out
If the user sets ~~PULSE_HOME, then FSTAR_EXE is required~~ EVERPARSE_USE_PULSE_HOME=1, then automatically EVERPARSE_USE_FSTAR_EXE=1, because the .checked files in Pulse must match the user's F* install, and EverParse is not going to recheck Pulse in that case.
If Z3 4.13.3 cannot be found via fstar.exe --locate_z3, or in the PATH, or in opt/z3, then the Makefile downloads it into opt/z3 and updates the PATH accordingly.
This step is skipped if ADMIT=1 is provided (which automatically appends --admit_smt_queries true to OTHERFLAGS.)
Then, the Makefile creates and includes the global .depend F* dependency file as done currently. This dependency file itself depends on F*, Karamel and Pulse as determined with internal NEED_OPAM, NEED_FSTAR, NEED_KRML, NEED_PULSE and NEED_Z3 variables automatically computed from the presence or absence of the corresponding user environment variables at the beginning of the Makefile.
Then, the rest of the build happens as before, since all auxiliary Makefiles have been included at this point.

Steps 1 to 6 can be reproduced with make deps.

The only dependencies not automatically built are Rust and system packages that need to be installed as root. For transparency reasons, we describe them explicitly in the README.md, rather than letting opam depext automatically install them behind the user's back (also because there is no way for opam to ask for confirmation for opam depext but not for the rest of opam install, since we want to skip any user interaction when setting up anything in opt/)

Then, the user can automatically set up their Bash environment with eval "$(make -s env)" . This will set up the OCaml and opam environments, FSTAR_EXE, KRML_HOME, PULSE_HOME, EVERPARSE_HOME and PATH accordingly. For users' convenience, we provide a Bash wrapper script, ./shell.sh, to open a Bash shell (or run a command) with the environment set up accordingly.

New release system

This PR defines .github/workflows/release.yml so that we just need to push a single button to provide the whole release automatically. This workflow now only uses GitHub-hosted runners, including on Windows. Example runs can be found at https://github.com/tahina-pro/quackyducky/actions/runs/17664901098 (that run has not been fully configured with Visual Studio Code yet, however) and https://github.com/tahina-pro/quackyducky/actions/runs/17686176690 (fully configured with Visual Studio Code, but with a custom version number that I set by hand at tahina-pro/quackyducky@32bbc76 and that I reverted by hand at tahina-pro/quackyducky@312d0bc)

User inputs:

The name of the EverParse release branch (by default _release).
The repository and branch for F*

Then, when hitting the "release" button from a branch (called the "running branch" hereafter):

The GitHub workflow creates a F* source package on a Ubuntu runner. (This is necessary because F* cannot be built as is on Windows.)
Then, from the running branch, the GitHub workflow creates a release-specific branch, _dzomo_release_NNNN where NNNN is the run ID (the number following actions/runs in the run URL.) This branch merges the release branch, commits the contents of the F* source package, and ~~creates submodules for Karamel, Pulse, Everest and opam-repository (which allows~~ uses opam lock to freeze the versions of the opam packages used to build everything ) into opt/. Then this branch creates a version number of the form vYYYY.MM.DD and writes it into version.txt . Please note that the hashes of F* (from which the GitHub workflow creates a source package), Karamel and Pulse are already assumed to be recorded in the running branch, usually via the nightly.yml workflow (or make -C opt advance).
The user can produce a specific version.txt or specific copies of ~~Everest~~, Karamel, etc. into opt/ on the running branch before starting the workflow. In that case, the workflow will use those instead, but then the user needs to manually remove those copies from the release branch at the end of the release process, otherwise future releases will fail.
Then, from the release-specific branch, the GitHub workflow builds and tests MacOS, Windows and Linux binary packages, using version.txt for the version number. We also perform interoperability tests between binary packages to check that the hashes produced by 3D on one platform can be checked with --check_hashes on another platform. Binary packages are pushed as run artifacts.
In parallel with 3, the GitHub workflow builds a linux/amd64 Docker image containing a Visual Studio Code Server with the F* VSCode Assistant (from a04d4dd, thanks @gebner !), and pushes it into GitHub packages as ghcr.io/project-everest/everparse:_dzomo_release_NNNN. Then, a full make test is run in a container based on that image.
Once all tests succeed, the GitHub workflow pushes a new tag, vYYYY.MM.DD, corresponding to the version number in version.txt
Then, the GitHub workflow downloads the binary packages created as run artifacts, pushes them into a new GitHub release associated with that tag, and deletes the artifacts.
Then, from the release branch, the GitHub workflow merges the running branch, and then merges the release-specific branch, and then reverts that merge. At this point, the release branch and the running branch should have the same contents. This allows all release tags to be in a single ancestry lineage; thus, the message produced when creating the GitHub release can reference the immediately previous release in that lineage.
In parallel with 6 and 7, the GitHub workflow pushes a new Docker image tagged with that tag, based on the :dzomo_release_NNNN image, the only difference being that the Git clone within the Docker image is now tagged with the version tag as well.
Then, the GitHub workflow removes the release-specific branch.

Caveats:

Pulse fails to build on Windows, so EverCDDL is excluded from Windows builds.
I don't know how to refer to the OpenSSL headers on MacOS or Windows, so EverCOSign is excluded from MacOS and Windows builds. (For Windows, I think we should use SymCrypt instead of OpenSSL anyway, and I don't know how to do that either.)

Documentation

This PR updates the README.md with all build instructions.

Since dependency build has become much easier for the user, this PR removes the whole "build" chapter from the manual.

This PR also updates the Visual Studio Code configuration files: now, the user is assumed to call Visual Studio Code from a shell suitably configured with ./shell.sh

…ate environment

…aramana_standalone_opam

…ygwin already)

…aramana_new_release

mtzguido · 2025-09-23T17:27:32Z

Trying a build overriding F*/krml and using my own OPAM root. make clean tries to build pulse:

$ make clean
rm -rf opam-env.Makefile.tmp
/home/guido/r/everparse/main/opt/opam-env.sh > opam-env.Makefile.tmp
echo >> opam-env.Makefile.tmp
echo env: opam-env >> opam-env.Makefile.tmp
echo .PHONY: opam-env >> opam-env.Makefile.tmp
echo opam-env: >> opam-env.Makefile.tmp
echo "  \"/home/guido/r/everparse/main/opt\"/opam-env.sh --shell" >> opam-env.Makefile.tmp
mv opam-env.Makefile.tmp opam-env.Makefile
touch opam-env.Makefile
make -C /home/guido/r/everparse/main/opt/pulse/ ADMIT=1
   DEPEND          /home/guido/r/everparse/main/opt/pulse/src/checker
   CHECK           Pulse.Config.fsti
   CHECK           Pulse.Config.fst
   EXTRACT         Pulse.Config.fst.checked

I also noticed some errors like these:

* Error 241 at /home/guido/r/everparse/main/opt/pulse/out/lib/pulse/lib/PulseCore.FractionalPermission.fst(0,0-0,0):
  - Unable to load
    /home/guido/r/everparse/main/opt/pulse/out/lib/pulse/lib/PulseCore.FractionalPermission.fst.checked
    since checked file
    /home/guido/r/everparse/main/opt/pulse/out/lib/pulse/lib/PulseCore.FractionalPermission.fst.checked
    is stale (dependence hash mismatch, use --debug CheckedFiles for more
    details); will recheck
    /home/guido/r/everparse/main/opt/pulse/out/lib/pulse/lib/PulseCore.FractionalPermission.fst
    (suppressing this warning for further modules)

* Error 317:
  - Expected
    /home/guido/r/everparse/main/opt/pulse/out/lib/pulse/lib/PulseCore.FractionalPermission.fst
    to already be checked.

due to stray files in opt/pulse from older builds, fixed it by running git clean in opt/pulse. Maybe the Makefile should run clean inside this directory when the F* we are using changes?

mtzguido

Other than my comment above, looks good to me. I tested it in a couple of different ways.

tahina-pro · 2025-09-23T18:42:39Z

Yes, I completely overlooked make clean. Thanks a lot Guido for the heads up!

make clean would clean EverParse but not its dependencies; I should add a make distclean rule that would. Then, for that rule, make should not try to rebuild included Makefiles, but I don't know how to do that.

tahina-pro · 2025-09-23T19:00:03Z

Maybe the Makefile should run clean inside this directory when the F* we are using changes?

Yes, there can be a problem if a user switches between two different F* while keeping the same Pulse (or Karamel): Pulse's .depend files are not updated. There is no obvious way to fix that without cleaning the Pulse directory, because making Pulse's .depend file depend on the F* executable would not work if the user switches to an F* with an older timestamp.

gebner · 2025-09-23T22:24:49Z

Does vscode work for anyone? I'm getting errors like this:

fstar lax stderr: * Warning 152:
  - Not a valid include directory: ./lib/evercddl/plugin

* Warning 152:
  - Not a valid include directory: ./lib/evercddl/lib


fstar lax stderr: * Error 64:
  - Could not find evercddl_lib.cmxs to load

1 error was reported (see above)

fstar stderr: * Warning 152:
  - Not a valid include directory: ./lib/evercddl/plugin

* Warning 152:
  - Not a valid include directory: ./lib/evercddl/lib


fstar stderr: * Error 64:
  - Could not find evercddl_lib.cmxs to load

1 error was reported (see above)

gebner · 2025-09-23T22:38:22Z

Ah, vscode works now after everything has finished building.

gebner · 2025-09-23T23:38:32Z

I haven't been able to figure out how to disable the built-in opam root. It always runs opam init.
export EVERPARSE_USE_{OPAMROOT,FSTAR_EXE,KRML_HOME,PULSE_HOME}=1 is quite a few environment variables. (And it took me a few tries to figure out if I need to set it to 0 or 1.) Could we trim that down to export EVERPARSE_USE_OPT=0?

with that, `make test && make distclean` yields a clean state

tahina-pro · 2025-09-24T05:08:14Z

I haven't been able to figure out how to disable the built-in opam root. It always runs opam init.

Even with EVERPARSE_USE_OPAMROOT=1 ?

export EVERPARSE_USE_{OPAMROOT,FSTAR_EXE,KRML_HOME,PULSE_HOME}=1 is quite a few environment variables. (And it took me a few tries to figure out if I need to set it to 0 or 1.) Could we trim that down to export EVERPARSE_USE_OPT=0?

If needed, I can add such a shortcut that will set all such variables to 1.

mtzguido · 2025-09-24T05:10:48Z

Even with EVERPARSE_USE_OPAMROOT=1 ?

This did work for me FWIW. (And I think the shortcut would be nice too!)

tahina-pro · 2025-09-24T05:12:04Z

Thanks to Guido's comments, I fixed the make clean rule, and I added a make distclean rule:

make clean cleans up all of EverParse-only build products
make distclean cleans up all of EverParse build products and removes everything in opt (opam, F*, Karamel, etc.) I tested and I can confirm that make distclean yields a fully clean state, even after make test. I haven't dared to add a CI test for that, though.

tahina-pro · 2025-09-24T16:38:24Z

From your unanimous requests, I added a shortcut, EVERPARSE_USE_MY_DEPS=1, which turns all customization environment variables to 1.

gebner · 2025-09-24T23:33:02Z

I'm running into a new error now:

$ make ADMIT=1
[...]
/home/gebner.linux/everparse/opt/FStar/out/bin/fstar.exe  --z3version 4.13.3  --admit_smt_queries true --include /home/gebner.linux/everparse/opt/karamel/krmllib --include /home/gebner.linux/everparse/opt/karamel/krmllib/obj --include /home/gebner.linux/everparse/opt/pulse/out/lib/pulse --include src/lowparse --include src/ASN1 --include src/3d/prelude --include src/cbor/spec --include src/cbor/spec/raw --include src/cbor/spec/raw/everparse --include src/cddl/spec --include src/lowparse/pulse --include src/cbor/pulse --include src/cbor/pulse/raw --include src/cbor/pulse/raw/everparse --include src/cddl/pulse --include src/cddl/tool --include . --cache_checked_modules --warn_error @241 --already_cached PulseCore,Pulse,C,LowStar,*,-LowParse,-EverParse3d,-ASN1,-CBOR,-CDDL,Prims,FStar,LowStar --cmi --ext context_pruning  --dep full @.depend.rsp --output_deps_to .depend.aux
* Warning 152:
  - Not a valid include directory:
      /home/gebner.linux/everparse/opt/karamel/krmllib/obj

* Warning 274:
  - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c'
    in file "/home/gebner.linux/everparse/opt/karamel/krmllib/C.fst".
  - Rename
    "/home/gebner.linux/everparse/opt/karamel/krmllib/C.fst"
    to avoid conflicts.

* Error 317:
  - Expected C.Loops to be already checked but could not find it.

1 error was reported (see above)

gebner · 2025-09-24T23:35:28Z

Ah, that's because karamel fails to build the first time. But after retrying everparse believes karamel has already been built!

❯ make -j4 ADMIT=1
eval "$(opam env --root="/home/gebner.linux/everparse/opt/opam" --set-root)" && env OTHERFLAGS='--admit_smt_queries true' make -C /home/gebner.linux/everparse/opt/karamel/
make[1]: Entering directory '/home/gebner.linux/everparse/opt/karamel'
dune build
ln -sf _build/default/src/Karamel.exe krml
make -C krmllib
make[2]: Entering directory '/home/gebner.linux/everparse/opt/karamel/krmllib'
which: no time in (/home/gebner.linux/everparse/opt/opam/5.3.0/bin:./:/home/gebner.linux/.opam/5.3.0/bin:/home/gebner.linux/fstar/bin:/home/gebner.linux/.local/sbin:/home/gebner.linux/.local/bin:/home/gebner.linux/.cargo/bin:/home/gebner.linux/.cabal/bin:/usr/local/bin:/usr/bin:/home/gebner/.pulumi/bin)
../Makefile.common:12: *** 'time' not found, try apt-get install time.  Stop.
make[2]: Leaving directory '/home/gebner.linux/everparse/opt/karamel/krmllib'
make[1]: *** [Makefile:31: krmllib] Error 2
make[1]: Leaving directory '/home/gebner.linux/everparse/opt/karamel'
/home/gebner.linux/everparse/src/common.Makefile:94: .depend: No such file or directory
make: *** [deps.Makefile:156: /home/gebner.linux/everparse/opt/karamel/_build/default/src/Karamel.exe] Error 2

…est)

tahina-pro · 2025-09-25T18:09:56Z

This is because I am not tracking the right witness to declare Karamel correctly built. Let me fix that. Thanks Gabriel!

tahina-pro and others added 30 commits August 23, 2025 00:32

install opam packages within make -C opt and local opam root, autom…

643dc6e

…ate environment

use separate Makefile to clone opt/ subdirs

e610968

remove useless opam exec

f126985

OPAMNODEPEXTS should be left for the user to choose

aa9838d

git.Dockerfile: allow specifying branch, recurse submodules

af0d531

CI: enable submodules on checkout

a806a6e

make env: fix opam env with --set-root

0469135

opam-env.sh: make PATH update compositional

15d875b

Makefile: re-enable PulseParse tests

9a43e35

Dockerfiles: build 3 stages, deps, all and test

3c6554c

add one more base stage

8e96a90

git.Dockerfile: fix use of CI_BRANCH

f776cfe

Merge branch 'master' of github.com:project-everest/everparse into _t…

6bd5b4b

…aramana_standalone_opam

Some fixes to prevent using external OCamls

28c6bf7

do not download opam packages if OPAMROOT is set

039b528

use a separate EVERPARSE_USE_OPAMROOT variable instead

f16a54d

backport Dockerfiles from ccs2025

e6c485b

fix opam environment

4c8a9f5

remove redundant opam env

b7f8f2f

eval $(make -s env) => eval "$(make -s env)"

84d6aa0

integrate dependency build with make, with customization knobs

5bc7201

remove package build commands in favor of Makefile rules

3165272

move a definition from CDDL.Spec.MapGroup.fsti to .fst

3e092dc

rlimit

62a4774

update Windows setup

17bafa9

opam init: use local Cygwin install (since we assume running within C…

a7b4696

…ygwin already)

cannot directly exec Bash scripts on Windows

7ba4a5e

do not explicitly specify CC

73121ab

build F* source package on Linux

fd6e396

(TEMP) enable CI

46b658e

tahina-pro added 2 commits September 19, 2025 23:58

install cygwin packages from a local list

57510ab

install opam packages from fstar.opam, karamel.opam, pulse.opam

02cb04b

tahina-pro force-pushed the _taramana_new_release branch from cbd3fd2 to 02cb04b Compare September 20, 2025 06:12

tahina-pro added 2 commits September 22, 2025 14:52

Merge branch 'master' of github.com:project-everest/everparse into _t…

a1cfb70

…aramana_new_release

narrow down Cygwin package list

90be734

mtzguido approved these changes Sep 23, 2025

View reviewed changes

tahina-pro added 2 commits September 24, 2025 03:32

3d doc: move static assertions from out/ to 3d-snapshot/

463be45

tidy up make clean (thanks @mtzguido)

4fd0d1c

with that, `make test && make distclean` yields a clean state

tahina-pro added 4 commits September 24, 2025 15:16

add a shortcut environment variable, EVERPARSE_USE_MY_DEPS=1

6d5e68b

run make clean in F* for releases

8d0cb68

advance hashes

6301ecb

rlimit

0a1a330

Cygwin packages: add zip, unzip for make package

9a7d55f

replace CI task with build-ubuntu (with current hashes instead of lat…

84eb8dd

…est)

use *.done witness files instead of select files in each dep

1b8a4d4

tahina-pro merged commit 7e3e00d into master Sep 25, 2025
13 checks passed

tahina-pro deleted the _taramana_new_release branch September 25, 2025 21:35

New auto-configurable Makefile and release system #232

New auto-configurable Makefile and release system #232

Uh oh!

Conversation

tahina-pro commented Sep 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

New Makefile

New release system

Documentation

Uh oh!

mtzguido commented Sep 23, 2025

Uh oh!

mtzguido left a comment

Choose a reason for hiding this comment

Uh oh!

tahina-pro commented Sep 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tahina-pro commented Sep 23, 2025

Uh oh!

gebner commented Sep 23, 2025

Uh oh!

gebner commented Sep 23, 2025

Uh oh!

gebner commented Sep 23, 2025

Uh oh!

tahina-pro commented Sep 24, 2025

Uh oh!

mtzguido commented Sep 24, 2025

Uh oh!

tahina-pro commented Sep 24, 2025

Uh oh!

tahina-pro commented Sep 24, 2025

Uh oh!

gebner commented Sep 24, 2025

Uh oh!

gebner commented Sep 24, 2025

Uh oh!

tahina-pro commented Sep 25, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tahina-pro commented Sep 12, 2025 •

edited

Loading

tahina-pro commented Sep 23, 2025 •

edited

Loading