Jason Gross

Oops, I closed and reopened to restart the CI, and coqbot removed the 1.15.0 milestone :-(

I'd be quite interested in seeing the code coverage diff between, say, all of the current CI vs all of the current CI + fiat-crypto-legacy (which I've been maintaining compatible...

It might be possible to combine code coverage diffs with the bug minimizer to increase the coverage of the test-suite. In particular, if you can find CI developments that cover...

If you make multiple makefile targets for the different versions of Coq, you can just have a travis environment variable that says which make target to build.

Currently tracking #16332, looking at the issue with MetaCoq in https://github.com/coq/coq/pull/16332#issuecomment-1190289835

Now that https://github.com/JasonGross/coq-tools/pull/127 has been merged, let's try @coqbot ci minimize ci-metacoq

@coqbot resume ci minimize ci-fiat_crypto_legacy ``` Require Crypto.Util.ZUtil.Div. Module Export Modulo. Import Coq.ZArith.ZArith. Import Coq.ZArith.Znumtheory. Import Crypto.Util.ZUtil.Hints.ZArith. Module Export Z. Lemma mul_div_eq_full : forall a m, m 0 -> m...

@coqbot resume ci minimize ci-fiat_crypto_legacy ``` Require Crypto.Util.ZUtil.Div. Module Export Modulo. Import Coq.ZArith.ZArith. Import Coq.ZArith.Znumtheory. Import Crypto.Util.ZUtil.Hints.ZArith. Module Export Z. Lemma mul_div_eq_full : forall a m, m 0 -> m...

@coqbot resume ci minimize ci-fiat_crypto_legacy ``` Declare ML Module "coq-core.plugins.ltac". Module Export AdmitTactic. Module Import LocalFalse. Inductive False : Prop := . End LocalFalse. Axiom proof_admitted : False. Global Set...

Trying this again to see if updated annotations work @coqbot resume ci minimize ci-fiat_crypto_legacy ``` Require Crypto.Util.ZUtil.Div. Module Export Modulo. Import Coq.ZArith.ZArith. Import Coq.ZArith.Znumtheory. Import Crypto.Util.ZUtil.Hints.ZArith. Module Export Z. Lemma...