diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2020-08-28 17:36:58 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2020-08-28 17:36:58 +0200 |
| commit | a4f73057842e0ea9534dfaa9c1ac2cf5102d8117 (patch) | |
| tree | 2e9731bc3cc4765e38e65546b2a735576d382bf9 /ci | |
| parent | c314187dac30be326b35eab9a6f4665523c2eac0 (diff) | |
| download | smtcoq-a4f73057842e0ea9534dfaa9c1ac2cf5102d8117.tar.gz smtcoq-a4f73057842e0ea9534dfaa9c1ac2cf5102d8117.zip | |
Creating a docker container
Diffstat (limited to 'ci')
| -rw-r--r-- | ci/smtcoq.docker | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/ci/smtcoq.docker b/ci/smtcoq.docker new file mode 100644 index 0000000..2f6d08d --- /dev/null +++ b/ci/smtcoq.docker @@ -0,0 +1,62 @@ +############################################################ +# Dockerfile to build SMTCoq docker image +# Based on the debian image +# Build with `docker build -t smtcoq -f smtcoq.docker .` +# Run with `docker run -ti --rm -e DISPLAY=host.docker.internal:0 smtcoq bash` +# Warning: +# To build the container, dockers needs more that 2GB of memory (8GB is enough). +# On Mac, see: https://docs.docker.com/docker-for-mac/#advanced. +############################################################ + +FROM coqorg/base:4.09.1-flambda +USER coq + +##################### PREREQUISITES ######################## + +RUN sudo apt-get -y update && \ + sudo apt-get -y install wget atool bison flex + +################# INSTALL Coq and SMTCoq ################### + +WORKDIR /home/coq + +RUN opam repo add coq-released https://coq.inria.fr/opam/released && \ + opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev && \ + opam install -y coq-smtcoq coqide + +###################### COMPILE ZChaff ###################### + +WORKDIR /home/coq + +RUN wget http://www.princeton.edu/~chaff/zchaff/zchaff.2008.10.12.zip && \ + aunpack zchaff.2008.10.12.zip && \ + cd zchaff && \ + sed -i -re 's/\/\/ #define VERIFY_ON/#define VERIFY_ON/' zchaff_solver.cpp && \ + make + +###################### COMPILE veriT ####################### + +WORKDIR /home/coq + +RUN wget https://www.lri.fr/~keller/Documents-recherche/Smtcoq/veriT9f48a98.tar.gz && \ + aunpack veriT9f48a98.tar.gz && \ + cd veriT9f48a98 && \ + autoconf && \ + ./configure && \ + make + +###################### DOWNLOAD CVC4 ####################### + +WORKDIR /home/coq/bin + +RUN wget http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt && \ + chmod ugo+x cvc4-1.6-x86_64-linux-opt + +######################### BINARIES ######################### + +WORKDIR /home/coq/bin + +RUN ln -s /home/coq/zchaff/zchaff && \ + ln -s /home/coq/veriT9f48a98/veriT + +ENV PATH="/home/coq/bin:${PATH}" |