10 files changed, 94 insertions, 10 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 87122e0fb5..608cc127a0 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -209,7 +209,7 @@
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_REF:=master}"
+: "${bedrock2_CI_REF:=tested}"
 : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
 : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
 
@@ -256,6 +256,13 @@
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
+# reduction-effects
+########################################################################
+: "${reduction_effects_CI_REF:=master}"
+: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
+: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+
+########################################################################
 # menhirlib
 ########################################################################
 : "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 2af4b58201..9ce5da9f50 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -6,8 +6,8 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_crypto_legacy
 
-fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
-fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded"
+fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   ./etc/ci/remove_autogenerated.sh && \
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
 # We need a larger stack size to not overflow ocamlopt+flambda when
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
 
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
-        ulimit -s 32768 && \
+        ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh
new file mode 100755
index 0000000000..6b6de3fa2f
--- /dev/null
+++ b/dev/ci/ci-reduction_effects.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download reduction_effects
+
+( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install)
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 2b1d2298f2..b9d6215e60 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+
+# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
+# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
 
 mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
 
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index a9cc91170f..f08a08531f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; })
 
 let unicoq = callPackage ./unicoq { inherit coq; }; in
 
+let StructTact = coqPackages.StructTact.overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master";
+  }); in
+
+let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master";
+  }); in
+
+let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/uwplse/verdi/tarball/master";
+  }); in
+
 let callPackage = newScope { inherit coq
   bignums coq-ext-lib coqprime corn iris math-classes
-  mathcomp simple-io ssreflect stdpp unicoq;
+  mathcomp simple-io ssreflect stdpp unicoq Verdi;
 }; in
 
 # Environments for building CI libraries with this Coq
@@ -89,6 +103,7 @@ let projects = {
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
   quickchick = callPackage ./quickchick.nix {};
+  verdi-raft = callPackage ./verdi-raft.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 0f0ee91387..1105fba7a6 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
-{ coqprime }:
+{ ocamlPackages }:
 {
-  coqBuildInputs = [ coqprime ];
+  buildInputs = with ocamlPackages; [ ocaml findlib ];
   configure = "git submodule update --init --recursive && ulimit -s 32768";
-  make = "make new-pipeline c-files";
+  make = "make c-files printlite lite && make -j 1 coq";
 }
diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix
new file mode 100644
index 0000000000..6a98f4ef47
--- /dev/null
+++ b/dev/ci/nix/verdi-raft.nix
@@ -0,0 +1,5 @@
+{ Verdi }:
+{
+  coqBuildInputs = [ Verdi ];
+  configure = "./configure";
+}
diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
new file mode 100644
index 0000000000..f41271804a
--- /dev/null
+++ b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then
+
+    unicoq_CI_REF=rm-global-uses-evd
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+    equations_CI_REF=rm-global-uses-evd
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
new file mode 100644
index 0000000000..a125337dd9
--- /dev/null
+++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
@@ -0,0 +1,33 @@
+if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then
+
+    mathcomp_CI_REF=non_maximal_implicit
+    mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
+
+    oddorder_CI_REF=non_maximal_implicit
+    oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
+
+    stdlib2_CI_REF=non_maximal_implicit
+    stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
+
+    coq_dpdgraph_CI_REF=non_maximal_implicit
+    coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
+
+    vst_CI_REF=non_maximal_implicit
+    vst_CI_GITURL=https://github.com/SimonBoulier/VST
+
+    equations_CI_REF=non_maximal_implicit
+    equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
+
+    mtac2_CI_REF=non_maximal_implicit
+    mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
+
+    relation_algebra_CI_REF=non_maximal_implicit
+    relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
+
+    fiat_parsers_CI_REF=non_maximal_implicit
+    fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
+
+    Corn_CI_REF=non_maximal_implicit
+    Corn_CI_GITURL=https://github.com/SimonBoulier/corn
+
+fi