Minimize imports

Stream: mathlib4

[Moritz Firsching]

Is there an automated method for a file that works with import Mathlib, to figure out what is a minimal set of imports needed, so that it still works when removing import Mathlib?

[Kevin Buzzard]

I think there's find_home! which works on individual declarations; I don't know about a file-wide solution.

[Michael Stoll]

#minimize_imports (at the end of the file).

[Michael Rothgang]

If you want to minimize imports across multiple files, lake exe shake is really useful. You can run this on an individual "module" (think file, but with names à la Mathlib.Data.Real.Basic instead of Mathlib/Data/Real/Basic.lean), but also on the whole project. It even works on projects depending on mathlib.

[Michael Rothgang]

Both #minimize_imports and lake exe shake do not take notation or tactics into account: you might find that it removes "too much".

[Kim Morrison]

I wrote #minimize_imports (I think??) and Mario wrote lake exe shake, so you should expect shake to be more reliable. :-)