Can anyone think of a way to generate all errors that would be caused by making a definition Qed-opaque, CI-wide, not just the first ones blocking the build? E.g., making Nat.add opaque should yell a lot (vector append, etc), whereas most uses of Z.add might be fine with any definition that satisfies the standard-library lemmas, but in both cases just trying to build everything would fail early at some core lemma.
I wonder if running coqc in async mode would fit the bill: think about interpreting to the end in coqide / vscoq, but project-wide
This would struggle if you use enough dependent types, since async mode doesn't admit definitions that fail to typecheck.
But I'm assuming you qed the definition first
Yea this might work. Has the CI been built in async mode successfully?
by async do you mean vio?
.vio is file level parallelism / async. At least in IDEs there is also proof level parallelism / async - not sure if coqc has this as well.
vio also has proof level parallelism (in the vio2vo step)
see also https://github.com/coq/coq/issues/9262
@Andres Erbsen coq-lsp has enough error recovery that could work for your case, as long as indeed lemma statements can be still type-checked (if a proof fails, coq-lsp will indeed skip it and admit the lemma, that still may produce problems due to universes)
Actually coq-lsp error recovery is programmable
so you could add a rule to it that says "if this has failed because this particular unfolding error, retry but making the definition transparent"
But indeed the checking engine in coq-lsp was geared towards efficiently handling this kind of changes, by producing a global error list in a project
Last updated: Dec 05 2023 at 12:01 UTC