Minimal lean file for a definition or theorem

Stream: general

[Joseph Tooby-Smith]

Suppose I'm working in a project, let me call it A, downstream of Mathlib. Given a list of commands (or names corresponding to commands) in A, call it L, I want to create the minimal lean file satisfying the following four conditions:

• The Lean file runs without error (assuming A runs without error).
• Every command in the file corresponds to a command in A.
• Every command in L has a corresponding command in the file.
• The file only imports Mathlib files.

Is there anything obvious I'm missing regarding e.g. metaprogramming which would make this unfeasible?

The motivation is to create a file which can be imported into https://live.lean-lang.org (so e.g. follow up results could be derived without installing A), and also understand the dependencies of the results in L.

There is also a variation of this question for results in Mathlib, although I'm personally less interested in that.

[Eric Wieser]

In general I think this is impossible, because the commands you run could make assertions about the current module name

[Eric Wieser]

But also, you'd need to be careful about private defs in different files that share a name, so would need to rewrite those

[Eric Wieser]

Maybe it's possible to write a file_contents macro that treats its contents as if it were the contents of an imported module?

[Julian Berman]

It's only somewhat related (in that it isn't Lean, and doesn't relate to your conditions) but I have https://github.com/JasonGross/coq-tools starred to look at at some point, I'm sure because someone here linked it as being useful in the Coq world, possibly Kevin.

[Damiano Testa]

A few people have tried to write a minimizer, but this is actually quite involved. I don't think that there is anything ready to be used for that.

[Bhavik Mehta]

I appreciate a minimizer is difficult, but I'd just like to add that I'd find it _incredibly_ valuable - about 70% of my Lean time is spent trying to isolate and minimize issues/bugs

[Mario Carneiro]

I'm pretty sure @Johan Commelin or @Rob Lewis already built one? I forget the details

[Damiano Testa]

I remember a "tree-shaking" discussion with @Anne Baanen writing a prototype.

[Damiano Testa]

Ok, this is probably what I remember: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Minimizer.20script.

[Mario Carneiro]

aha, good job me for remembering none of the people involved correctly

[Damiano Testa]

Anyway, I also tried this for a while, and it resulted in me learning about find_home, minImports, Syntax and refactor.

[Damiano Testa]

I think that I may give this another go, since I understand a bit more the involved pieces.

[Kim Morrison]

Someone is actively working on a test case reducer currently, and making rapid progress. They want to keep the project private for a bit longer, but David+Johan+I are actively talking to them and providing metaprogramming help where necessary. (They are also making good use of lessons learned from minImports!)

[Kim Morrison]

I think everyone agrees this is a priority, and I'm really excite someone is seriously working on it.

[Kim Morrison]

If, for any reason, that project stalls out or needs help, we'll make sure to update everyone.

[Damiano Testa]

Ok, thanks for the update: I will not look again into this, then -- at least until this project has any update.

[Kevin Buzzard]

I've not needed to minimise stuff recently, but during the port and for the year or so afterwards when we were trying to understand the differences between lean 3 and lean 4's typeclass inference algorithms and I was often having to spend hours de-mathlibbing problems, so I'm very excited to hear that someone is thinking about this seriously :-) I've got extremely limited experience with using Coq so I was probably not recommending the tool, I was just pointing out that I was jealous of it :-) My answer to it was here (building alg heirarchies from scratch) and it was still a huge pain to minimise.

[Heather Macbeth]

Kim Morrison said:

Someone is actively working on a test case reducer currently, and making rapid progress. They want to keep the project private for a bit longer, but David+Johan+I are actively talking to them and providing metaprogramming help where necessary.

If, for any reason, that project stalls out or needs help, we'll make sure to update everyone.

Back in September someone was working on a test case reducer -- has this project seen any progress? It would be very useful to have such a tool!

[Kim Morrison]

Work is still happening! Not there yet, but progress...