Some old Coq Dockerfiles

coq-dockerfiles.md

Coq Dockerfiles

These are just experiments. Turns out the ocaml/opam docker containers only use a local copy of the opam repo, so opam update does nothing. Consequently, opam install coq.8.8.1 (for instance) would always say No such package. After I learned that I simply needed to add a remote opam repository to the docker container, regular opam install X started to work again, so my docker files got simpler.

I'm putting these here just to save them somewhere. There are little tricks like apt install X that are sometimes helpful.

Dockerfile 8.8.1

FROM jtpaasch/opam:1.2.2
  
RUN opam repo add coq-released https://coq.inria.fr/opam/released; \
    opam update; \
    opam install coq.8.8.1

Dockerifel 8.8.1-quickchick

FROM jtpaasch/coq:8.8.1
  
RUN opam update; \
    opam install coq-quickchick

Dockerfile 8.8-vst

FROM jtpaasch/coq:8.8-emacs

RUN sudo apt-get update; \
    sudo apt-get install -y wget; \
    mkdir ~/vendor; \
    cd ~/vendor; \
    wget http://compcert.inria.fr/release/compcert-3.3.tgz; \
    wget http://vst.cs.princeton.edu/download/vst-2.2.tgz; \
    tar -xzvf compcert-3.3.tgz; \
    tar -xzvf vst-2.2.tgz

RUN opam install menhir; \
    eval `opam config env`; \
    cd ~/vendor/CompCert-3.3; \
    ./configure -clightgen x86_32-linux; \
    cd ~/vendor/vst; \
    make

RUN sudo mkdir /workspace; \
    sudo chown opam:opam /workspace; \
    cd /workspace; \
    echo "VST_LOC=~/vendor/vst" >> CONFIGURE; \
    echo "CC_LOC=~/vendor/CompCert-3.3" >> CONFIGURE

# Now you can mount the _Software Foundations_ vol 5 directory
# and run `make`.

Dockerfile 8.8-emacs

FROM jtpaasch/coq:8.8-build

RUN sudo apt-get install -y emacs-nox && \
    git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG && \
    make -C ~/.emacs.d/lisp/PG && \
    echo ";; Open .v files with Proof General's Coq mode" >> ~/.emacs && \
    echo "(require 'proof-site \"~/.emacs.d/lisp/PG/generic/proof-site\")" >> ~/.emacs

Dockerfile 8.7-bare

FROM ocaml/opam:ubuntu-16.04_ocaml-4.06.0
RUN opam config exec -- opam install coq

Dockerfile 8.8-build

FROM ocaml/opam:ubuntu-16.04_ocaml-4.06.0

RUN eval `opam config env` && \
    opam install ocamlfind camlp5 num && \
    git clone https://github.com/coq/coq.git && \
    cd coq && \
    git checkout v8.8 && \
    ./configure -local && \
    make

ENV PATH /home/opam/coq/bin:$PATH

ENTRYPOINT ["opam", "config", "exec", "--"]

CMD ["coqtop"]

Dockerfile 8.8-bare-root

FROM ubuntu:bionic

RUN apt-get -qqy update && \                                                                                                                        
    apt-get -qqy install \                                                                                                                          
      software-properties-common \                                                                                                                  
      git \                                                                                                                                         
      make \                                                                                                                                        
      m4 \                                                                                                                                          
      aspcud \                                                                                                                                      
      ocaml \                                                                                                                                       
      opam && \                                                                                                                                     
    apt-get clean && \                                                                                                                              
    rm -rf /var/lib/apt/lists/* && \                                                                                                                
    opam init --compiler=4.06.1 --yes --auto-setup && \                                                                                             
    opam config exec -- opam repo add coq-released https://coq.inria.fr/opam/released && \                                                          
    opam config exec -- opam pin add coq 8.8.0 --yes

ENTRYPOINT ["opam", "config", "exec", "--"]

Dockerfile 8.7-bare-alpine

FROM ocaml/opam:alpine
RUN sudo apk add m4; opam install --yes coq
RUN sudo mkdir -p /workspace
WORKDIR /workspace
ENTRYPOINT ["opam", "config", "exec", "--"]