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)

1 files changed, 14 insertions, 7 deletions

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