andrew touchet (Feb 08 2023 at 11:02): 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?
Gaëtan Gilbert (Feb 08 2023 at 11:05):no
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.
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).
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.
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.
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.
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.
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!
Notification Bot (Feb 08 2023 at 15:13):andrew touchet has marked this topic as resolved.
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: Jun 05 2023 at 10:01 UTC