Finding F*: FSTAR_HOME, PATH, etc...

[mtzguido]

Hi all,

with the soon-to-come new F* build and packaging (#3637) we no longer would have a real need for an FSTAR_HOME that points to the root of repo, which is traditionally roughly what most of our projects have been doing to find a working F*. I say roughly since some projects will also check the PATH, some will try to peek upwards into ../FStar to see if they are in an everest checkout, etc. I think this is a nice time to unify what we're doing here.

Given the somewhat-new --locate family of options in F*, an external project only needs to find a working fstar.exe and can then call it to find anything else that may be needed (like the OCaml library path, the standard library, etc). There is no need to hardcode or find anything else but fstar.exe; so the question is now how that should be done uniformly by all projects.

A: just PATH) There's one clear solution: do nothing and just put fstar.exe in the PATH (see comment by Gabriel here FStarLang/karamel#512 (comment)). I think this makes sense if we all agree to ditch FSTAR_HOME and FSTAR_EXE, but it would mean updating a chunk of Makefiles to remove these and make sure PATH is properly set.

B: FSTAR_EXE/FSTAR_HOME/PATH) In FStarLang/karamel#512 I proposed that Makefiles should try to read FSTAR_EXE from the environment and use that if set. If unset, and FSTAR_HOME is set, we use $FSTAR_HOME/bin/fstar.exe. If FSTAR_HOME is also unset, we check the path. My thinking was that I was just want to provide the executable, but FSTAR_HOME is used by most projects, and I don't necessarily want to remove it immediately (though we should, since it does not have a consistent meaning).

I've already done this for Steel here FStarLang/steel#186. The same locate_fstar.mk can be used by most projects.

--

(Note karamel does some finding of F* on its own too, and I think this logic should match exactly what the Makefiles do.)

Any thoughts..?

[mtzguido]

Similarly I wonder if we still want a generic makefile like the existing fstar.mk . I'm not sure many projects are using this one, though maybe we can take the newer mk/test.mk and make it fit for external use (and make sure to test it as such).

[mtzguido]

We are leaning towards dropping FSTAR_HOME immediately, and having FSTAR_EXE ?= fstar.exe in our Makefiles. This would default to the PATH, and allow overriding, while still being simple.

[mtzguido]

This will be the convention, FSTAR_HOME is no longer meaningful. See also this karamel PR FStarLang/karamel#516, karamel will stop looking at FSTAR_HOME in the environment.