-
Notifications
You must be signed in to change notification settings - Fork 0
/
Dockerfile
45 lines (29 loc) · 1.42 KB
/
Dockerfile
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
FROM coqorg/coq:8.11.2-ocaml-4.11.2-flambda
MAINTAINER Vasily Pestun "pestun@ihes.fr"
# conda + pythnon 3.10
RUN curl https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh -o \
Miniconda3-latest-Linux-x86_64.sh && bash Miniconda3-latest-Linux-x86_64.sh -b -f
ENV HOME="/home/coq"
ENV CONDA_EXE="${HOME}/miniconda3/bin/conda"
RUN $CONDA_EXE create -n python3.10 python=3.10 -y
ENV CONDA_PREFIX="${HOME}/miniconda3/envs/python3.10"
ENV CONDA_PYTHON_EXE="${HOME}/miniconda3/bin/python"
RUN echo 'PATH=$CONDA_PREFIX/bin:$PATH' >> .profile
RUN $CONDA_EXE install -n python3.10 -c conda-forge capnproto
# apt-get level project dependencies
RUN sudo apt-get update
RUN sudo apt-get --yes install graphviz pkg-config libev-dev libxxhash-dev cmake build-essential
COPY --chown=coq:coq . coq-tactician-api
WORKDIR coq-tactician-api
RUN eval $(opam env) && opam update \
&& opam install --assume-depexts -t ./coq-tactician-api.opam -y
RUN pip install .
# run script proof as in former pytact-test
RUN eval $(opam env) \
&& pytact-prover --with-coq --loglevel=INFO
# run script proof over a single tcp connection
RUN eval $(opam env) \
&& pytact-prover --tcp --with-coq --tcp-sessions 1 --loglevel=INFO
# run dfs proof on a sample file prop with 4 variables in a single tcp session
RUN eval $(opam env) \
&& pytact-prover --tcp --with-coq --tcp-sessions 1 --dfs --test prop4.txt --loglevel=ERROR --dfs-limit=20