The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

My goal is to have it work well for things such as universe inconsistencies, anomalies, type errors, etc.  There are currently still some bugs in the code, in particular in the part which parses what constitutes a definition and how to remove a definition, and I haven't had much time to devote to it today.

If you want to try it out, you can clone the code, and run

./find-bug.py --fast --directory path/to/development path/to/buggy/file.v path/to/output/file.v -v

And this will inline all of the dependencies, remove unused Ltacs, and remove lines which come after the line which generates the error.  It also attempts to remove unused definitions, and attempts to replace the bodies of definitions with [Admitted] where doing this does not remove the universe inconsistencies (or whatever the bug was), but I'm still working out the bugs in these parts of the code.  (If you want to try your hand at fixing them, be my guest.  I can direct you to the relevant python files and let you know the approach I took.)

-Jason

On Fri, Apr 12, 2013 at 2:56 AM, Hendrik Tews <tews AT os.inf.tu-dresden.de> wrote:

Jason Gross <jasongross9 AT gmail.com> writes:

   I've thrown together a bit of code at
   https://github.com/JasonGross/coq-bug-finder which does some basic

It would be nice if your tool could also be used to create
minimal examples for bugs in Coq specifications.

For example, I have a universe inconsistency error within a
development of 10,000 lines. I would be really interested to
strip this down to the minimal set of definitions/lemmas that
reproduce the universe inconsistency.

Bye,

Hendrik