10 files changed, 98 insertions, 10 deletions
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 01769aeddb..06b617d4c1 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is
 to give merge permissions to someone from the Coq team as to help with
 these kind of merges.
 
+### OCaml and plugin-specific considerations
+
+Developments that link against Coq's OCaml API [most of them are known
+as "plugins"] do have some special requirements:
+
+- Coq's OCaml API is not stable. We hope to improve this in the future
+  but as of today you should expect to have to merge a fair amount of
+  "overlays", usually in the form of Pull Requests from Coq developers
+  in order to keep your plugin compatible with Coq master.
+
+  In order to alleviate the load, you can delegate the merging of such
+  compatibility pull requests to Coq developers themselves, by
+  granting access to the plugin repository or by using `bots` such as
+  [Bors](https://github.com/apps/bors) that allow for automatic
+  management of Pull Requests.
+
+- Plugins in the CI should compile with the OCaml flags that Coq
+  uses. In particular, warnings that are considered fatal by the Coq
+  developers _must_ be also fatal for plugin CI code.
+
 ### Add your development by submitting a pull request
 
 Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 0c89809ee9..4f5988c59c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -254,7 +254,7 @@
 : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}"
 
 ########################################################################
-# relation-algebra
+# relation_algebra
 ########################################################################
 : "${relation_algebra_CI_REF:=master}"
 : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b4d2a9ca4e..7aa265cf90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -108,10 +108,9 @@ install_ssreflect()
 
   git_download mathcomp
 
-  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
-    make Makefile.coq && \
-    make -f Makefile.coq ssreflect/all_ssreflect.vo && \
-    make -f Makefile.coq install )
+  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \
+    make && \
+    make install )
 
 }
 
@@ -123,8 +122,11 @@ install_ssralg()
   git_download mathcomp
 
   ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
-    make Makefile.coq && \
-    make -f Makefile.coq algebra/all_algebra.vo && \
-    make -f Makefile.coq install )
+    make -C ssreflect && \
+    make -C ssreflect install && \
+    make -C fingroup && \
+    make -C fingroup install && \
+    make -C algebra && \
+    make -C algebra install )
 
 }
diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh
index 84bed5bdfe..84bed5bdfe 100755
--- a/dev/ci/ci-relation-algebra.sh
+++ b/dev/ci/ci-relation_algebra.sh
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e553cbed1b..8eebb3af64 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-12-V1"
+# CACHEKEY: "bionic_coq-V2019-04-20-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
-    CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
new file mode 100644
index 0000000000..67f6f8610a
--- /dev/null
+++ b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then
+
+    ltac2_CI_REF=master-parsing-decimal
+    ltac2_CI_GITURL=https://github.com/proux01/ltac2
+
+    quickchick_CI_REF=master-parsing-decimal
+    quickchick_CI_GITURL=https://github.com/proux01/QuickChick
+
+    Corn_CI_REF=master-parsing-decimal
+    Corn_CI_GITURL=https://github.com/proux01/corn
+
+    HoTT_CI_REF=master-parsing-decimal
+    HoTT_CI_GITURL=https://github.com/proux01/HoTT
+
+    stdlib2_CI_REF=master-parsing-decimal
+    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+fi
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
new file mode 100644
index 0000000000..12be1b676a
--- /dev/null
+++ b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
+
+    HoTT_CI_REF=rm-hardwired-hint-db
+    HoTT_CI_GITURL=https://github.com/vbgl/HoTT
+
+    ltac2_CI_REF=rm-hardwired-hint-db
+    ltac2_CI_GITURL=https://github.com/vbgl/ltac2
+
+    UniMath_CI_REF=rm-hardwired-hint-db
+    UniMath_CI_GITURL=https://github.com/vbgl/UniMath
+
+fi
diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
new file mode 100644
index 0000000000..1e1d36d54a
--- /dev/null
+++ b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then
+
+    elpi_CI_REF=recarg-cleanup
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    quickchick_CI_REF=recarg-cleanup
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
new file mode 100644
index 0000000000..01d3068591
--- /dev/null
+++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then
+
+    elpi_CI_REF=pretyping-rm-global
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    coqhammer_CI_REF=pretyping-rm-global
+    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+    equations_CI_REF=pretyping-rm-global
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+    ltac2_CI_REF=pretyping-rm-global
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    paramcoq_CI_REF=pretyping-rm-global
+    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+    mtac2_CI_REF=pretyping-rm-global
+    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
new file mode 100644
index 0000000000..9a6e25d893
--- /dev/null
+++ b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then
+
+    elpi_CI_REF=overlay-elpi1.2-coq-master
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi