blob: aee7d0d8180633c170d4db374534da41a83b6985 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
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}"
|
