ci-local-noclean target fails #605
Comments
3 tasks
JasonGross
added a commit
to JasonGross/coq
that referenced
this issue
Nov 10, 2021
This will ensure that the MetaCoq CI job continues to be minimizable, and will catch issues like MetaCoq/metacoq#605 earlier. It's plausible that we should instead have a general CI target that is dependent on all successful CI targets (perhaps split amongst the various base Coq jobs), to test this everywhere. Or perhaps the CI should run each ci-script.sh twice, which might be a good enough approximation.
|
This issue is still making metacoq failures unminimizable at coq/coq#15770 (comment) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
At https://github.com/coq-community/run-coq-bug-minimizer/runs/4123345900?check_suite_focus=true#step:5:46597
You can recreate this (for now) by downloading the artifacts at https://gitlab.com/coq/coq/-/jobs/1750733291/artifacts/download and https://gitlab.com/coq/coq/-/jobs/1750733365/artifacts/download. This is at coq/coq@0e663cc
The text was updated successfully, but these errors were encountered: