diff options
| author | Erik Martin-Dorel | 2018-12-20 01:36:37 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2018-12-21 12:17:07 +0100 |
| commit | 25630e23f09cd9c1b4b8bb9dbb2b3172111a92f1 (patch) | |
| tree | dfc6efbbbad3a68e655876e4b036c1d421467d0d /Dockerfile | |
| parent | 036e10fc07ca816e9c0587e2bde55a2928c37388 (diff) | |
Add Dockerfile to build mathcomp using its opam files
Diffstat (limited to 'Dockerfile')
| -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"] |