Stream: Coq devs & plugin devs

Topic: Finding all locations where a definition is unfolded

Andres Erbsen (Mar 21 2023 at 19:29):

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.

Paolo Giarrusso (Mar 21 2023 at 21:10):

I wonder if running coqc in async mode would fit the bill: think about interpreting to the end in coqide / vscoq, but project-wide

Paolo Giarrusso (Mar 21 2023 at 21:11):

This would struggle if you use enough dependent types, since async mode doesn't admit definitions that fail to typecheck.

Paolo Giarrusso (Mar 21 2023 at 21:12):

But I'm assuming you qed the definition first

Andres Erbsen (Mar 21 2023 at 22:47):

Yea this might work. Has the CI been built in async mode successfully?

Gaëtan Gilbert (Mar 21 2023 at 22:58):

by async do you mean vio?

Michael Soegtrop (Mar 22 2023 at 10:05):

.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.

Gaëtan Gilbert (Mar 22 2023 at 10:09):

vio also has proof level parallelism (in the vio2vo step)

Gaëtan Gilbert (Mar 22 2023 at 10:11):

see also https://github.com/coq/coq/issues/9262

Emilio Jesús Gallego Arias (Mar 22 2023 at 17:06):

@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

Emilio Jesús Gallego Arias (Mar 22 2023 at 17:07):

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"

Emilio Jesús Gallego Arias (Mar 22 2023 at 17:08):

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: May 28 2023 at 16:30 UTC