diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-08-28 20:11:48 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-08-28 20:11:48 +0200 |
| commit | 3d11e77273cfb6e10758ad242035e106f502fda8 (patch) | |
| tree | 789df3f0d3e85994622157e0927da5b41eb3d811 /ci | |
| parent | a4f73057842e0ea9534dfaa9c1ac2cf5102d8117 (diff) | |
| download | smtcoq-3d11e77273cfb6e10758ad242035e106f502fda8.tar.gz smtcoq-3d11e77273cfb6e10758ad242035e106f502fda8.zip | |
Full docker script
Diffstat (limited to 'ci')
| -rw-r--r-- | ci/smtcoq.docker | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/ci/smtcoq.docker b/ci/smtcoq.docker index 2f6d08d..aee7d0d 100644 --- a/ci/smtcoq.docker +++ b/ci/smtcoq.docker @@ -3,6 +3,7 @@ # 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` +# or `docker run --net=host --env="DISPLAY" --volume="$HOME/.Xauthority:/home/coq/.Xauthority:rw" smtcoq coqide` # 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. @@ -22,6 +23,7 @@ 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 depext -y coq-smtcoq coqide && \ opam install -y coq-smtcoq coqide ###################### COMPILE ZChaff ###################### @@ -47,16 +49,27 @@ RUN wget https://www.lri.fr/~keller/Documents-recherche/Smtcoq/veriT9f48a98.tar. ###################### DOWNLOAD CVC4 ####################### -WORKDIR /home/coq/bin +WORKDIR /home/coq 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 +##################### LFSC SIGNATURES ###################### + +WORKDIR /home/coq + +RUN git clone https://github.com/smtcoq/smtcoq.git + +ENV LFSCSIGS="/home/coq/smtcoq/src/lfsc/tests/signatures/" + +ENV DONTSHOWVERIT="yes" + ######################### BINARIES ######################### WORKDIR /home/coq/bin RUN ln -s /home/coq/zchaff/zchaff && \ - ln -s /home/coq/veriT9f48a98/veriT + ln -s /home/coq/veriT9f48a98/veriT && \ + ln -s /home/coq/cvc4-1.6-x86_64-linux-opt cvc4 ENV PATH="/home/coq/bin:${PATH}" |