aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-13 15:16:04 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-13 17:05:13 +0100
commiteced3ec17e156a6cf5c96822bc675b353a9b0168 (patch)
tree7aebf4a0f26a12e84c7fcb504e6c41d99c56afd2 /.circleci
parentf10d9fefdaf694253495c1ecf2e57ce5099b9375 (diff)
Circle CI: uses dependencies between external developments.
Diffstat (limited to '.circleci')
-rw-r--r--.circleci/config.yml30
1 files changed, 27 insertions, 3 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 718bd6b5e..437f5cd2e 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -220,7 +220,11 @@ before_script: &before_script
echo 'start:coq.test'
make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB}
echo 'end:coq.test'
- environment: &ci-template-vars
+ - persist_to_workspace:
+ root: &workspace ~/
+ paths:
+ - coq/
+environment: &ci-template-vars
<<: *envvars
EXTRA_PACKAGES: *timing-packages
@@ -338,6 +342,12 @@ jobs:
<<: *ci-template-vars
EXTRA_PACKAGES: "time python autoconf automake"
+ ci-math-classes:
+ <<: *ci-template
+
+ ci-corn:
+ <<: *ci-template
+
ci-formal-topology:
<<: *ci-template
@@ -382,7 +392,10 @@ workflows:
- documentation: *req-main
- ci-bignums: *req-main
- - ci-color: *req-main
+ - ci-color:
+ requires:
+ - build
+ - ci-bignums
- ci-compcert: *req-main
- ci-coq-dpdgraph: *req-main
- ci-coquelicot: *req-main
@@ -391,7 +404,18 @@ workflows:
- ci-fiat-crypto: *req-main
- ci-fiat-parsers: *req-main
- ci-flocq: *req-main
- - ci-formal-topology: *req-main
+ - ci-math-classes:
+ requires:
+ - build
+ - ci-bignums
+ - ci-corn:
+ requires:
+ - build
+ - ci-math-classes
+ - ci-formal-topology:
+ requires:
+ - build
+ - ci-corn
- ci-hott: *req-main
- ci-iris-lambda-rust: *req-main
- ci-ltac2: *req-main