Make CI MacOS compatible (#239)

- Adapts the solver install scripts to be MacOS compatible. 
- runs CI on Linux and MacOS on push

Author: sankalpgambhir

.github/workflows/inox-CI.yml

@@ -8,15 +8,19 @@ on:
 jobs:
   tests:
     if: github.event.pull_request.draft == false
-    runs-on: [self-hosted, linux]
+    name: ${{ matrix.runners.name }} / JDK ${{ matrix.java-version }}
+    runs-on: ${{ matrix.runners.labels }}
     strategy:
       matrix:
+        runners:
+          - name: Linux
+            os: Linux
+            labels: ['self-hosted', 'linux']
+          - name: macOS ARM64
+            os: macOS
+            labels: ['self-hosted', 'macOS', 'ARM64']
         java-version: [17, 21]
     env:
-      # define Java options for both official sbt and sbt-extras
-      JAVA_OPTS_TMP_DIR: ./tmp_java
-      JAVA_OPTS: -Xss64M -Xms1024M -Xmx8G -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR
-      JVM_OPTS:  -Xss64M -Xms1024M -Xmx8G -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR
       # solver versions to test against
       INSTALL_SOLVERS: 1
       Z3_VER: 4.15.1
@@ -32,17 +36,30 @@ jobs:
       with:
         distribution: temurin
         java-version: ${{ matrix.java-version }}
-    - name: Install and unpack sbt
+    - name: Set Java and SBT options
+      run: |
+        # path for sbt to create a local folder and sockets
+        # needs to be a bit shallower than the workspace
+        # to avoid unix socket path length limits
+        echo "XDG_RUNTIME_DIR=$(realpath ..)" >> $GITHUB_ENV
+        # java options for sbt and sbt-extras
+        JAVA_OPTS_TMP_DIR=./tmp_java
+        JAVA_OPTS="-Xss64M -Xms1024M -Xmx8G -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR"
+        JVM_OPTS="$JAVA_OPTS"
+        echo "JAVA_OPTS_TMP_DIR=$JAVA_OPTS_TMP_DIR" >> $GITHUB_ENV
+        echo "JAVA_OPTS=$JAVA_OPTS" >> $GITHUB_ENV
+        echo "JVM_OPTS=$JVM_OPTS" >> $GITHUB_ENV 
+    - name: Install and set up sbt
       run: |
         ./scripts/install_sbt.sh
-        echo "PATH=./sbt/bin/:$PATH" >> "$GITHUB_ENV"
+        echo "$(pwd)/sbt/bin/" >> $GITHUB_PATH
     - name: Prepare temp folder
       run: rm -rf $JAVA_OPTS_TMP_DIR && mkdir -p $JAVA_OPTS_TMP_DIR
     - name: Install solvers
       run: ./scripts/install_solvers.sh $GITHUB_WORKSPACE/.local/bin $Z3_VER $CVC4_VER $CVC5_VER
     - name: Add solvers to PATH
       run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
-    - name: Test solvers availability
+    - name: Test solver availability
       run: cvc5 --version && z3 --version && cvc4 --version
     - name: Run Tests
       run: sbt -Dtest-parallelism=10 -batch test

.github/workflows/inox-mac-CI.yml

@@ -1,9 +1,11 @@
 #!/usr/bin/env sh
 
+CURL='curl -L -s -C - -O'
+
 SBT_VER="$(grep 'sbt.version' project/build.properties | cut -d= -f2)"
 if [ -z "$SBT_VER" ]; then
   echo "sbt.version not found in project/build.properties"
   exit 1
 fi
-wget -c https://github.com/sbt/sbt/releases/download/v${SBT_VER}/sbt-${SBT_VER}.tgz -q
+$CURL https://github.com/sbt/sbt/releases/download/v${SBT_VER}/sbt-${SBT_VER}.tgz
 tar xfz "sbt-${SBT_VER}.tgz"

scripts/install_sbt.sh

@@ -5,6 +5,13 @@ if [ "$INSTALL_SOLVERS" != "1" ]; then
   exit 0
 fi
 
+INFO_MSG="[INFO]"
+WARN_MSG="\033[33m[WARNING]\033[0m"
+ERROR_MSG="\033[1;31m[ERROR]\033[0m"
+
+# curl command with default flags
+CURL='curl -L -s -C -'
+
 TEMP_DIR="$(pwd)/temp"
 SOLVERS_DIR=${1:-"$(pwd)/solvers"}
 
@@ -19,36 +26,65 @@ SHORT_ARCH=$(uname -m | sed 's/x86_64/x64/;s/aarch64/arm64/;')
 
 # libc linked against z3
 # (glibc for Linux, osx for macOS)
-LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+Z3_LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+
+# os names as used by CVC5 builds
+CVC5_OS_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/macOS/;s/linux/Linux/;')
 
 mkdir -p "$SOLVERS_DIR"
 mkdir -p "$TEMP_DIR"
+
+reset_temp_dir() {
+  rm -rf "$TEMP_DIR"
+  mkdir -p "$TEMP_DIR"
+}
+
+echo "$INFO_MSG Installing Solvers to $SOLVERS_DIR"
+
 # cvc5
-wget -c "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-Linux-${ARCH}-static.zip" -O "$TEMP_DIR/cvc5.zip" -q
-unzip "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR" 
+echo "$INFO_MSG Installing cvc5 (v${CVC5_VER})"
+
+$CURL "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-${CVC5_OS_NAME}-${ARCH}-static.zip" --output "$TEMP_DIR/cvc5.zip"
+unzip -q "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR" 
 CVC5_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*cvc5*")
 mv "$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5"
 chmod +x "$SOLVERS_DIR/cvc5"
-rm -rf "$TEMP_DIR"
 
-# # CVC4
-wget -c "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" -O "$SOLVERS_DIR/cvc4" -q
+reset_temp_dir
+
+# CVC4
+echo "$INFO_MSG Installing CVC4 (v${CVC4_VER})"
+
+if [ "$CVC5_OS_NAME" = "macOS" ]; then
+  echo "$WARN_MSG CVC4 installation on macOS; defaulting to only build available (x86_64 v1.8)"
+  $CURL "https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-macos-opt" --output "$SOLVERS_DIR/cvc4"
+elif [ "$CVC5_OS_NAME" = "Linux" ]; then
+  $CURL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" --output "$SOLVERS_DIR/cvc4"
+else
+  echo "$ERROR_MSG CVC4 installation not supported on unknown OS: $CVC5_OS_NAME"
+  exit 1
+fi
 chmod +x "$SOLVERS_DIR/cvc4"
 
+reset_temp_dir
+
 # z3
-mkdir -p "$TEMP_DIR"
-Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
+echo "$INFO_MSG Installing Z3 (v${Z3_VER})"
+
+# z3 release file names contain libc versions in them, which makes them hard to
+# guess. Just get the correct one via the GitHub release API.
+Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${Z3_LIBC_NAME}" # followed by -<libcversion>.zip
 Z3_URL=$(
-  curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
-  grep "browser_download_url.*${Z3_FILE_PREFIX}" | #| # find url for the correct build
+  $CURL "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
+  grep "browser_download_url.*${Z3_FILE_PREFIX}" | # find url for the correct build
   sed 's/^.*: //;s/^"//;s/"$//' # strip non-url
 )
-wget -c "${Z3_URL}" -O "$TEMP_DIR/z3.zip" -q
-unzip "$TEMP_DIR/z3.zip" -d "$TEMP_DIR" 
+$CURL "${Z3_URL}" --output "$TEMP_DIR/z3.zip"
+unzip -q "$TEMP_DIR/z3.zip" -d "$TEMP_DIR" 
 Z3_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*z3*")
 mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
 chmod +x "$SOLVERS_DIR/z3"
 rm -rf "$TEMP_DIR"
 
-echo "************** Solvers Installed **************"
-exit 0
+echo "$INFO_MSG Solvers Installed"
+exit 0