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