Merge PR coq#18238: ci: build and reuse bedrock2 version from fiat-cr…

…ypto Reviewed-by: SkySkimmer Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
herbelin · Nov 1, 2023 · 2a7bea4 · 2a7bea4
2 parents 5da7f39 + 7b04450
commit 2a7bea4
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 6 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -656,6 +656,7 @@ library:ci-fiat_crypto:
   needs:
   - build:edge+flambda
   - library:ci-coqprime
+  - library:ci-bedrock2
   - plugin:ci-bignums
   - plugin:ci-rewriter
   timeout: 3h

diff --git a/Makefile.ci b/Makefile.ci
@@ -122,7 +122,7 @@ ci-coq_library_undecidability: ci-metacoq
 
 ci-mtac2: ci-unicoq
 
-ci-fiat_crypto: ci-coqprime ci-rewriter
+ci-fiat_crypto: ci-coqprime ci-rewriter ci-bedrock2
 ci-fiat_crypto_ocaml: ci-fiat_crypto
 
 ci-fourcolor: ci-mathcomp

diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
@@ -6,12 +6,12 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 WITH_SUBMODULES=1
-git_download bedrock2
+git_download fiat_crypto
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 export COQEXTRAFLAGS='-native-compiler no'
-( cd "${CI_BUILD_DIR}/bedrock2"
+( cd "${CI_BUILD_DIR}/fiat_crypto/rupicola/bedrock2"
   COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make
   make install
 )
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
@@ -5,9 +5,6 @@ set -e
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-WITH_SUBMODULES=1
-git_download fiat_crypto
-
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 # We need a larger stack size to not overflow ocamlopt+flambda when
@@ -20,6 +17,7 @@ stacksize=32768
 # version of other developments
 make_args=(EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1)
 
+export COQEXTRAFLAGS='-native-compiler no' # following bedrock2
 ( cd "${CI_BUILD_DIR}/fiat_crypto"
   ulimit -s $stacksize
   make "${make_args[@]}" pre-standalone-extracted printlite lite ||