Stream: Miscellaneous

Topic: ✔ Whitelist of proof starters and enders


view this post on Zulip andrew touchet (Feb 08 2023 at 11:02):

Is there a whitelist of commands to start proofs and end proofs for Coq versions > 8.9?

view this post on Zulip Gaëtan Gilbert (Feb 08 2023 at 11:05):

no

view this post on Zulip Karl Palmskog (Feb 08 2023 at 12:02):

if this is about parsing Coq code, this is strongly recommended against due to Coq's lexer and parser changing dynamically during execution. See https://github.com/ejgallego/coq-serapi for a more principled way to get code out of Coq.

view this post on Zulip andrew touchet (Feb 08 2023 at 13:23):

Thanks! I was hoping there was a short list I could use to extract broken proofs since it seems that checking for the end of a broken proof would difficult with any of the existing tools (as far as I’ve seen and heard).

view this post on Zulip Karl Palmskog (Feb 08 2023 at 13:26):

it's very difficult to know anything about where a proof script begins or ends unless you are Coq. Some proofs are not even defined by proof scripts.

view this post on Zulip Guillaume Melquiond (Feb 08 2023 at 13:31):

If you are not using a plugin to change the syntax, then the keywords are Qed, Defined, Admitted, Save, and Abort.

view this post on Zulip Pierre Courtieu (Feb 08 2023 at 14:56):

ProofGeneral data on this:
https://github.com/ProofGeneral/PG/blob/8416875696cb0c4283e96fe721d343277882ecea/coq/coq-syntax.el#L537
There is also terrible code to detect when a Definition (and others) does not contain a := and hence is actually a goal starter.

view this post on Zulip Pierre Courtieu (Feb 08 2023 at 14:58):

It is not so common that a plugin defines a new way to start a goal, but indeed it breaks everything.

view this post on Zulip andrew touchet (Feb 08 2023 at 15:13):

I might be able to hack something together then as long as I check for plugins, and match the starters to Enders appropriately. Might not be perfect but that was still helpful!

view this post on Zulip Notification Bot (Feb 08 2023 at 15:13):

andrew touchet has marked this topic as resolved.

view this post on Zulip Meven Lennon-Bertrand (Feb 09 2023 at 08:57):

Pierre Courtieu said:

It is not so common that a plugin defines a new way to start a goal, but indeed it breaks everything.

Is not so uncommon to use plugins with some obligation mechanism though, right? In which case, Next Obligation also starts a proof script. Although it is maybe more like a sub-proof of the previous definition, really


Last updated: Dec 07 2023 at 17:01 UTC