The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I am attempting to create minimal reproducing examples for some bugs I have found in Coq.  Currently my strategy is to:

1. start with the source file which displays the error in Coq

2. recursively inline all of the files in my development which that file imports

3. rename things so that this bloated file displays the error (e.g., if I have duplicate section names, I need to rename one of them)

4. remove all lines of code which come after the line displaying the error

5a. replace as many proofs, definition bodies, etc. with [admit] as I can, while keeping the file compiling and displaying the bug

5b. work backwards through the file, removing any definitions, theorems, etc. which are not used later in the file (and for which removing them does not make the error go away)

6. play around with the drastically smaller file, trying to further eliminate things.

(I sometimes interleave 5a and 5b.)

I have created a python script that does step 2 for me automatically (assuming that all [Require Import] commands span only one line), and steps 3 and 4 do not take much time.  Currently, most of the manual drudge-work and time is spent in 5a and 5b.  I am considering writing python scripts to automate these for me, but before I do, I want to ask, does anyone know of any existing scripts which do this?  (Alternatively, do people have suggestions about how to better create such examples?)

Thanks,

Jason