No FSTAR_HOME #516
Merged
No FSTAR_HOME #516
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Karamel will just find fstar.exe in the PATH. If one wants to override this then `-fstar /path/to/fstar.exe` can be used. There is also no trying to peek into the an F* Git repo to get a commit hash, just looking at the output of `fstar.exe --version` instead.
mtzguido
force-pushed
the
no_fstar_home
branch
from
079d429 to
21ea5a0
Compare
11 tasks
msprotz
approved these changes
Jan 8, 2025
There was a problem hiding this comment.
Super happy about this change. @Nadrieril any thoughts on the nix changes?
mtzguido
added a commit
to mtzguido/merkle-tree
that referenced
this pull request
Jan 8, 2025
mtzguido
added a commit
to mtzguido/merkle-tree
that referenced
this pull request
Jan 8, 2025
|
Looks good to me |
Wait until the ocamlenv is actually needed. It seems to be only relevant for the 'pre' rule, which also does not seem to be required...
|
Guido and I talked extensively about this and I just did one last round of review, this is good for me |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
With this PR krml will no longer do anything fancy to find an "FSTAR_HOME" or the F* executable: it will use the PATH. It can be overriden with the new
-fstaroption though. The library can be located by just asking F*.All the makefiles set
FSTAR_EXE ?= fstar.exeand pass-fstar $(FSTAR_EXE)to krml, so one can set FSTAR_EXE instead of placing F* in the PATH. But this is a convention of the Makefiles.