13 files changed, 61 insertions, 21 deletions
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..85107780f1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-10-12-V89"
+# CACHEKEY: "bionic_coq-V2020-11-26-V92"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -42,8 +42,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 +62,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