From f427613138c0ed6ba7c64d12140ed55c2c5bd310 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 30 May 2020 21:52:26 -0400
Subject: [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
---
 dev/ci/ci-fiat_crypto.sh       | 4 ++--
 dev/ci/ci-fiat_crypto_ocaml.sh | 8 ++++++++
 2 files changed, 10 insertions(+), 2 deletions(-)
 create mode 100755 dev/ci/ci-fiat_crypto_ocaml.sh

(limited to 'dev/ci')

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 )
-- 
cgit v1.2.3