From 7705f280899759a007ee7a94be4ecc99334ff47a Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 10:43:58 -0700 Subject: [PATCH 1/6] Try linear installation of SMT solvers to reveal yices-specific errors. --- .github/ci.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index 7823a1d88..e9e6a9ae3 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -133,11 +133,11 @@ install_llvm() { } install_system_deps() { - install_z3 & + install_z3 # install_cvc4 & - install_yices & - install_llvm & - wait + install_yices + install_llvm + # wait export PATH=$PWD/$BIN:$PATH echo "$PWD/$BIN" >> $GITHUB_PATH is_exe "$BIN" z3 && is_exe "$BIN" yices From f0b09eb5aa406e395bf076897455135ca0c138c6 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 12:33:16 -0700 Subject: [PATCH 2/6] Don't hide curl errors in CI setup. --- .github/ci.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index e9e6a9ae3..9a82c1d14 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -46,7 +46,7 @@ install_z3() { macOS) file="osx-10.14.6.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" + curl -o z3.zip -L "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 @@ -65,9 +65,9 @@ install_cvc4() { esac # Temporary workaround if [[ "$RUNNER_OS" == "Linux" ]]; then - curl -o cvc4$EXT -sL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-08-18-x86_64-linux-opt" + curl -o cvc4$EXT -L "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-08-18-x86_64-linux-opt" else - curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file" + curl -o cvc4$EXT -L "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file" fi $IS_WIN || chmod +x cvc4$EXT mv cvc4$EXT "$BIN/cvc4$EXT" @@ -81,7 +81,7 @@ install_yices() { 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" + curl -o "yices$ext" -L "https://yices.csl.sri.com/releases/$YICES_VERSION/yices-$YICES_VERSION-x86_64-$file" if $IS_WIN; then 7z x -bd "yices$ext" From 4b59dea4a6792531756c386c37c2a61bdfe2ad29 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 17:43:27 -0700 Subject: [PATCH 3/6] Can we get llvm @ 11? --- .github/ci.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/ci.sh b/.github/ci.sh index 9a82c1d14..dbcdf9e15 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -123,7 +123,7 @@ install_llvm() { if [[ "$RUNNER_OS" = "Linux" ]]; then sudo apt-get update -q && sudo apt-get install -y clang-10 llvm-10-tools elif [[ "$RUNNER_OS" = "macOS" ]]; then - brew install llvm@10 + brew install llvm@11 elif [[ "$RUNNER_OS" = "Windows" ]]; then choco install llvm else From 10bd4c837742073c30f57d77fa9315f5b6d2e98e Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 18:09:43 -0700 Subject: [PATCH 4/6] Add CACHE_VERSION selector to wasm github action workflow. --- .github/workflows/crucible-wasm-build.yml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/.github/workflows/crucible-wasm-build.yml b/.github/workflows/crucible-wasm-build.yml index 43f8e48b4..cce90c0e8 100644 --- a/.github/workflows/crucible-wasm-build.yml +++ b/.github/workflows/crucible-wasm-build.yml @@ -5,6 +5,19 @@ on: pull_request: workflow_dispatch: +# The CACHE_VERSION can be updated to force the use of a new cache if +# the current cache contents become corrupted/invalid. This can +# sometimes happen when (for example) the OS version is changed but +# older .so files are cached, which can have various effects +# (e.g. cabal complains it can't find a valid version of the "happy" +# tool). +# +# This also periodically happens on MacOS builds due to a tar bug +# (symptom: "No suitable image found ... unknown file type, first +# eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00") +env: + CACHE_VERSION: 1 + jobs: build: runs-on: ${{ matrix.os }} @@ -54,9 +67,9 @@ jobs: path: | ${{ steps.setup-haskell.outputs.cabal-store }} dist-newstyle - key: cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} + key: ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} restore-keys: | - cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- + ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- - shell: bash run: .github/ci.sh install_system_deps From f6872261e029e23633c5cb3d7672744ee404780b Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 18:10:14 -0700 Subject: [PATCH 5/6] Add CACHE_VERSION selector to crux-llvm github action workflow. --- .github/workflows/crux-llvm-build.yml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml index 88095a6cd..df4cd9bda 100644 --- a/.github/workflows/crux-llvm-build.yml +++ b/.github/workflows/crux-llvm-build.yml @@ -6,6 +6,19 @@ on: pull_request: workflow_dispatch: +# The CACHE_VERSION can be updated to force the use of a new cache if +# the current cache contents become corrupted/invalid. This can +# sometimes happen when (for example) the OS version is changed but +# older .so files are cached, which can have various effects +# (e.g. cabal complains it can't find a valid version of the "happy" +# tool). +# +# This also periodically happens on MacOS builds due to a tar bug +# (symptom: "No suitable image found ... unknown file type, first +# eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00") +env: + CACHE_VERSION: 1 + jobs: outputs: runs-on: ubuntu-latest @@ -71,9 +84,9 @@ jobs: path: | ${{ steps.setup-haskell.outputs.cabal-store }} dist-newstyle - key: cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} + key: ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} restore-keys: | - cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- + ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- - shell: bash run: .github/ci.sh install_system_deps From 9e6278bc80968589b87860b4f5c66a6f573a8b39 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 30 Mar 2021 18:10:30 -0700 Subject: [PATCH 6/6] Bump mir github action workflow CACHE_VERSION to fix macos. --- .github/workflows/crux-mir-build.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml index a2c0beeef..7712e992c 100644 --- a/.github/workflows/crux-mir-build.yml +++ b/.github/workflows/crux-mir-build.yml @@ -11,8 +11,12 @@ on: # older .so files are cached, which can have various effects # (e.g. cabal complains it can't find a valid version of the "happy" # tool). +# +# This also periodically happens on MacOS builds due to a tar bug +# (symptom: "No suitable image found ... unknown file type, first +# eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00") env: - CACHE_VERSION: 1 + CACHE_VERSION: 2 jobs: outputs: