mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-16 17:30:27 +03:00
CVC4 linux fixes (#871)
* add cvc4 version workaround * bump z3 version in github actions to match dockerfile
This commit is contained in:
parent
e75aaef5a0
commit
3a379bcbc0
7
.github/ci.sh
vendored
7
.github/ci.sh
vendored
@ -74,7 +74,12 @@ install_cvc4() {
|
||||
Windows) file="win64-opt.exe" ;;
|
||||
macOS) file="macos-opt" ;;
|
||||
esac
|
||||
curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
|
||||
# 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"
|
||||
else
|
||||
curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
|
||||
fi
|
||||
$IS_WIN || chmod +x cvc4$EXT
|
||||
mv cvc4$EXT "$BIN/cvc4$EXT"
|
||||
}
|
||||
|
2
.github/workflows/build.yml
vendored
2
.github/workflows/build.yml
vendored
@ -82,7 +82,7 @@ jobs:
|
||||
- shell: bash
|
||||
run: .github/ci.sh install_system_deps
|
||||
env:
|
||||
Z3_VERSION: "4.8.7"
|
||||
Z3_VERSION: "4.8.8"
|
||||
CVC4_VERSION: "4.1.8"
|
||||
YICES_VERSION: "2.6.2"
|
||||
|
||||
|
37
Dockerfile
37
Dockerfile
@ -1,4 +1,4 @@
|
||||
from debian:buster AS solvers
|
||||
FROM debian:buster AS solvers
|
||||
|
||||
# Install needed packages for building
|
||||
RUN apt-get update \
|
||||
@ -10,27 +10,29 @@ WORKDIR /solvers
|
||||
RUN mkdir -p rootfs/usr/local/bin
|
||||
|
||||
# Get Z3 4.8.8 from GitHub
|
||||
RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip --output z3.zip
|
||||
RUN unzip z3.zip
|
||||
RUN mv z3-*/bin/z3 rootfs/usr/local/bin
|
||||
RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip --output z3.zip && \
|
||||
unzip z3.zip && \
|
||||
mv z3-*/bin/z3 rootfs/usr/local/bin
|
||||
|
||||
# Build abc from GitHub. (Latest version.)
|
||||
RUN git clone https://github.com/berkeley-abc/abc.git
|
||||
RUN cd abc && make -j$(nproc)
|
||||
RUN cp abc/abc rootfs/usr/local/bin
|
||||
RUN git clone https://github.com/berkeley-abc/abc.git && \
|
||||
( cd abc && make -j$(nproc) ) && \
|
||||
cp abc/abc rootfs/usr/local/bin
|
||||
|
||||
# Build Boolector release 3.2.1 from source
|
||||
RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz
|
||||
RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc)
|
||||
RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin
|
||||
RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz && \
|
||||
( cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc) ) && \
|
||||
cp boolector*/build/bin/boolector rootfs/usr/local/bin
|
||||
|
||||
# Install Yices 2.6.2
|
||||
RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz
|
||||
RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
|
||||
RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz && \
|
||||
cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
|
||||
&& cp yices*/bin/yices rootfs/usr/local/bin
|
||||
|
||||
# Install CVC4 1.8
|
||||
RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
|
||||
# The latest CVC4 1.8 and the release version has a minor discrepency between it, causing sbv to fail
|
||||
# https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
|
||||
RUN curl -L https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-08-18-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
|
||||
|
||||
# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
|
||||
# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
|
||||
@ -53,13 +55,14 @@ ENV LANG=C.UTF-8 \
|
||||
LC_ALL=C.UTF-8
|
||||
COPY cabal.GHC-8.8.3.config cabal.project.freeze
|
||||
RUN mkdir -p rootfs/usr/local/bin
|
||||
RUN cabal v2-update
|
||||
RUN cabal v2-install --install-method=copy --installdir=rootfs/usr/local/bin exe:cryptol
|
||||
RUN cabal v2-install --install-method=copy --installdir=bin test-lib
|
||||
RUN cabal v2-update && \
|
||||
cabal v2-build -j cryptol:exe:cryptol && \
|
||||
cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \
|
||||
cabal v2-install --install-method=copy --overwrite-policy=always --installdir=bin test-lib
|
||||
RUN ./bin/test-runner --ext=.icry --exe=./rootfs/usr/local/bin/cryptol -F -b tests
|
||||
ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
|
||||
RUN ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
|
||||
# && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
|
||||
# && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
|
||||
&& ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
|
||||
&& ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
|
||||
&& ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
|
||||
|
Loading…
Reference in New Issue
Block a user