diff options
| -rw-r--r-- | Dockerfile | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..58f2d12 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,33 @@ +ARG coq_image="coqorg/coq:dev" +FROM ${coq_image} + +ENV MATHCOMP_VERSION="dev" +ENV MATHCOMP_PACKAGE="coq-mathcomp-character" + +WORKDIR /home/coq/mathcomp + +COPY . . + +ARG compiler="base" +# other possible value: "edge" + +RUN ["/bin/bash", "--login", "-c", "set -x \ + && declare -A switch_table \ + && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \ + && compiler=\"${switch_table[${compiler}]}\" \ + && [ -n \"$compiler\" ] \ + && opam switch set ${compiler} \ + && eval $(opam env) \ + && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \ + && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \ + && opam update -y \ + && opam config list && opam repo list && opam list && coqc --version \ + && sudo chown -R coq:coq /home/coq/mathcomp \ + && opam pin add -n -k path coq-mathcomp-ssreflect . \ + && opam pin add -n -k path coq-mathcomp-fingroup . \ + && opam pin add -n -k path coq-mathcomp-algebra . \ + && opam pin add -n -k path coq-mathcomp-solvable . \ + && opam pin add -n -k path coq-mathcomp-field . \ + && opam pin add -n -k path coq-mathcomp-character . \ + && opam install -y -v -j ${NJOBS} coq-mathcomp-character \ + && opam clean -a -c -s --logs"] |