Tree shaking

Stream: general

[Johan Commelin]

Inspired by @Anne Baanen's Minimizer script thread, I was wondering again, how hard is it now to write a tree shaker for Lean 4 files?

I'm not yet sure what interacting with the treeshaker should look like. But to get a conversation going: I would like to autogenerate a new project ZeroToRealInSixThousandLines starting from Std and Mathlib, that contains everything needed for the construction of the real numbers, and nothing else. And the resulting project shouldn't depend on anything (except core, of course).

[Alex J. Best]

It sounds like @Anne Baanen has essentially already written it? From what I read in the linked thread if you made a file with only #check Real Anne's minimizer would eventually make such a file? Though perhaps it could get stuck at present, @Anne Baanen when your tool replaces an import by the file contents does it put everyhing in a section at least?

[Anne Baanen]

Alex J. Best said:

Anne Baanen when your tool replaces an import by the file contents does it put everyhing in a section at least?

It does!

[Anne Baanen]

Alex J. Best said:

It sounds like Anne Baanen has essentially already written it? From what I read in the linked thread if you made a file with only #check Real Anne's minimizer would eventually make such a file?

That's the ideal case, and if you're lucky it can get quite close. But you probably want to disable some of the more invasive passes, such as sorrying everything it can, though :)

[Johan Commelin]

Huh, @Anne Baanen Will your tool expand (aka inline) imports?

[Johan Commelin]

Aah, I see now that is indeed one of the features

[Anne Baanen]

Yes! It probably goes wrong with files outside of the current project but that should be fixable :)

[Johan Commelin]

But I guess tree-shaking can be done deterministically, and much faster than using the minimizer script.

[Johan Commelin]

So I think both tools are valuable, and probably deserve separate implementations