Stream: Coq devs & plugin devs

Topic: Finding all locations where a definition is unfolded


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 21 2023 at 21:12):

But I'm assuming you qed the definition first

view this post on Zulip Andres Erbsen (Mar 21 2023 at 22:47):

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

view this post on Zulip Gaëtan Gilbert (Mar 21 2023 at 22:58):

by async do you mean vio?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 22 2023 at 10:09):

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

view this post on Zulip Gaëtan Gilbert (Mar 22 2023 at 10:11):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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: Dec 05 2023 at 12:01 UTC