Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use prebuilt solver binaries from what4-solvers #1284

Merged
merged 12 commits into from
Sep 17, 2021
Merged

Use prebuilt solver binaries from what4-solvers #1284

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
c8bfa20
Use prebuilt solver binaries from what4-solvers
Sep 14, 2021
5fbb175
Fix typo in solver binary archive names
Sep 14, 2021
aa3426e
Fix Yices executable name
Sep 14, 2021
88d24a1
Always overwrite solvers when unzipping
Sep 14, 2021
bdb2c96
Make solver package version configurable
Sep 14, 2021
c537017
Include abc in with-solvers tarballs
Sep 14, 2021
5e31bd0
Attempt to fix build stall on Windows
Sep 15, 2021
45c28c3
Switch back to GHC 8.10.2 for now
Sep 15, 2021
94a32f9
Disable RPC tests on macOS
Sep 17, 2021
b885441
Check dynamic library dependencies of solvers
Sep 17, 2021
6cd4383
Fix solver dependency analysis
Sep 17, 2021
1bb2b54
Bump solver package snapshot version
Sep 17, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 12 additions & 61 deletions .github/ci.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ;;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the intent of the || true for these? It will always allow these to succeed, so is this just for getting logging output to show which binary is running and the validity of the available shared libs?

Copy link
Contributor Author

@atomb atomb Sep 20, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At least ldd (and maybe otool?) return non-zero for statically-linked executables, and some of the executables we generate are expected to be statically linked. And, ultimately, yeah, the purpose of this is to have extra log output to help with debugging.

esac
}

extract_exe() {
exe="$(cabal v2-exec which "$1$EXT")"
name="$(basename "$exe")"
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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/
Expand Down
24 changes: 16 additions & 8 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down