[ci] Split fiat-crypto into non-OCaml and OCaml

Note that this should reduce the overall build time of fiat-crypto
related targets by about 10--20 minutes, as I've removed the heaviest
jobs (about 25--30 minutes in serial) from the OCaml target.

I'd like to keep the OCaml target around just to make sure that Coq
doesn't introduce a change to extraction that breaks compilation of
extracted OCaml code.  See https://github.com/ocaml/ocaml/issues/7826
for the issue tracking performance of compiling the extracted OCaml
code (and perhaps there should be another issue opened on the OCaml bug
tracker about flambda on the fiat-crypto extracted files?)

Alternative to #12405
Closes #12405
Fixes #12400

4 files changed, 31 insertions, 6 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 87101ecae7..e8244fafc8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -6,6 +6,7 @@ stages:
   - stage-2 # Only dependencies in stage 1
   - stage-3 # Only dependencies in stage 1 and 2
   - stage-4 # Only dependencies in stage 1, 2 and 3
+  - stage-5 # Only dependencies in stage 1, 2, 3, and 4
   - deploy
 
 # When a job has no dependencies, it goes to stage 1.  Otherwise, we
@@ -704,12 +705,13 @@ library:ci-engine_bench:
 library:ci-fcsl_pcm:
   extends: .ci-template
 
-# We cannot use flambda due to
-# https://github.com/ocaml/ocaml/issues/7842, see
-# https://github.com/coq/coq/pull/11916#issuecomment-609977375
 library:ci-fiat_crypto:
-  extends: .ci-template
+  extends: .ci-template-flambda
   stage: stage-4
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
   needs:
   - build:edge+flambda
   - library:ci-coqprime
@@ -720,6 +722,19 @@ library:ci-fiat_crypto:
   - library:ci-coqprime
   - plugin:ci-rewriter
 
+# We cannot use flambda due to
+# https://github.com/ocaml/ocaml/issues/7842, see
+# https://github.com/coq/coq/pull/11916#issuecomment-609977375
+library:ci-fiat_crypto_ocaml:
+  extends: .ci-template
+  stage: stage-5
+  needs:
+  - build:edge+flambda
+  - library:ci-fiat_crypto
+  dependencies:
+  - build:edge+flambda
+  - library:ci-fiat_crypto
+
 library:ci-flocq:
   extends: .ci-template-flambda
   artifacts:
diff --git a/Makefile.ci b/Makefile.ci
index 9b7008f765..9231fa6fed 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,6 +28,7 @@ CI_TARGETS= \
     ci-equations \
     ci-fcsl_pcm \
     ci-fiat_crypto \
+    ci-fiat_crypto_ocaml \
     ci-fiat_parsers \
     ci-flocq \
     ci-geocoq \
@@ -72,6 +73,7 @@ ci-corn: ci-math_classes
 ci-mtac2: ci-unicoq
 
 ci-fiat_crypto: ci-coqprime ci-rewriter
+ci-fiat_crypto_ocaml: ci-fiat_crypto
 
 ci-simple_io: ci-ext_lib
 ci-quickchick: ci-ext_lib ci-simple_io
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 811fefda35..3ecdb32a51 100755
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -15,8 +15,8 @@ fiat_crypto_CI_STACKSIZE=32768
 # 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"
+fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite"
+fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
         ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh
new file mode 100755
index 0000000000..20d3deb14f
--- /dev/null
+++ b/dev/ci/ci-fiat_crypto_ocaml.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
+
+( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files )