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

no

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.

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

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.

If you are not using a plugin to change the syntax, then the keywords are `Qed`

, `Defined`

, `Admitted`

, `Save`

, and `Abort`

.

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.

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

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!

andrew touchet has marked this topic as resolved.

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