coq-community / run-coq-bug-minimizer

Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
MIT License
2 stars 0 forks source link

Support ci-metacoq #7

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

Currently minimizing ci-metacoq doesn't work (https://github.com/coq/coq/pull/14328#issuecomment-854079065) for reasons I'm not clear about (https://github.com/coq/coq/issues/14453) and which are hard to debug (https://github.com/coq/coq/issues/14448, https://github.com/MetaCoq/metacoq/issues/563). This issue is a reminder and a place for centralizing the tracking of issues related to getting CI minimization to work for metacoq. Help on this would be very much appreciated, as I'd like CI minimization to work for metacoq and I don't understand the metacoq build system well enough to get what's going on with Coq's CI artifacts.

JasonGross commented 3 years ago

Seems to now be fixed by https://github.com/coq/coq/pull/14489 and https://github.com/MetaCoq/metacoq/issues/563#issuecomment-859508675