aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile5
-rw-r--r--dev/ci/user-overlays/09439-sep-variance.sh14
2 files changed, 15 insertions, 4 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 4cd7faf757..43278c37b1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-01-28-V1"
+# CACHEKEY: "bionic_coq-V2019-02-17-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \
COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
BASE_OPAM_EDGE="dune-release.1.1.0"
-RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
- opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE
-
# EDGE+flambda switch, we install CI_OPAM as to be able to use
# `ci-template-flambda` with everything.
RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh
new file mode 100644
index 0000000000..cca85a2f68
--- /dev/null
+++ b/dev/ci/user-overlays/09439-sep-variance.sh
@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then
+ elpi_CI_REF=sep-variance
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+ equations_CI_REF=sep-variance
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ mtac2_CI_REF=sep-variance
+ mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+ paramcoq_CI_REF=sep-variance
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+fi