Introduce Z3 version switching #2995
Merged
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
Useful to later display messages about it.
|
This needs a tweak to fstar-mode before merging, since it always passes the |
|
Merging this now. Emacs will still work as before, taking z3 from the PATH, but switching the version won't be possible until I post a fix to fstar-mode. |
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.
As proposed in this note #2974.
With this PR F* will now look explicitly for
z3-4.8.5in the PATH, and prefer that over justz3(in Windows, both would have.exesuffixes), but it will still default toz3if the former is not found. An option--z3versionis also introduced to be able to switch the version, even within a single file, and have F* run the correct executable. F* will verify that it is talking to the correct Z3 version via issuing a(get-info :version)to Z3 and reading the output, failing with an error on a mismatch (though it can be downgraded to a warning or ignored).This is part of the move to using a new Z3.
F* will also use the version to decide which options to pass to Z3 (as a prefix of the SMT2 file). This PR also includes the options needed for the current Z3 master (which will be
4.12.3), so F* is readily usable with master Z3 right now.However, we still require some changes to the image creation, documentation, everest script, etc. But this change should be self-contained and not break anything (I think).