aboutsummaryrefslogtreecommitdiff
path: root/Dockerfile
diff options
context:
space:
mode:
Diffstat (limited to 'Dockerfile')
-rw-r--r--Dockerfile17
1 files changed, 6 insertions, 11 deletions
diff --git a/Dockerfile b/Dockerfile
index eddbb0f..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 \
@@ -29,10 +23,11 @@ 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
+ENV COMPILER=""
ENV MATHCOMP_VERSION="dev"
ENV MATHCOMP_PACKAGE="coq-mathcomp-character"