From a4f73057842e0ea9534dfaa9c1ac2cf5102d8117 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Fri, 28 Aug 2020 17:36:58 +0200
Subject: Creating a docker container

---
 ci/smtcoq.docker | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 ci/smtcoq.docker

(limited to 'ci')

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}"
-- 
cgit