Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11

1 files changed, 75 insertions, 0 deletions

diff --git a/ci/smtcoq.docker b/ci/smtcoq.docker
new file mode 100644
index 0000000..aee7d0d
--- /dev/null
+++ b/ci/smtcoq.docker
@@ -0,0 +1,75 @@
+############################################################
+# 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`
+#   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.
+############################################################
+
+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 depext -y coq-smtcoq coqide && \
+    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
+
+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/cvc4-1.6-x86_64-linux-opt cvc4
+
+ENV PATH="/home/coq/bin:${PATH}"