aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorJason Gross2020-04-24 17:14:43 -0400
committerJason Gross2020-04-27 20:24:42 -0400
commit9e7a47b94a333c7c4c19d31642f04b7263db415b (patch)
treec24ed9c968277de81e3a60b481d9bb0e29297703 /.gitlab-ci.yml
parentd15b99d93b67f37a0c572950868713b2a7a2b1a4 (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).
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml3
1 files changed, 3 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