diff options
| -rw-r--r-- | .gitlab-ci.yml | 88 |
1 files changed, 45 insertions, 43 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 108ecb5a04..5bcf94eda8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -174,20 +174,17 @@ after_script: script: - set -e - echo 'start:coq.test' - - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET} + - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" - echo 'end:coq.test' - set +e dependencies: - build:base - variables: &ci-template-vars - TEST_TARGET: "$CI_JOB_NAME" .ci-template-flambda: &ci-template-flambda <<: *ci-template dependencies: - build:edge+flambda variables: - <<: *ci-template-vars OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" @@ -445,93 +442,98 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" -ci-aac_tactics: - <<: *ci-template +# Libraries are by convention the projects that depend on Coq +# but not on its ML API -ci-bedrock2: +library:ci-bedrock2: <<: *ci-template allow_failure: true -ci-bignums: - <<: *ci-template - -ci-color: +library:ci-color: <<: *ci-template-flambda -ci-compcert: +library:ci-compcert: <<: *ci-template-flambda -ci-coq_dpdgraph: +library:ci-coquelicot: <<: *ci-template -ci-coquelicot: +library:ci-cross-crypto: <<: *ci-template -ci-cross-crypto: +library:ci-fcsl-pcm: <<: *ci-template -ci-elpi: - <<: *ci-template +library:ci-fiat-crypto: + <<: *ci-template-flambda -ci-equations: - <<: *ci-template +library:ci-fiat-crypto-legacy: + <<: *ci-template-flambda -ci-fcsl-pcm: +library:ci-flocq: <<: *ci-template -ci-fiat-crypto: +library:ci-formal-topology: <<: *ci-template-flambda -ci-fiat-crypto-legacy: +library:ci-geocoq: <<: *ci-template-flambda -ci-fiat-parsers: +library:ci-hott: <<: *ci-template -ci-flocq: +library:ci-iris-lambda-rust: + <<: *ci-template-flambda + +library:ci-math-comp: + <<: *ci-template-flambda + +library:ci-sf: <<: *ci-template -ci-formal-topology: +library:ci-unimath: <<: *ci-template-flambda -ci-geocoq: +library:ci-vst: <<: *ci-template-flambda -ci-coqhammer: +# Plugins are by definition the projects that depend on Coq's ML API + +plugin:ci-aac_tactics: <<: *ci-template -ci-hott: +plugin:ci-bignums: <<: *ci-template -ci-iris-lambda-rust: - <<: *ci-template-flambda +plugin:ci-coq_dpdgraph: + <<: *ci-template -ci-ltac2: +plugin:ci-coqhammer: <<: *ci-template -ci-math-comp: - <<: *ci-template-flambda +plugin:ci-elpi: + <<: *ci-template -ci-mtac2: +plugin:ci-equations: <<: *ci-template -ci-paramcoq: +plugin:ci-fiat-parsers: <<: *ci-template -ci-plugin_tutorial: +plugin:ci-ltac2: <<: *ci-template -ci-quickchick: - <<: *ci-template-flambda +plugin:ci-mtac2: + <<: *ci-template -ci-relation-algebra: +plugin:ci-paramcoq: <<: *ci-template -ci-sf: +plugin:ci-plugin_tutorial: <<: *ci-template -ci-unimath: +plugin:ci-quickchick: <<: *ci-template-flambda -ci-vst: - <<: *ci-template-flambda +plugin:ci-relation-algebra: + <<: *ci-template |