bug in #minimize_imports, vs. #redundant_imports

Stream: mathlib4

[Michael Rothgang]

I wanted to find out if the imports in my file are optimal (or if there are redundant imports).

I vaguely remembered the #minimize_imports command - that looked like just what I need. The docstring mentioned syntax and tactics, neither of which are an issue for me. So I ran this at the end of my file.

Actually, this yielded just the file name. I had expected, however, to be suggested a minimal set of imports for the top of this file. For instance, deliberately introducing a superfluous import should yield a message telling me that.

Would you accept a PR adding a sentence clarifying this to the docs?

[Michael Rothgang]

Besides, I'm puzzled now: when does #minimize_imports yield a non-trivial answer? (If it always yields the current file, it surely isn't useful --- so what am I missing?) I'm still pretty new to Lean, so I'm sure I just don't know this yet...

[Scott Morrison]

Sorry, #minimize_imports is buggy. :-(

[Scott Morrison]

It should never report the file you are actually in!

[Scott Morrison]

The implementation is not that complicated. If anyone wants to hit F12 and read the code, it is probably easily fixable. :-)

[Michael Rothgang]

Oh, I see. Here's a somewhat minimal example of my setting then.

import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
set_option autoImplicit false

variable
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G]
  (J : ModelWithCorners ℝ F G) {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
  [SmoothManifoldWithCorners J N] [FiniteDimensional ℝ F]
  [MeasurableSpace F] [BorelSpace F]
variable {J}

variable (J) in
def MeasureZero (s : Set N) : Prop :=
  ∀ (μ : MeasureTheory.Measure F) [MeasureTheory.Measure.IsAddHaarMeasure μ], ∀ e ∈ atlas G N, μ (J ∘ e '' (e.source ∩ s)) = 0

lemma iUnion { ι : Type* } [Encodable ι] { s : ι → Set N } (hs : ∀ n : ι, MeasureZero J (s n)) : MeasureZero J (⋃ (n : ι),  s n) := by sorry
-- BUG: running `#minimize_imports` here just suggests this file itself.

[Michael Rothgang]

(Uses lean-4.0.0-rc4 and mathlib as of Wednesday. I don't know how to minimize that further/what is important for this bug.)

[Michael Rothgang]

Another related question (feel free to move to a new thread if better!): searching the mathlib4 docs turned up #redundant_imports also. How do these relate?

Deliberately introducing a never-used import gets flagged by #redundant_imports --- but I would also like a command looking inside my imports. (For instance, I'm not using anything inside Mathlib.MeasureTheory.Function.Jacobian above.) Is this "looking inside" what minimize_imports is supposed to do?

[Scott Morrison]

Yes

[Michael Rothgang]

Ah, I see. Is there a way to clarify the documentation? I don't find that obvious from the current phrasing.

[Michael Rothgang]

(I don't see an obvious improvement either.)

[Scott Morrison]

Does

import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
import Mathlib.MeasureTheory.Group.Measure

sound right?

[Scott Morrison]

Try out #7025.

[Scott Morrison]

Unfortunately it is hard to write good tests for this right now, because the way we have our tests organised you can't import one test file from another!

[Michael Rothgang]

Works like a charm in this example :heart:

[Michael Rothgang]

The original file needs something more...

[Scott Morrison]

Syntax / macros / tactics are going to confuse the current implementation, which just inspects the constants used.

[Michael Rothgang]

How can I use that PR, without building mathlib all by myself? (I'm in an external project depending on mathlib.) Pointer to the docs is fine if that's just RTFM.

[Michael Rothgang]

Scott Morrison said:

Syntax / macros / tactics are going to confuse the current implementation, which just inspects the constants used.

No, that file just has more math content :-)

[Scott Morrison]

In your lakefile.lean, change "master" on the line that specifies mathlib as a dependency to "fix_minimize_imports"

[Michael Rothgang]

Scott Morrison said:

In your lakefile.lean, change "master" on the line that specifies mathlib as a dependency to "fix_minimize_imports"

There's no such line; the relevant section seems to be.
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

[Scott Morrison]

Ah, sorry

[Scott Morrison]

Just add @ "fix_minimize_imports" at the end of that line.

[Scott Morrison]

However until CI finishes on #7025 you want have any oleans available, so it will be painful to use. Waiting an hour should solve that.

[Michael Rothgang]

Thanks a lot for all the guidance!!

[Michael Rothgang]

Scott Morrison said:

Just add @ "fix_minimize_imports" at the end of that line.

Tried now; the new toolchain works. At first I just noticed this wasn't working; then I saw an info message on the first line, "manifest out of date"; following its instructions seems to work.

[Michael Rothgang]

I think the correct steps are.

• edit lakefile.lean to point to the brain (as above, in my case, appending @ "fix_minimize_imports")
• close VS Code
• run lake update; in this case, this includes downloading a new lean toolchain
• run lake exe cache get to update the mathlib case
• open VS Code again

On first try, I ran lake update in the terminal while having VS Code open, then got a prompt asking me to restart the server, and saw it happily building std and mathlib... cancelling it and updating the cache cut that short :-)

[Scott Morrison]

lake update is actually a bit dangerous if you have dependencies that point to branches rather than commits, as it will update to the head of that branch. e.g. if you do this in Mathlib itself (but not in a project that depends on Mathlib) suddenly you are responsible for dealing with any breaking changes in std, aesop, etc.

Sometimes safer is just to delete your lake-packages directory. Then the next lake exe cache get or lake build will reconstitute it.

[Scott Morrison]

Obviously this is not an ideal situation, but we don't seem to have come up with a way to prevent users hurting themselves with lake update!

[Michael Rothgang]

Ah, I see. So much to still learn :-) I'll just delete that directory next time then.

[Michael Rothgang]

@Scott Morrison I'm now wondering how these commands differ. Is the following an accurate description?

#redundant_imports looks for import lines which can be straight up removed (as it's already transitively included),
where #minimize_imports also checks if a file can be replaced by an import lower in the hierarchy.

In particular, it seems to me that #redundant_imports does a subset of #minimize_imports. Is this correct? (If so, I'm wondering why both commands exist --- is the former faster to run or so?)

[Scott Morrison]

Suppose we have files A.lean, B.lean, C.lean, and D.lean where C.lean contains

import A
import B
import D

and B.lean contains

import A

Now (regardless of the definitions in the file!) #redundant_imports in C.lean should suggest deleting import A, because this is transitively implied by the import B.

[Scott Morrison]

Further suppose that the definitions in C.lean in fact only depend on material from A.lean. Then #minimize_imports in C.lean should suggest deleting import B and import D.

[Scott Morrison]

So no, they are not "comparable".