The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

On 9 avr. 2013, at 22:14, 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?)
This would be very handy indeed to have an automatic tool for isolating bugs.
I remember spending quite some time trimming down a development to eventually 
come up with a ridiculously small buggy input!

There is an algorithm/approach called delta debugging 
http://www.st.cs.uni-saarland.de/dd/
which automates the process of isolating a small buggy input by performing 
some kind of binary search.
I do not precisely remember the requirements for using this approach and how 
generic the algorithm is.
At the time, it looked pretty neat to me…

Best,
--
Frédéric