Bug minimizer

Stream: general

[Bas Spitters]

@Jason Gross made a very useful bug minimizer for Rocq: https://coqpl.cs.washington.edu/wp-content/uploads/2014/12/bug-minimizer.pdf
https://github.com/JasonGross/coq-tools

One of the features it has, is given a theorem, it collects it's minimal set of definition/lemma dependencies all in one file. This is great for debugging/ reporting bugs.
Does there exist a similar tool for Lean ?

[Bhavik Mehta]

I would find this very useful, but I don't know of one that exists yet

[Jason Gross]

The trickiest part of the bug minimizer in Rocq is figuring out how to deal with naming and imports in Rocq, especially in the presence of global flags and diamond dependencies. I'm less familiar with the intricacies of Lean; what would go wrong with the following strategy?
Topologically sort the dependencies, wrap each file in section...end, strip out all import statements, concatenate together into a single file.

[Matthew Ballard]

Claude is doing this for me right now! Unclear how well...

[Henrik Böving]

Jason Gross said:

The trickiest part of the bug minimizer in Rocq is figuring out how to deal with naming and imports in Rocq, especially in the presence of global flags and diamond dependencies. I'm less familiar with the intricacies of Lean; what would go wrong with the following strategy?
Topologically sort the dependencies, wrap each file in section...end, strip out all import statements, concatenate together into a single file.

That with arbitrary meta programming it is quite non trivial to figure out what you even want to import to begin with.

[Michael Rothgang]

@Damiano Testa You mentioned you had a prototype for this, right? Is this something you can already usefully share?

[Johan Commelin]

@Christian Kalhauge has been working on this for Lean as well. @Bas Spitters you're both in Denmark (-;

[Johan Commelin]

And I think @Emilio Jesús Gallego Arias is also (starting to) working on that repo?

[Matthew Ballard]

The task is unsolvable given constraints: preserve theorem unchanged + reach zero Mathlib imports.

[Jason Gross]

Bas Spitters said:

https://coqpl.cs.washington.edu/wp-content/uploads/2014/12/bug-minimizer.pdf
https://github.com/JasonGross/coq-tools

Btw, there's a more recent publication on this, from 2022

[Christian Kalhauge]

@Bas Spitters and @Johan Commelin Just saying hi :). Yes I have been working on a reducer as part of a larger research project. I'll love to talk about it, if you are interested :)

[Bas Spitters]

Yes, please tell us more!

[Christian Kalhauge]

Sorry the delays in coms. I have been facilitating exams the last couple of weeks.

I'm working on a new way of writing reducers, which instead of using the syntax driven approach (like ddmin) or the list based approach (like quick checks shrink) uses an approach closer to fuzzing. I.e., reduction is seen as using a string of bits to produce smaller programs.
Using this formulation (in contrast to the others), we can reduce programs with dynamic syntax, while keeping the context of the reduction (which is lost when doing list based reduction).

Anyhow, I did an initial prototype of the idea in a closed repository, but had to divert resources to actually get the idea published (which is still in progress). In the mean time, the prototype has stoped working because it uses some of the compiler internals to do the reduction in stages. I think @David Thrane Christiansen is looking into finding resources to get it up and running again.

If you are ever in the Copenhagen area, or if you just want to come by and visit us at DTU, please let me know. It could be a lot of fun :).