Merge pull request #1284 from GaloisInc/at-prebuilt-solvers

Use prebuilt solver binaries from what4-solvers
GaloisInc · Sep 17, 2021 · 30af0ba · 30af0ba
2 parents ee8cbac + 1bb2b54
commit 30af0ba
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 69 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -9,6 +9,14 @@ mkdir -p "$BIN"
 
 is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; }
 
+deps() {
+  case "$RUNNER_OS" in
+    Linux) ldd $1 || true ;;
+    macOS) otool -L $1 || true ;;
+    Windows) ldd $1 || true ;;
+  esac
+}
+
 extract_exe() {
   exe="$(cabal v2-exec which "$1$EXT")"
   name="$(basename "$exe")"
@@ -45,63 +53,6 @@ setup_dist_bins() {
   strip dist/bin/cryptol* || echo "Strip failed: Ignoring harmless error"
 }
 
-install_z3() {
-  is_exe "$BIN" "z3" && return
-
-  case "$RUNNER_OS" in
-    Linux) file="ubuntu-18.04.zip" ;;
-    macOS) file="osx-10.15.7.zip" ;;
-    Windows) file="win.zip" ;;
-  esac
-  curl -o z3.zip -sL "https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/z3-$Z3_VERSION-x64-$file"
-
-  if $IS_WIN; then 7z x -bd z3.zip; else unzip z3.zip; fi
-  cp z3-*/bin/z3$EXT $BIN/z3$EXT
-  $IS_WIN || chmod +x $BIN/z3
-  rm z3.zip
-}
-
-install_cvc4() {
-  version="${CVC4_VERSION#4.}" # 4.y.z -> y.z
-
-  case "$RUNNER_OS" in
-    Linux) file="x86_64-linux-opt" ;;
-    Windows) file="win64-opt.exe" ;;
-    macOS) file="macos-opt" ;;
-  esac
-  # Temporary workaround
-  if [[ "$RUNNER_OS" == "Linux" ]]; then
-    #latest="$(curl -sSL "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/" | grep linux-opt | tail -n1 | sed -e 's/.*href="//' -e 's/\([^>]*\)">.*$/\1/')"
-    latest="cvc4-2021-03-13-x86_64-linux-opt"
-    curl -o cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest"
-  else
-    curl -o cvc4$EXT -sSL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
-  fi
-  $IS_WIN || chmod +x cvc4$EXT
-  mv cvc4$EXT "$BIN/cvc4$EXT"
-}
-
-install_yices() {
-  ext=".tar.gz"
-  case "$RUNNER_OS" in
-    Linux) file="pc-linux-gnu-static-gmp.tar.gz" ;;
-    macOS) file="apple-darwin18.7.0-static-gmp.tar.gz" ;;
-    Windows) file="pc-mingw32-static-gmp.zip" && ext=".zip" ;;
-  esac
-  curl -o "yices$ext" -sL "https://yices.csl.sri.com/releases/$YICES_VERSION/yices-$YICES_VERSION-x86_64-$file"
-
-  if $IS_WIN; then
-    7z x -bd "yices$ext"
-    mv "yices-$YICES_VERSION"/bin/*.exe "$BIN"
-  else
-    tar -xzf "yices$ext"
-    pushd "yices-$YICES_VERSION" || exit
-    sudo ./install-yices
-    popd || exit
-  fi
-  rm -rf "yices$ext" "yices-$YICES_VERSION"
-}
-
 build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
@@ -114,10 +65,9 @@ build() {
 }
 
 install_system_deps() {
-  install_z3 &
-  install_cvc4 &
-  install_yices &
-  wait
+  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BIN_ZIP_FILE" && unzip -o bins.zip && rm bins.zip)
+  chmod +x $BIN/*
+  cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
   is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
@@ -169,6 +119,7 @@ zip_dist_with_solvers() {
   : "${VERSION?VERSION is required as an environment variable}"
   name="${name:-"cryptol-$VERSION-$RUNNER_OS-x86_64"}"
   sname="${name}-with-solvers"
+  cp "$(which abc)"        dist/bin/
   cp "$(which cvc4)"       dist/bin/
   cp "$(which yices)"      dist/bin/
   cp "$(which yices-smt2)" dist/bin/

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -9,9 +9,7 @@ on:
   workflow_dispatch:
 
 env:
-  Z3_VERSION: "4.8.10"
-  CVC4_VERSION: "4.1.8"
-  YICES_VERSION: "2.6.2"
+  SOLVER_PKG_VERSION: "snapshot-20210917"
 
 jobs:
   config:
@@ -57,6 +55,8 @@ jobs:
         ghc-version: ["8.6.5", "8.8.4", "8.10.2"]
         exclude:
           # https://gitlab.haskell.org/ghc/ghc/-/issues/18550
+          - os: windows-latest
+            ghc-version: 8.8.4
           - os: windows-latest
             ghc-version: 8.10.2
     outputs:
@@ -94,6 +94,8 @@ jobs:
 
       - shell: bash
         run: .github/ci.sh install_system_deps
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
 
       - shell: bash
         env:
@@ -219,10 +221,10 @@ jobs:
             target: ''
             os: ubuntu-latest
             continue-on-error: false
-          - suite: rpc
-            target: ''
-            os: macos-latest
-            continue-on-error: false
+          #- suite: rpc
+          #  target: ''
+          #  os: macos-latest
+          #  continue-on-error: false
           #- suite: rpc
           #  target: ''
           #  os: windows-latest
@@ -234,7 +236,7 @@ jobs:
 
       - uses: haskell/actions/setup@v1
         with:
-          ghc-version: '8.10.2'
+          ghc-version: '8.10.3'
 
       - if: matrix.suite == 'rpc'
         uses: actions/setup-python@v2
@@ -257,13 +259,19 @@ jobs:
           path: bin
 
       - shell: bash
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
         run: |
           set -x
           chmod +x dist/bin/cryptol
           chmod +x dist/bin/cryptol-remote-api
           chmod +x dist/bin/cryptol-eval-server
           chmod +x bin/test-runner
           .github/ci.sh install_system_deps
+          .github/ci.sh deps bin/abc*
+          .github/ci.sh deps bin/cvc4*
+          .github/ci.sh deps bin/yices-smt2*
+          .github/ci.sh deps bin/z3*
           ghc_ver="$(ghc --numeric-version)"
           cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
           cabal v2-update