7 files changed, 76 insertions, 4 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 493397adee..6afe3bd0a8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -562,7 +562,11 @@ library:ci-argosy:
   extends: .ci-template
 
 library:ci-bedrock2:
-  extends: .ci-template
+  extends: .ci-template-flambda
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
 
 library:ci-color:
   extends: .ci-template-flambda
@@ -577,6 +581,19 @@ library:ci-color:
 library:ci-compcert:
   extends: .ci-template-flambda
 
+library:ci-coqprime:
+  stage: stage-3
+  extends: .ci-template-flambda
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
+  needs:
+  - build:edge+flambda
+  - plugin:ci-bignums
+  dependencies:
+  - plugin:ci-bignums
+
 library:ci-coquelicot:
   extends: .ci-template
 
@@ -588,6 +605,17 @@ library:ci-fcsl-pcm:
 
 library:ci-fiat-crypto:
   extends: .ci-template-flambda
+  stage: stage-4
+  needs:
+  - build:edge+flambda
+  - library:ci-bedrock2
+  - library:ci-coqprime
+  - plugin:ci-bignums
+  - plugin:ci-rewriter
+  dependencies:
+  - library:ci-bedrock2
+  - library:ci-coqprime
+  - plugin:ci-rewriter
 
 library:ci-fiat-crypto-legacy:
   extends: .ci-template-flambda
@@ -699,3 +727,10 @@ plugin:ci-quickchick:
 
 plugin:ci-relation_algebra:
   extends: .ci-template
+
+plugin:ci-rewriter:
+  extends: .ci-template-flambda
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
diff --git a/Makefile.ci b/Makefile.ci
index e9f7fa2db5..8315c16c64 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -19,6 +19,7 @@ CI_TARGETS= \
     ci-coquelicot \
     ci-corn \
     ci-cross-crypto \
+    ci-coqprime \
     ci-elpi \
     ci-ext-lib \
     ci-equations \
@@ -38,6 +39,7 @@ CI_TARGETS= \
     ci-perennial \
     ci-quickchick \
     ci-relation_algebra \
+    ci-rewriter \
     ci-sf \
     ci-simple-io \
     ci-stdlib2 \
@@ -56,10 +58,14 @@ ci-all: $(CI_TARGETS)
 
 ci-color: ci-bignums
 
+ci-coqprime: ci-bignums
+
 ci-math-classes: ci-bignums
 
 ci-corn: ci-math-classes
 
+ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter
+
 ci-simple-io: ci-ext-lib
 ci-quickchick: ci-ext-lib ci-simple-io
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5139113083..de21b17f9f 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -144,6 +144,13 @@
 : "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}"
 
 ########################################################################
+# rewriter
+########################################################################
+: "${rewriter_CI_REF:=master}"
+: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}"
+: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}"
+
+########################################################################
 # fiat_parsers
 ########################################################################
 : "${fiat_parsers_CI_REF:=master}"
@@ -200,6 +207,13 @@
 : "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}"
 
 ########################################################################
+# coqprime
+########################################################################
+: "${coqprime_CI_REF:=master}"
+: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}"
+: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
+
+########################################################################
 # bedrock2
 ########################################################################
 : "${bedrock2_CI_REF:=master}"
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 2ac78d3c2b..8570c34194 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install )
diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh
new file mode 100755
index 0000000000..a4fd296896
--- /dev/null
+++ b/dev/ci/ci-coqprime.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coqprime
+
+( cd "${CI_BUILD_DIR}/coqprime" && make && make install)
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index eec9d50ae4..000c418137 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -10,8 +10,9 @@ git_download fiat_crypto
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
 
-fiat_crypto_CI_TARGETS1="standalone-ocaml c-files rust-files printlite lite"
-fiat_crypto_CI_TARGETS2="all"
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=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 && \
diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh
new file mode 100755
index 0000000000..235482ffeb
--- /dev/null
+++ b/dev/ci/ci-rewriter.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download rewriter
+
+( cd "${CI_BUILD_DIR}/rewriter" && make && make install)