GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 09:20:24 +03:00
Code Issues Projects Releases Wiki Activity
755d4d2de3
cryptol/Dockerfile

83 lines
3.3 KiB
Docker
Raw Normal View History

Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
from debian:buster AS solvers
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
# Install needed packages for building
RUN apt-get update \
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
&& apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
RUN useradd -m user
RUN install -d -o user -g user /solvers
USER user
WORKDIR /solvers
RUN mkdir -p rootfs/usr/local/bin
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
# 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
# Build abc from GitHub. (Latest version.)
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
RUN git clone https://github.com/berkeley-abc/abc.git
RUN cd abc && make -j$(nproc)
RUN 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
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
# Install Yices 2.6.2
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
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
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
&& cp yices*/bin/yices rootfs/usr/local/bin
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
# Install CVC4 1.8
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
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
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
# 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/*
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
FROM haskell:8.8 AS build
RUN apt-get update && apt-get install -y libncurses-dev
COPY --from=solvers /solvers/rootfs /
RUN useradd -m cryptol \
&& su -c '/opt/cabal/bin/cabal v2-update' cryptol
COPY --chown=cryptol:cryptol . /cryptol
USER cryptol
WORKDIR /cryptol
ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH
ARG CRYPTOLPATH="/cryptol/.cryptol"
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-install --install-method=copy --installdir=rootfs/usr/local/bin exe:cryptol
RUN cabal v2-install --install-method=copy --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
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
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=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 .) \
&& ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
&& cp -r lib/* rootfs/"${CRYPTOLPATH}"
USER root
RUN chown -R root:root /cryptol/rootfs
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
FROM debian:buster-slim
Update Docker build to use Debian as a base This makes it easier to do Haskell builds and incorporate external tools, even though it results in a slightly bigger image.
2019-04-17 01:16:24 +03:00
RUN apt-get update \
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
&& apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \
Implement GitHub actions (#722) * Builds nightly binary tarballs on Linux, macOS, and Windows * Runs tests on every PR and merge to master * Includes GitHub Actions status in README instead of Travis * Makes the GitRev recompile hack less fragile * Makes the Makefile Cabal v3 compatible * Builds the manual as part of the CI process
2020-05-14 20:50:22 +03:00
&& apt-get clean && rm -rf /var/lib/apt/lists/*
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
Add Dockerfile.
2018-06-26 21:10:28 +03:00
COPY --from=build /cryptol/rootfs /
Add additional SMT solvers to Docker image. (#811) * Add additional SMT solvers to Docker image. This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired. This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone. As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well. Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
2020-07-14 02:47:25 +03:00
COPY --from=solvers /solvers/rootfs /
Add Dockerfile.
2018-06-26 21:10:28 +03:00
USER cryptol
Build system and documentation cleanup (#816) * Remove `Makefile` * Remove Travis and AppVeyor configurations * Improve portability of the `cry` script * Fix Docker builds * Update documentation to remove references to `make` * Update copyright dates * Fix omitted section of CONTRIBUTING.md * Update Z3 installation instructions Fixes #570, #603, #790, #807.
2020-07-14 20:58:38 +03:00
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8
Add Dockerfile.
2018-06-26 21:10:28 +03:00
ENTRYPOINT ["/usr/local/bin/cryptol"]
Reference in New Issue Copy Permalink