diff --git a/.github/ci.sh b/.github/ci.sh index dcc61295d..8c09e3c7a 100755 --- 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 index 5b3d46ea0..9531d63b6 100644 --- 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,6 +259,8 @@ jobs: path: bin - shell: bash + env: + BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip run: | set -x chmod +x dist/bin/cryptol @@ -264,6 +268,10 @@ jobs: 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