Now, with this PR, make -C opt will automatically build opam package dependencies under opt/opam , unless EVERPARSE_USE_OPAMROOT is set, in which case the user's existing opam setup instead.

Now the remaining next step: what should be the default behavior of make?

@mtzguido, you were advocating the fact that make should not fail by default, unless there is a ./configure script. Currently, even with this PR make fails by default.

One could argue that, with this PR, make -C opt will play some role of a "coarse-grained" configure script. This may be enough for most EverParse users: to compile EverParse, they would only need to do make opt && make . In that case, we could merge this PR as is.

Another possibility could be to have make automatically invoke make -C opt. In that case, everything about the user's configuration would be ignored, except EVERPARSE_USE_OPAMROOT.

I say coarse-grained, because the only configurable bit here is for the user to set EVERPARSE_USE_OPAMROOT to use their own opam configuration instead of opt/opam. If a user wants to use their own F*, Karamel, or Pulse, even just one of them, then they need to set all environment variables by hand and they cannot use make -C opt at all. (In that case, make should not automatically call make -C opt.)

Then, do you think we need to adapt opt/Makefile so as to automatically recognize if the user has set FSTAR_HOME, etc., and compile only those components for which the user has not set the corresponding environment variable? Or, do you believe this should be done through a ./configure script instead, if at all?

Here's my (opinionated) 2 cents, some of which we discussed today:

If everparse has local copies of F*/karamel/pulse (via submodules, hashes, or whatever), then it should just use them, and not look into the user's environment at all (e.g. reading *_HOME variables, or trying to use an F* from the PATH). I routinely have to tweak things since everparse tries to call $FSTAR_EXE (which I have unset), or because it read my KRML_HOME instead of using the one in opt/.

I think the default should be to just use the dependencies in opt, including for CI purposes. This way, there is no leeway in what is being checked: we check that everparse builds and passes the tests with the checked-in snapshots (submodules/hashes) of the projects. This also means that changes in F*/krml/pulse will not break the everparse master branch, as there is no implicit requirement of being up-to-date.

Of course, we want to be up-to-date anyway, so a nightly job could try to advance the submodules, test the build, and commit this new state if everything passes.

If a user wants to use a local F*/krml/Pulse, this should be a very explicit step to deviate from the norm. Maybe running make use-local or similar would 1) write a config file with pointers to the system F*/krml/pulse, 2) disable the automatic building of opt/. One can also add a top-level fstar.sh script to either call the F* in opt, or the system one according to this setting, and use this script as the fstar_exe in the VS Code configs, to make this work nicely in the IDE too.

This is what I do for Kuiper (except for allowing using external dependencies, I haven't seen a need for this yet) and it's been working nicely.

Thanks Guido!

I agree with you that having precise submodules in opt/ and using them by default, with a non-trivial opt-out, offers the best reusability guarantee. But as you mention, it comes at the cost of regularly updating the submodules. This is why I propose a compromise: to have such submodules in releases (where reusability and reproducibility are a must), and to automatically clone the latest main branches of F*, Pulse, etc. on the main EverParse branch. Yes, I agree with you that there is a risk that a user tries to build EverParse at a time when it does not work with the main F* branch, etc. but I believe that it is the reponsibility of the EverParse developers to ensure that EverParse master always works with the latest F* (either with a nightly EverParse build, or with F*'s check-world), to avoid the converse risk of falling behind with an old submodule no longer updated.

Regarding the environment variables: I agree that one shouldn't automatically rely on PATH for F* or Karamel, because PATH is often silently set up in the user's back, especially if the user installs F* via opam. (For z3, I am less worried, since we look for a specific version in the Z3 executable name anyway.) However, if the user uses specific environment variables, such as FSTAR_EXE, KRML_HOME, etc., the user will have set up these variables themselves: there is no automatic installation that would have set up any of these variables behind the user's back. This is why I believe that there is no need for an extra step to configure EverParse when any of those variables are set, and that these variables should supersede opt/ if set.

I implemented my proposals above in #232 , which subsumes this PR. Thanks again!