From a7f4eb76935157112aa844b6c5ac29a36898235f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 17 Jan 2020 16:14:38 +0100
Subject: Revert "Don't run "opam clean -c" to workaround ocaml/opam#3828"

This reverts commit a03e0cb0ff40afabcaccba7f764076355ca82962.
---
 Dockerfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Dockerfile')

diff --git a/Dockerfile b/Dockerfile
index eddbb0f..74ee396 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -29,7 +29,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && 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 -s --logs"]
+  && opam clean -a -c -s --logs"]
 
 FROM coqorg/base:bare
 
-- 
cgit v1.2.3


From 563f395e1a41caf4978fe9881250ec68796e36a0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 8 Mar 2020 15:22:33 +0100
Subject: refactor: Simplify the Dockerfiles

* the CLI option --build-arg=compiler="${OPAM_SWITCH}" is now useless
  (it had been introduced to be able to compile Coq versions < 8.7,
  while mathcomp-dev now requires Coq 8.7+)

* the "coqorg/base:bare" image now contains the two environment vars
  COMPILER and COMPILER_EDGE => clear COMPILER="" in mathcomp-dev's
  Dockerfile multi-stage build.
---
 Dockerfile | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

(limited to 'Dockerfile')

diff --git a/Dockerfile b/Dockerfile
index 74ee396..65b7b30 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -5,18 +5,12 @@ 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}\" ) \
-  && opam_switch=\"${switch_table[${compiler}]}\" \
-  && [ -n \"opam_switch\" ] \
-  && opam switch set ${opam_switch} \
+  && [ -n \"${COMPILER_EDGE}\" ] \
+  && opam switch set \"${COMPILER_EDGE}\" \
   && eval $(opam env) \
-  && unset \"switch_table[${compiler}]\" \
-  && for sw in \"${switch_table[@]}\"; do if [ -n \"$sw\" ]; then opam switch remove -y \"${sw}\"; fi; done \
+  && [ -n \"${COMPILER}\" ] \
+  && opam switch remove -y \"${COMPILER}\" \
   && 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 \
@@ -33,6 +27,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
 
 FROM coqorg/base:bare
 
+ENV COMPILER=""
 ENV MATHCOMP_VERSION="dev"
 ENV MATHCOMP_PACKAGE="coq-mathcomp-character"
 
-- 
cgit v1.2.3