Merge pull request #119 from project-everest/nik_get_z3

add downloading z3 4.13.3 and 4.8.5 to the everest script

everest

@@ -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"
 }
 
@@ -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
 }
@@ -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 $z3_versions_dest" true
   fi
+
 }
 
 do_check ()

get_fstar_z3.sh

@@ -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..."
+  else
+    download_z3 "$url" "$z3_ver" "$destination_file_name"
+  fi
+done