14 files changed, 62 insertions, 23 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 801e29ac95..f5ca6c495f 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -171,7 +171,7 @@ loaded by subsequent jobs.
 
 **IMPORTANT**: When updating Coq's CI docker image, you must modify
 the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml)
-and [`Dockerfile`](docker/bionic_coq/Dockerfile)
+(see comment near it for details).
 
 The Docker building job reuses the uploaded image if it is available,
 but if you wish to save more time you can skip the job by setting
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 75d9efaadc..18fdd83218 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -306,7 +306,7 @@
 # menhirlib
 ########################################################################
 # Note: menhirlib is now in subfolder coq-menhirlib of menhir
-: "${menhirlib_CI_REF:=master}"
+: "${menhirlib_CI_REF:=20201122}"
 : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}"
 : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
 
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b85261d7fc..1a4ebc0e90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -19,20 +19,20 @@ then
 elif [ -d "$PWD/_build/install/default/" ];
 then
     # Dune build
-    export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH"
+    export OCAMLPATH="$PWD/_build/install/default/lib/:$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_build/install/default/bin"
     export COQLIB="$PWD/_build/install/default/lib/coq"
     CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
     export CI_BRANCH
 else
     # We assume we are in `-profile devel` build, thus `-local` is set
-    export OCAMLPATH="$PWD:$OCAMLPATH"
+    export OCAMLPATH="$PWD:$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/bin"
     CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
     export CI_BRANCH
 fi
 
-export PATH="$COQBIN:$PATH"
+export PATH="$COQBIN:$PWD/_install_ci/bin:$PATH"
 
 # Coq's tools need an ending slash :S, we should fix them.
 export COQBIN="$COQBIN/"
@@ -42,6 +42,9 @@ ls -l "$COQBIN"
 # Where we download and build external developments
 CI_BUILD_DIR="$PWD/_build_ci"
 
+# Where we install external binaries and ocaml libraries
+CI_INSTALL_DIR="$PWD/_install_ci"
+
 ls -l "$CI_BUILD_DIR" || true
 
 declare -A overlays
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 6b09726606..3c8d65f5c1 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -7,6 +7,6 @@ git_download compcert
 
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
-      ./configure -ignore-coq-version x86_32-linux && \
+      ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq && \
       make && \
       make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index ffe92dcecf..777d36a6d7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-install_ssreflect
-
 git_download coquelicot
 
-( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/coquelicot" && ( if [ ! -x ./configure ]; then autoreconf -i -s && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index a3a704091b..cb6c3e6452 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download flocq
 
-( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-fourcolor.sh b/dev/ci/ci-fourcolor.sh
new file mode 100755
index 0000000000..72a1567398
--- /dev/null
+++ b/dev/ci/ci-fourcolor.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download fourcolor
+
+( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh
new file mode 100755
index 0000000000..fe7b3f9fbe
--- /dev/null
+++ b/dev/ci/ci-interval.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download interval
+
+export COQEXTRAFLAGS='-native-compiler no'
+( cd "${CI_BUILD_DIR}/interval" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh
index b1aa56ec4e..f170b35327 100755
--- a/dev/ci/ci-mathcomp.sh
+++ b/dev/ci/ci-mathcomp.sh
@@ -7,11 +7,3 @@ ci_dir="$(dirname "$0")"
 git_download mathcomp
 
 ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install )
-
-git_download fourcolor
-
-( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
-
-git_download oddorder
-
-( cd "${CI_BUILD_DIR}/oddorder" && make )
diff --git a/dev/ci/ci-menhir.sh b/dev/ci/ci-menhir.sh
new file mode 100755
index 0000000000..5ad78383d8
--- /dev/null
+++ b/dev/ci/ci-menhir.sh
@@ -0,0 +1,8 @@
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download menhirlib
+
+( cd "${CI_BUILD_DIR}/menhirlib" && dune build @install -p menhirLib,menhirSdk,menhir && dune install -p menhirLib,menhirSdk,menhir menhir menhirSdk menhirLib --prefix=${CI_INSTALL_DIR} )
+
+( cd "${CI_BUILD_DIR}/menhirlib" && make -C coq-menhirlib && make -C coq-menhirlib install )
diff --git a/dev/ci/ci-oddorder.sh b/dev/ci/ci-oddorder.sh
new file mode 100755
index 0000000000..b2da32ad61
--- /dev/null
+++ b/dev/ci/ci-oddorder.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download oddorder
+
+( cd "${CI_BUILD_DIR}/oddorder" && make && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index c17ec502e7..96d96328f8 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,5 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-10-12-V89"
-# ^^ Update when modifying this file.
+# Update CACHEKEY in the .gitlab-ci.yml when modifying this file.
 
 FROM ubuntu:bionic
 LABEL maintainer="e@x80.org"
@@ -42,8 +41,8 @@ ENV COMPILER="4.05.0"
 
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
-    CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.11.4"
+    CI_OPAM="ocamlgraph.1.8.8" \
+    BASE_ONLY_OPAM="elpi.1.12.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
@@ -62,7 +61,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.11.1" \
-    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0"
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
new file mode 100644
index 0000000000..0bf806085e
--- /dev/null
+++ b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then
+
+    overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs
+
+    overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs
+
+    overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs
+fi
diff --git a/dev/ci/user-overlays/13481-elpi-1.12.sh b/dev/ci/user-overlays/13481-elpi-1.12.sh
new file mode 100644
index 0000000000..a6be2e3a1a
--- /dev/null
+++ b/dev/ci/user-overlays/13481-elpi-1.12.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13481" ] || [ "$CI_BRANCH" = "elpi-1.12" ]; then
+
+    elpi_CI_REF=coq-master+elpi.1.12
+    elpi_hb_CI_REF=coq-master+coq-elpi-1.7.0+elpi-1.12
+
+fi