From c8c122fac61191162c5c5c106735496a317ecba0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 28 Sep 2021 16:23:16 -0700 Subject: [PATCH 1/2] Migrate Docker images to use what4-solvers builds --- .github/workflows/ci.yml | 3 +- Dockerfile | 60 ++++++----------------------------- cryptol-remote-api/Dockerfile | 49 ++-------------------------- 3 files changed, 13 insertions(+), 99 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e151a2717..00c6e8d9b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -294,7 +294,7 @@ jobs: build-push-image: runs-on: ubuntu-latest needs: [config] - if: github.event_name == 'schedule' + if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' strategy: fail-fast: false matrix: @@ -307,7 +307,6 @@ jobs: file: cryptol-remote-api/Dockerfile image: ghcr.io/galoisinc/cryptol-remote-api cache: ghcr.io/galoisinc/cache-cryptol-remote-api - if: ${{ github.event_name == 'schedule' }} - build-args: PORTABILITY=false file: cryptol-remote-api/Dockerfile image: ghcr.io/galoisinc/cryptol-remote-api diff --git a/Dockerfile b/Dockerfile index 58739509a..b8afbb1a8 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,62 +1,21 @@ -FROM debian:buster-20210511 AS solvers - -# Install needed packages for building -RUN apt-get update \ - && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip -RUN useradd -m user -RUN install -d -o user -g user /solvers -USER user -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 && \ - 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 && \ - ( 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 && \ - ( 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 && \ - cp yices*/bin/yices-smt2 rootfs/usr/local/bin \ - && cp yices*/bin/yices rootfs/usr/local/bin - -# Install CVC4 1.8 -# 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 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/')" && \ -RUN latest="cvc4-2021-03-13-x86_64-linux-opt" && \ - curl --output rootfs/usr/local/bin/cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest" - -# 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 -# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin - -# Set executable and run tests -RUN chmod +x rootfs/usr/local/bin/* - FROM haskell:8.8.4 AS build -RUN apt-get update && apt-get install -y libncurses-dev -COPY --from=solvers /solvers/rootfs / +RUN apt-get update && apt-get install -y libncurses-dev unzip RUN useradd -m cryptol COPY --chown=cryptol:cryptol . /cryptol USER cryptol WORKDIR /cryptol +RUN mkdir -p rootfs/usr/local/bin +WORKDIR /cryptol/rootfs/usr/local/bin +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip" +RUN unzip solvers.zip && rm solvers.zip && chmod +x * +WORKDIR /cryptol ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH +RUN z3 --version ARG CRYPTOLPATH="/cryptol/.cryptol" ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 COPY cabal.GHC-8.8.4.config cabal.project.freeze -RUN mkdir -p rootfs/usr/local/bin RUN cabal v2-update && \ cabal v2-build -j cryptol:exe:cryptol && \ cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \ @@ -66,8 +25,8 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH RUN ! $(cryptol -c ":s prover=yices" | 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=abc" | tail -n +2 | grep -q .) \ - && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \ + && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \ + # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \ && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .) RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ && cp -r lib/* rootfs/"${CRYPTOLPATH}" @@ -80,7 +39,6 @@ RUN apt-get update \ && apt-get clean && rm -rf /var/lib/apt/lists/* RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol COPY --from=build /cryptol/rootfs / -COPY --from=solvers /solvers/rootfs / USER cryptol ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 diff --git a/cryptol-remote-api/Dockerfile b/cryptol-remote-api/Dockerfile index 58acb2c4f..f5871e8b6 100644 --- a/cryptol-remote-api/Dockerfile +++ b/cryptol-remote-api/Dockerfile @@ -1,49 +1,5 @@ ARG GHCVER="8.10.3" ARG GHCVER_BOOTSTRAP="8.10.2" -FROM debian:buster-20210511 AS solvers - -# Install needed packages for building -RUN apt-get update \ - && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip -RUN useradd -m user -RUN install -d -o user -g user /solvers -USER user -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 && \ - 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 && \ - ( 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 && \ - ( 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 && \ - cp yices*/bin/yices-smt2 rootfs/usr/local/bin \ - && cp yices*/bin/yices rootfs/usr/local/bin - -# Install CVC4 1.8 -# 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 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/')" && \ - curl --output rootfs/usr/local/bin/cvc4 -sSL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/$latest" - -# 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 -# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin - -# Set executable and run tests -RUN chmod +x rootfs/usr/local/bin/* - FROM debian:buster-20210511 AS toolchain ARG PORTABILITY=false RUN apt-get update && apt-get install -y libncurses-dev libz-dev \ @@ -53,7 +9,6 @@ ENV GHCUP_INSTALL_BASE_PREFIX=/opt \ PATH=/opt/.ghcup/bin:$PATH RUN curl -o /usr/local/bin/ghcup "https://downloads.haskell.org/~ghcup/0.1.14/x86_64-linux-ghcup-0.1.14" && \ chmod +x /usr/local/bin/ghcup -COPY --from=solvers /solvers/rootfs / RUN ghcup install cabal --set ENV PATH=/root/.cabal/bin:$PATH ADD ./cryptol-remote-api/ghc-portability.patch . @@ -101,6 +56,9 @@ RUN cabal v2-update && \ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ && cp -r lib/* rootfs/"${CRYPTOLPATH}" +WORKDIR /cryptol/rootfs/usr/local/bin +RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip" && \ + unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /cryptol/rootfs @@ -110,7 +68,6 @@ RUN apt-get update \ && apt-get clean && rm -rf /var/lib/apt/lists/* RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol COPY --from=build /cryptol/rootfs / -COPY --from=solvers /solvers/rootfs / USER cryptol ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 From 5f769af694a261db183212c25f2af939cb1d0130 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 29 Sep 2021 08:13:42 -0700 Subject: [PATCH 2/2] Install unzip in cryptol-remote-api/Dockerfile --- cryptol-remote-api/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-remote-api/Dockerfile b/cryptol-remote-api/Dockerfile index f5871e8b6..3fd27ce70 100644 --- a/cryptol-remote-api/Dockerfile +++ b/cryptol-remote-api/Dockerfile @@ -2,7 +2,7 @@ ARG GHCVER="8.10.3" ARG GHCVER_BOOTSTRAP="8.10.2" FROM debian:buster-20210511 AS toolchain ARG PORTABILITY=false -RUN apt-get update && apt-get install -y libncurses-dev libz-dev \ +RUN apt-get update && apt-get install -y libncurses-dev libz-dev unzip \ build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \ $(if ${PORTABILITY}; then echo git autoconf python3; fi) ENV GHCUP_INSTALL_BASE_PREFIX=/opt \