AFAIK, Coq currently stops processing a proof script once it finds the first failing proof. Wouldn’t it be better if Coq could continue processing and report all the proof failures in a single run? Reporting and fixing one error at a time requires O(n^2) time (n is the number of errors) to fix the entire script. For scripts that have non-trivial run times, the time savings could be significant. Also it may be helpful to know up front whether you have 2 errors or 25 errors to fix (ex: you’re converting an Ltac1 script to Ltac2).
A related use case is creating new proof scripts: If a user has multiple incomplete proofs in a file and they want to work on any one of these other than the first, they have to mark all the prior incomplete proofs with “Admitted” to reach the one they want. That seems tedious.
And another: if a proof script is compute intensive, there could be a long wait between starting Coq and being able to resume work on an incomplete proof. Obviously, it helps to avoid restarting Coq, but that can’t always be avoided. In this case, it would be helpful to have a way to automatically Admit all proofs (skipping most of the work) up to to a user-designated point in the script.
I don’t know if these use cases matter enough to justify implementing these features, but I thought I’d put the idea out for discussion.
(PS How about updating the category description to mention, if correct, that this is a place to discuss enhancement ideas?)
This is already supported by CoqIDE and coq-lsp; they both include error-recovery heuristics.
However the current CoqIDE/STM implementation is known to have some open issues around so I am not sure about the support on Windows.
Regarding flags for enabling such options see also issue https://github.com/coq/coq/issues/9236
My working workflow with Coq is to use Proof General, which lets me go up to the first failing proof and saves the correct work done before that (the granularity is the ltac command). Used in this way, there is no quadratic behavior as you mention: after I fix the first error, I can try checking up to the end of the file again without rechecking the already-done parts.
I can see how you could get quadratic behaviors when debugging a single tactic that does a lot of work (but then I don’t think automatically succeeded would work at all, given that failure of a search branch is important information for the tactic behavior), or when it is the Qed commend that fails at the end of a script – but I consider it a usuability problem when Qed can fail (typically in coinductive proofs) and try to find another way that does not (in the case of coinduction, using Paco); I would find it highly unusual to have a Qed command that fails for several different reasons.
@gasche PG and CoqIDE rely on Coq’s underlying support to avoid rechecking already-done proofs. Sounds like you’re comfortable with always fixing failing proofs in the order they appear in the file (or inserting Admitted).
@ejgallego
This is already support by CoqIDE and coq-lsp; they both include error-recovery heuristics.
How do I enable this, how does it work in CoqIDE? If I get an Attempt to save an incomplete proof error, the Definition is not processed.
:
Qed.
Definition a := 0.
But the current support requires that async proofs are enabled? (AFAIK async proofs are not supported on Windows).
It’s not that the support is not there, but it is disabled by default because users of this feature have reported lots of issues that couldn’t (yet?) be fixed.
It’s a bit sad that this error-recovery feature is so tied up with the async proof mode. If the issues are with threading, we could perfectly imagine no threading on Windows but still an error-recovery mode that works. I guess the problem is that you don’t want to have to wait for the whole file to be evaluated before starting to fix your error, so that’s actually the issue with having an error-recovery mode without async proof support.
@jfehrle I’m afraid I don’t recall the exact flags settings to enable this, but IMHO you should be able to do it on Win. The defaults are very conservative as not to annoy users.