add downloading z3 4.13.3 and 4.8.5 to the everest script #119
Conversation
…use fstarlang_binaries
everest
Outdated
| ln -sf $new_z3_folder z3 | ||
| ./get_fstar_z3.sh $z3_versions_dest | ||
| magenta "Automatically customize $EVEREST_ENV_DEST_FILE with the z3 path $z3_versions_dest? [Yn]" | ||
| prompt_yes "write_z3_env_dest_file $z3versions_dest" true |
There was a problem hiding this comment.
Typo here? z3versions_dest -> z3_versions_dest
|
If we have a copy of |
|
Agree, but I'll merge this to fix the build for now, since Pulse already requires 4.13.3. |
| if [ -f "$destination_file_name" ]; then | ||
| echo ">>> Z3 $z3_ver already downloaded to $destination_file_name" | ||
| elif [ -z "$url" ]; then | ||
| echo ">>> Z3 $z3_ver not available for this architecture, skipping..." |
There was a problem hiding this comment.
On Apple Silicon, this declines to install 4.8.5. However, 4.8.5 can run on OSX, via its x64 emulation facilities (a.k.a. Rosetta 2). This is actually required for HACL* and other projects which have not yet upgraded to the latest z3.
I would suggest special-casing 4.8.5 / aarch64 to download the x64 version, and printing out a notice that Rosetta 2 ought to be installed on this machine.
A few more remarks:
- you'll probably have a better time using [[ for you tests, since this is lexed and parsed by bash itself, meaning it can deal with variables that expand to empty, rather than [, which has to obey command-line argument parsing as if it were calling the actual /usr/bin/[, and therefore will yield unexpected errors if owing to any circumstances some of your variables are actually empty
- you could use the
localkeyword in a few of your functions for local variables - your script requires bash >= 4 (associative arrays) but does not check for it -- this is pertinent for OSX, which ships bash 3 (the last GPLv2 version), but not bash 4; note that for now this is probably fine since this is only ever called via the everest script, which does run proper checks.
There was a problem hiding this comment.
Thanks! See FStarLang/FStar#3645
There was a problem hiding this comment.
you'll probably have a better time using [[ for you tests, since this is lexed and parsed by bash itself, meaning it can deal with variables that expand to empty, rather than [, which has to obey command-line argument parsing as if it were calling the actual /usr/bin/[, and therefore will yield unexpected errors if owing to any circumstances some of your variables are actually empty
[ works just fine with empty variables. You need to quote variables, but you should always quote them anyhow.
your script requires bash >= 4 (associative arrays) but does not check for it -- this is pertinent for OSX, which ships bash 3
I didn't test it at all on macos, thanks for serving as the guinea pig! FStarLang/FStar#3646 (I see Guido beat me to it.)
Preparing for F* upgrading to z3-4.13.3 in FStarLang/FStar#3631
This PR copies FStar/bin/get_fstar_z3.sh, which downloads the right versions of Z3 for each platform
And updates the everest script to call get_fstar_z3.sh instead of relying on FStarLang/binaries