The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I would like to announce that I have created a few python scripts that take in a Coq file displaying an error, and works to minimize that file.  The scripts can be found at https://github.com/JasonGross/coq-bug-finder, which currently additionally contains one example and a readme with instructions for running.

I have successfully used this code to create small examples to help track down a number of bugs in the universe polymorphic version of Coq at HoTT/coq on github; the average starting file size was around 5000 lines, and the code usually managed to trim this to around 1000-2000 lines by itself, and then down to 50-300 lines with a bit of extra manual help.  It currently can only handle developments with a flat directory structure, but if there's interest, I can work on making it handle dependencies in other folders as well.

-Jason

On Tue, Apr 9, 2013 at 4:14 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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