Coq docker file

Dockerfile

# docker build -t coq .
# coqtop() (docker run --rm -v "$HOME:$HOME" -ti coq sh -c "cd $HOME ; "'coqtop $(cat ~/src/VST/_CoqProject-export)'" $@")

#FROM coqorg/coq:dev
FROM coqorg/coq:8.11.0

RUN opam init -y; \
    opam repo --set-default add coq-released https://coq.inria.fr/opam/released; \
    opam install -y -b coq-mathcomp-algebra coq-mathcomp-analysis coq-coquelicot coq-compcert
    
RUN opam install -y -b coq-geometric-algebra

RUN opam install -y -b coq-equations coq-flocq coq-coqeal

RUN sh -lc "mkdir ~/src; cd src; git clone https://github.com/PrincetonUniversity/VST.git; cd VST; make -j"

RUN opam install -y coq-coq2html

RUN \
  cd ~/.opam/4.05.0/.opam-switch/build; \
  DOC=~/doc; mkdir -p $DOC; \
  rm -f $DOC/*; \
  ~/.opam/4.05.0/bin/coqdoc -utf8 -d $DOC \
    -R ~/src/VST VST $(find ~/src/VST -name \*.v) \
    -R coq-flocq.*/src Flocq  $(find coq-flocq.*/src -name \*.v) \
    -R coq-coqeal.* CoqEAL  $(find coq-coqeal.* -name \*.v) \
    -R coq-coquelicot.*/theories Coquelicot  $(find coq-coquelicot.*/theories -name \*.v) \
    -R coq-equations.*/theories Equations  $(find coq-equations.*/theories -name \*.v) \
    -R coq-geometric-algebra.* GeometricAlgebra  $(find coq-geometric-algebra.* -name \*.v) \
    -R coq-mathcomp-algebra.* mathcomp  $(find coq-mathcomp-algebra.*/mathcomp/algebra -name \*.v) \
    -R coq-mathcomp-analysis.* mathcomp.analysis  $(find coq-mathcomp-analysis.*/theories -name \*.v) \
    -R coq-mathcomp-bigenough.* mathcomp.bigenough  $(find coq-mathcomp-bigenough.* -name \*.v) \
    -R coq-mathcomp-field.* mathcomp  $(find coq-mathcomp-field.*/mathcomp/field -name \*.v) \
    -R coq-mathcomp-finmap.* mathcomp.finmap  $(find coq-mathcomp-finmap.* -name \*.v) \
    -R coq-mathcomp-fingroup.* mathcomp  $(find coq-mathcomp-fingroup.*/mathcomp/fingroup -name \*.v) \
    -R coq-mathcomp-multinomials.*/src SsrMultinomials  $(find coq-mathcomp-multinomials.*/src -name \*.v) \
    -R coq-mathcomp-solvable.* mathcomp  $(find coq-mathcomp-solvable.*/mathcomp/solvable -name \*.v) \
    -R coq-mathcomp-ssreflect.* mathcomp  $(find coq-mathcomp-ssreflect.*/mathcomp/ssreflect -name \*.v) \
    -R ../../lib/coq/theories Coq $(find  ../../lib/coq/theories -name \*.v) \
    -R ../../lib/coq/plugins Coq $(find  ../../lib/coq/plugins -name \*.v) \
     ; tar czf doc.tgz -C $DOC/.. doc; cp doc.tgz $DOC
     
# dont know how to integrate the docs from compcert in a nice way...
#     -R coq-compcert.* compcert  $(find coq-compcert.* -name \*.v)\