Port the Coq bug minimizer to F*

[tchajed]

@JasonGross has an awesome bug minimizer for Coq (described in this CoqPL paper). The idea is to take a bug, defined as a specific error, and remove input that isn't necessary to trigger that bug. In addition, it inlines external modules to try to get a self-contained example.

This might be a super ambitious project, but I think in the long run such tools are really useful.

[catalin-hritcu]

Great idea, currently we spend significant time minimizing F* inputs.

How does Jason's tool vary from vanilla delta debugging for input minimization?
https://en.wikipedia.org/wiki/Delta_Debugging

[tchajed]

It sounds exactly like an instance of delta debugging, particularly the example of removing irrelevant lines. There are a few techniques to apply that are specific to verification; for example, you can try to replace definitions that are used with assume val.

[JasonGross]

The tool is somewhat specialized to Coq; it knows how to communicate with Coq, which things in the error message change between runs (line numbers, universe numbers, file names, evar numbers), and which don't. That said, it is basically a delta-debugging tool, though I haven't written the binary search part of it (and I hadn't heard of delta-debugging when I wrote it).

Specific passes that it does which are specific to Coq/verification:

• it lifts Require statements to the top of the file to work around Coq bugs
• it automatically finds dependency files, and goes through a lot of trouble to inline their contents (one at a time) in a way that doesn't change the error message (this is really hard because Coq doesn't have proper namespaces)
• it chunks entire theorem-proof blobs as one unit, and splits at sentences/commands outside of proofs, not at lines (since eol means nothing to Coq)
• it can admit proofs
• it has a special pass where it tries to recursively remove definitions of identifiers that don't appear later in the file, all at once. This trims down the amount of line-by-line removal that has to be done.

[JasonGross]

I guess another thing is that I take advantage of the fact that Coq sources are linear, so removing things from the end generally doesn't hurt, and that it's rare that you need to remove multiple lines simultaneously to remove any of them.

[cpitclaudel]

Bonus points if the whole thing is written as a tactic