diff options
| author | Jason Gross | 2020-04-24 17:14:43 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-27 20:24:42 -0400 |
| commit | 9e7a47b94a333c7c4c19d31642f04b7263db415b (patch) | |
| tree | c24ed9c968277de81e3a60b481d9bb0e29297703 | |
| parent | d15b99d93b67f37a0c572950868713b2a7a2b1a4 (diff) | |
[ci] Add coq-tools to the CI
After #12023 broke the bug minimizer, I'd like to add
[coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's
relatively light-weight (under 5 minutes, I believe), and I'd like to
know when it's going to break on master before it's broken, rather than
after. It tests a relatively under-tested part of Coq, mostly (the
display output of error message, by and large), and I'm happy to take
responsibility for fixing it when some PR is going to break it (mainly I
just want a sort-of early warning system, and I want PRs to not
accidentally break it by changing things that they don't realize they're
changing).
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-coq-tools.sh | 9 |
4 files changed, 20 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1a1d31bdd7..468161ff73 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -676,6 +676,9 @@ library:ci-color: library:ci-compcert: extends: .ci-template-flambda +library:ci-coq-tools: + extends: .ci-template + library:ci-coqprime: stage: stage-3 extends: .ci-template-flambda diff --git a/Makefile.ci b/Makefile.ci index 1a5e8166a2..b545c9de45 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -20,6 +20,7 @@ CI_TARGETS= \ ci-coquelicot \ ci-corn \ ci-cross-crypto \ + ci-coq-tools \ ci-coqprime \ ci-elpi \ ci-ext-lib \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index c18e556da8..88f410ef04 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -95,6 +95,13 @@ : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" ######################################################################## +# coq-tools +######################################################################## +: "${coq_tools_CI_REF:=master}" +: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}" +: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}" + +######################################################################## # Coquelicot ######################################################################## : "${coquelicot_CI_REF:=master}" diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq-tools.sh new file mode 100755 index 0000000000..9c95c49c9f --- /dev/null +++ b/dev/ci/ci-coq-tools.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coq_tools + +( cd "${CI_BUILD_DIR}/coq_tools" && make check || \ + { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } ) |