From 25630e23f09cd9c1b4b8bb9dbb2b3172111a92f1 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Thu, 20 Dec 2018 01:36:37 +0100
Subject: Add Dockerfile to build mathcomp using its opam files

---
 Dockerfile | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 Dockerfile

(limited to 'Dockerfile')

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"]
-- 
cgit v1.2.3


From 1c14614a2328d1854fd584d8d7ca54121faec0ee Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Thu, 20 Dec 2018 16:07:41 +0100
Subject: Improve the mathcomp-dev Dockerfile (using Docker's multi-stage
 build)

* Install coq-mathcomp-character in only 1 switch (cf. the build-arg $compiler)
* Remove the other switch
* Base the final image on coqorg/base:bare (which has no OCaml compiler layers)
---
 Dockerfile | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

(limited to 'Dockerfile')

diff --git a/Dockerfile b/Dockerfile
index 58f2d12..74ee396 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,8 +1,5 @@
 ARG coq_image="coqorg/coq:dev"
-FROM ${coq_image}
-
-ENV MATHCOMP_VERSION="dev"
-ENV MATHCOMP_PACKAGE="coq-mathcomp-character"
+FROM ${coq_image} as builder
 
 WORKDIR /home/coq/mathcomp
 
@@ -14,10 +11,12 @@ ARG compiler="base"
 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} \
+  && opam_switch=\"${switch_table[${compiler}]}\" \
+  && [ -n \"opam_switch\" ] \
+  && opam switch set ${opam_switch} \
   && eval $(opam env) \
+  && unset \"switch_table[${compiler}]\" \
+  && for sw in \"${switch_table[@]}\"; do if [ -n \"$sw\" ]; then opam switch remove -y \"${sw}\"; fi; done \
   && 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 \
@@ -31,3 +30,11 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam pin add -n -k path coq-mathcomp-character . \
   && opam install -y -v -j ${NJOBS} coq-mathcomp-character \
   && opam clean -a -c -s --logs"]
+
+FROM coqorg/base:bare
+
+ENV MATHCOMP_VERSION="dev"
+ENV MATHCOMP_PACKAGE="coq-mathcomp-character"
+
+COPY --from=builder --chown=coq:coq /home/coq/.opam /home/coq/.opam
+COPY --from=builder --chown=coq:coq /home/coq/.profile /home/coq/.profile
-- 
cgit v1.2.3