aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-07-10 13:47:56 +0200
committerGaëtan Gilbert2020-07-10 13:47:56 +0200
commit5a6afa0acfdf575b818d7d88588cb2fad5b813b8 (patch)
tree66000683458d444d8e9194664ddd761dd90fa8a9
parentf2dc2f5fc8c745c69c0161a91063b11838fb684b (diff)
Fix fiat_crypto(_ocaml) needs/dependencies
It seems gitlab has issues with missing transitive dependencies, for instance in https://gitlab.com/coq/coq/-/pipelines/164834444 rewriter failed (missing overlay), fiat_crypto was skipped and fiat_crypto_ocaml was incorrectly started and so failed. May also fix (intermittent?) issue where it doesn't download the rewriter or bignum artifact and gets incompatible ocaml when compiling.
-rw-r--r--.gitlab-ci.yml7
1 files changed, 7 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 819ad8a214..3b95800f0d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -751,6 +751,7 @@ library:ci-fiat_crypto:
dependencies:
- build:edge+flambda
- library:ci-coqprime
+ - plugin:ci-bignums
- plugin:ci-rewriter
library:ci-fiat_crypto_legacy:
@@ -765,9 +766,15 @@ library:ci-fiat_crypto_ocaml:
stage: stage-5
needs:
- build:edge+flambda
+ - library:ci-coqprime
+ - plugin:ci-bignums
+ - plugin:ci-rewriter
- library:ci-fiat_crypto
dependencies:
- build:edge+flambda
+ - library:ci-coqprime
+ - plugin:ci-bignums
+ - plugin:ci-rewriter
- library:ci-fiat_crypto
library:ci-flocq: