Merge pull request #3646 from FStarLang/gebner_getz3_macos

Support `get_fstar_z3.sh` on macos
FStarLang · Dec 26, 2024 · a3be612 · a3be612
2 parents dbc1020 + fb063f6
commit a3be612
Showing 1 changed file with 43 additions and 15 deletions.
diff --git a/bin/get_fstar_z3.sh b/bin/get_fstar_z3.sh
@@ -11,15 +11,28 @@ 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.13.3/z3-4.13.3-x64-win.zip"
+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"
+  "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"
+  "Windows-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
+  "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"
+  "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"
+  "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"
+  "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"
+  "Windows-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip"
+)
+
+get_url() {
+  local key elem
+  key="$1"
+
+  for elem in "${release_url[@]}"; do
+    if [ "${elem%%:*}" = "$key" ]; then
+      echo -n "${elem#*:}"
+      break
+    fi
+  done
+}
 
 trap "exit 1" HUP INT PIPE QUIT TERM
 cleanup() {
@@ -30,6 +43,7 @@ cleanup() {
 trap "cleanup" EXIT
 
 download_z3() {
+  local url version destination_file_name base_name z3_path
   url="$1"
   version="$2"
   destination_file_name="$3"
@@ -62,17 +76,31 @@ 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"
+    key="$kernel-$arch-$z3_ver"
+
+    case "$key" in
+      Linux-aarch64-4.8.5)
+        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install qemu-user (and shared libraries) to execute it."
+        key="$kernel-x86_64-$z3_ver"
+        ;;
+      Darwin-aarch64-4.8.5)
+        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install Rosetta 2 to execute it."
+        key="$kernel-x86_64-$z3_ver"
+        ;;
+    esac
+
+    url="$(get_url "$key")"
+
+    if [ -z "$url" ]; then
+      echo ">>> Z3 $z3_ver not available for this architecture, skipping..."
+    else
+      download_z3 "$url" "$z3_ver" "$destination_file_name"
+    fi
   fi
 done