10 files changed, 68 insertions, 5 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 7b3e2703b8..64936cd236 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..c18e556da8 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -200,6 +200,13 @@
 : "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
 
 ########################################################################
+# bbv
+########################################################################
+: "${bbv_CI_REF:=master}"
+: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}"
+: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}"
+
+########################################################################
 # bedrock2
 ########################################################################
 : "${bedrock2_CI_REF:=tested}"
@@ -330,3 +337,10 @@
 : "${perennial_CI_REF:=master}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh
new file mode 100755
index 0000000000..6892cea3e4
--- /dev/null
+++ b/dev/ci/ci-bbv.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download bbv
+
+( cd "${CI_BUILD_DIR}/bbv" && make && make install )
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index 756f54dfbd..a21310cbd5 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download bignums
 
-( cd "${CI_BUILD_DIR}/bignums" && make && make install)
+( cd "${CI_BUILD_DIR}/bignums" && make && make install && cd tests && make)
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e56e4d38ea..0c8733c75a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-19-V29"
+# CACHEKEY: "bionic_coq-V2020-03-27-V12"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.09.1" \
+ENV COMPILER_EDGE="4.10.0" \
     BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
new file mode 100644
index 0000000000..8a734feada
--- /dev/null
+++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then
+
+    quickchick_CI_REF=master+adapting-numTok-new-api-pr11703
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
new file mode 100644
index 0000000000..6928925e54
--- /dev/null
+++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then
+
+    equations_CI_REF=proof+more_naming_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    rewriter_CI_REF=proof+more_naming_unif
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+    elpi_CI_REF=proof+more_naming_unif
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+    metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi