Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add downloading z3 4.13.3 and 4.8.5 to the everest script #119

Merged
merged 3 commits into from
Dec 13, 2024
Merged

add downloading z3 4.13.3 and 4.8.5 to the everest script #119

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8f447f6
add downloading z3 4.13.3 and 4.8.5 to the everest script; no longer …
nikswamy Dec 13, 2024
740b821
typo
nikswamy Dec 13, 2024
68b31d6
Update get_fstar_z3.sh
gebner Dec 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 19 additions & 44 deletions everest
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ windows_check_or_modify_env_dest_file () {
write_z3_env_dest_file () {
str="
# This line automatically added by $0
export PATH=$(pwd)/$1/bin:\$PATH"
export PATH=$(pwd)/$1:\$PATH"
write_to_env_dest_file "$str"
}

Expand Down Expand Up @@ -259,14 +259,15 @@ try_git_clone () {
}

parse_z3_version () {
if ! which z3 >/dev/null 2>&1; then
z3_exec_name=$1
if ! which $z3_exec_name >/dev/null 2>&1; then
echo "no z3 in path!"
else
local z3_version=$(z3 --version)
local z3_version=$("$z3_exec_name" --version)
if echo $z3_version | grep hashcode >/dev/null 2>&1; then
z3 --version | $SED 's/.*build hashcode \(.*\)/\1/' | tr -d '\r'
$z3_exec_name --version | $SED 's/.*build hashcode \(.*\)/\1/' | tr -d '\r'
else
z3 --version | $SED 's/Z3 version \([0-9\.]\+\).*/\1/'
$z3_exec_name --version | $SED 's/Z3 version \([0-9\.]\+\).*/\1/'
fi
fi
}
Expand All @@ -276,50 +277,24 @@ parse_z3_version () {
# ------------------------------------------------------------------------------

do_update_z3 () {
# Update our clone of FStarLang/binaries and check that we have the blessed z3
# version
if ! [[ -d fstarlang_binaries ]]; then
echo "... cloning FStarLang/binaries"
try_git_clone "[email protected]:FStarLang/binaries.git" "https://github.com/FStarLang/binaries.git" fstarlang_binaries
fi
(cd fstarlang_binaries && git fetch && git checkout z3-4.8.5 && git reset --hard origin/z3-4.8.5)
# Check that we have z3-4.13.3 and z3-4.8.5 in the path
# Otherwise, run get_fstar_z3.sh to download them both from github.com/z3prover/z3
# and add them to the path

local current_z3=$(parse_z3_version)
echo "... version of z3 found in PATH: $current_z3"
local current_z3_4_13_3=$(parse_z3_version "z3-4.13.3")
local current_z3_4_8_5=$(parse_z3_version "z3-4.8.5")

if is_windows; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-win.zip
elif is_osx; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-osx-*.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Ubuntu" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-ubuntu-14.04.zip
elif [[ $(lsb_release -i | awk '{ print $3; }') == "Debian" ]]; then
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
if [[ $current_z3_4_13_3 == "4.13.3" && $current_z3_4_8_5 == "4.8.5" ]]; then
echo "Found z3-4.13.3 and z3-4.8.5 in PATH; nothing to do"
else
red "WARNING: could not figure out your system via lsb_release; defaulting to Debian"
local new_z3_file=fstarlang_binaries/z3-tested/z3-4.8.5*-x64-debian-*.zip
fi
local new_z3=4.8.5
new_z3_file=$(ls $new_z3_file)
echo "... version of z3 found in z3-tested is: $new_z3_file"

if [[ $new_z3 != $current_z3 ]]; then
magenta "Get the freshest z3 from FStarLang/binaries? [Yn]"
local z3_versions_dest="z3-versions"
magenta "Download z3 4.13.3 and 4.8.5 to $z3_versions_dest? [Yn]"
prompt_yes true "exit 1"
echo "... ls fstarlang_binaries/z3-tested"
ls -altrh fstarlang_binaries/z3-tested
echo "... ls $new_z3_file"
ls -altrh $new_z3_file
echo "... unzipping $new_z3_file"
unzip $new_z3_file
local new_z3_folder=${new_z3_file%%.zip}
new_z3_folder=${new_z3_folder##fstarlang_binaries/z3-tested/}
find $new_z3_folder -iname '*.dll' -or -iname '*.exe' | xargs chmod a+x
magenta "Automatically customize $EVEREST_ENV_DEST_FILE with the z3 path? [Yn]"
prompt_yes "write_z3_env_dest_file $new_z3_folder" true
rm -f z3
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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Typo here? z3versions_dest -> z3_versions_dest

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thanks!

fi

}

do_check ()
Expand Down
78 changes: 78 additions & 0 deletions get_fstar_z3.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
#!/usr/bin/env bash
set -euo pipefail

kernel="$(uname -s)"
case "$kernel" in
CYGWIN*) kernel=Windows ;;
esac

arch="$(uname -m)"
case "$arch" in
arm64) arch=aarch64 ;;
esac

declare -A release_url
release_url["Linux-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip"
release_url["Darwin-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip"
release_url["Windows-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
release_url["Linux-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip"
release_url["Linux-aarch64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-glibc-2.34.zip"
release_url["Darwin-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-osx-13.7.zip"
release_url["Darwin-aarch64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-osx-13.7.zip"
release_url["Windows-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"

trap "exit 1" HUP INT PIPE QUIT TERM
cleanup() {
if [ -n "${tmp_dir:-}" ]; then
rm -rf "$tmp_dir"
fi
}
trap "cleanup" EXIT

download_z3() {
url="$1"
version="$2"
destination_file_name="$3"

if [ -z "${tmp_dir:-}" ]; then
tmp_dir="$(mktemp -d --tmpdir get_fstar_z3.XXXXXXX)"
fi

echo ">>> Downloading Z3 $version from $url ..."
base_name="$(basename "$url")"

z3_path="${base_name%.zip}/bin/z3"
if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi

pushd "$tmp_dir"
curl -L "$url" -o "$base_name"
unzip "$base_name" "$z3_path"
popd

install -m0755 "$tmp_dir/$z3_path" "$destination_file_name"
echo ">>> Installed Z3 $version to $destination_file_name"
}

dest_dir="$1"
if [ -z "$dest_dir" ]; then
echo "Usage: get_fstar_z3.sh destination/directory/bin"
exit 1
fi

mkdir -p "$dest_dir"

for z3_ver in 4.8.5 4.13.3; do
key="$kernel-$arch-$z3_ver"
url="${release_url[$key]}"

destination_file_name="$dest_dir/z3-$z3_ver"
if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi

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..."
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 local keyword 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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! See FStarLang/FStar#3645

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

else
download_z3 "$url" "$z3_ver" "$destination_file_name"
fi
done
Loading