The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

tl;dr: I wrote a proof-using-helper.py script to automatically implement [Set Suggest Proof Using] suggestions.

Coq 8.5 comes with a really neat `quick` coq_makefile target that lets you defer opaque proof processing to be done later, in parallel.  If your proof ends in Qed, you will automatically get the benefit of this on your second (and later) run of `make`, due to autogenerated *.aux files.  If you want to do this on the first run of the file, too, you must use [Proof using <variables to be used in the proof>].

To help migrate code, there is a [Set Suggest Proof Using] toggle that causes Coq to suggest [Proof using] directives for each file.  For large developments with hundreds or thousands of theorems, this is tedious to implement by hand.  I thus announce a python script, available in my coq-tools repository, called proof-using-helper.py, that takes the output of `make quick` and the `-R` arguments passed to coq_makefile, and implements the suggestions automatically.

There are a few cases it does not support:

- [Add Parametric Morphism] - see bug 4004

- The change will break proofs that begin with [clear <list of section variables]; you will have to comment out the [clear] statement manually - see bug 4005

- My script will be confused by comments with [Theorem foo] in them, when trying to update an actual [Theorem foo]

- My script will be confused by nested proof blocks, such as [Theorem foo. .... Theorem bar. ... Qed. ... Qed.]

- My script might not (yet) handle [Obligation]s of the [Program] language

N.B., my script backs up all files it modifies automatically, so you will not lose any code by running it.

Please report bugs and request features on the github issue tracker, or drop me a line by email if you found the tool useful.

-Jason