How to minimize public imports

Stream: mathlib4

[Etienne Marion]

Hi, in #33064 by @David Ledvinka there is a new file created. The following imports work

public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
public import Mathlib.Probability.Notation

but this combination works too

public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
import Mathlib.Probability.Notation

and has the advantage of making public imports smaller. I thought that running lake shake Mathlib.MeasureTheory.Function.ConditionalLExpectation would automatically give the latter combination but instead it output a long list of imports changes in many files that resulted into

Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean:
  remove #[public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym]
  add #[import Mathlib.Tactic.Positivity.Finset, import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym, import Mathlib.MeasureTheory.Function.AEEqOfLIntegral, import Mathlib.MeasureTheory.Measure.Real, import Mathlib.Algebra.Order.Field.Power, import Mathlib.MeasureTheory.Integral.Lebesgue.Add, import Mathlib.Topology.Metrizable.Real, import Mathlib.MeasureTheory.Constructions.BorelSpace.Real, import Mathlib.Topology.GDelta.MetrizableSpace, import Mathlib.Tactic.Measurability, import Mathlib.Tactic.NormNum.GCD, import Mathlib.Data.Sym.Sym2.Init, import Mathlib.Tactic.ContinuousFunctionalCalculus, import Mathlib.Algebra.Order.BigOperators.Expect, import Mathlib.Data.EReal.Inv, import Mathlib.Topology.MetricSpace.ProperSpace.Real, import Mathlib.Algebra.Order.Module.Field, import Mathlib.Data.ENNReal.Inv, import Mathlib.Data.ENNReal.Real, import Mathlib.Algebra.Order.BigOperators.Ring.Finset, import Mathlib.Algebra.Order.Algebra, import Mathlib.Data.Rat.Floor, import Mathlib.Algebra.Order.Floor.Ring, import Mathlib.Tactic.NormNum.OfScientific, import Mathlib.Tactic.Positivity.Basic, import Mathlib.Tactic.NormNum.DivMod, import Mathlib.Tactic.NormNum.Ineq, import Mathlib.Tactic.NormNum.Eq, import Mathlib.Tactic.NormNum.Abs, import Mathlib.Data.Rat.Cast.Order, import Mathlib.Algebra.Order.Field.Basic, import Mathlib.Tactic.Bound.Init, import Mathlib.Data.Finset.Attr, import Mathlib.Tactic.SetLike, import Mathlib.Tactic.Finiteness.Attr, import Mathlib.Tactic.Common, import Mathlib.Init]

So to find the right combination I just kept adding public imports until the file built which is not really convenient. I conclude that I am wrong about how shake works, I thought it only worked on the current file, but I assume now that it works on all transitively imported files. It also seems like its output requires loads of nonpublic imports, which I suspect is because it requires all files to only public imports definitions, and so files which only contain theorems must be reimported over and over again as they are not transitively imported.

So my question is: Should we aim at minimizing public imports at all costs, i.e. follow shake's output and add long lists of nonpublic imports to all files? I am guessing no, because otherwise shake would have been run on Mathlib already. But then what is the middle ground? If all imports are public then I don't see why we have public imports.

[Kim Morrison]

I think you want lake shake --add-public, which will prevent shake suggesting replacing a public import with non-public ones (but will still allow for replacing a public import with an earlier public import).

[Kim Morrison]

The preferred settings for shake in Mathlib are currently lake shake --add-public --keep-implied --keep-prefix.

[Kim Morrison]

That said, contributors are welcome to propose replacing public imports with non-public ones. I think we're at the stage of exploring how much we want to do this! (The hope, I think, is that we can do it a lot!)

[Etienne Marion]

Thank you!