late imports

Stream: mathlib4

[Kim Morrison]

This isn't a "technical debt" metric (so perhaps we should move this to a new topic), but I think the following is very interesting:

1. Turn on linter.minImports globally:

diff --git a/lakefile.lean b/lakefile.lean
index 2296f7f90db..a553d8a3789 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -39,7 +39,8 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.style.longFile, .ofNat 1500⟩,
   ⟨`linter.style.missingEnd, true⟩,
   ⟨`linter.style.multiGoal, true⟩,
-  ⟨`linter.style.setOption, true⟩
+  ⟨`linter.style.setOption, true⟩,
+  ⟨`linter.minImports, true⟩
 ]

 /-- These options are passed as `leanOptions` to building mathlib, as well as the

2. lake build > minImport
3. grep "warning: .*Imports increased by [0-9][0-9]" minImports | sort -t':' -k3,3nr | head -n 20 reports

warning: ././././Mathlib/Topology/Algebra/Module/Basic.lean:2408:0: Imports increased by 17 to
warning: ././././Mathlib/Topology/Algebra/Module/Basic.lean:2356:0: Imports increased by 40 to
warning: ././././Mathlib/Data/Matrix/Basic.lean:2260:0: Imports increased by 79 to
warning: ././././Mathlib/Computability/TuringMachine.lean:2119:0: Imports increased by 10 to
warning: ././././Mathlib/Analysis/Asymptotics/Asymptotics.lean:1932:0: Imports increased by 19 to
warning: ././././Mathlib/Data/Set/Lattice.lean:1810:0: Imports increased by 75 to
warning: ././././Mathlib/Analysis/Asymptotics/Asymptotics.lean:1802:0: Imports increased by 12 to
warning: ././././Mathlib/Topology/Category/Profinite/Nobeling.lean:1756:0: Imports increased by 65 to
warning: ././././Mathlib/Analysis/InnerProductSpace/Basic.lean:1635:0: Imports increased by 18 to
warning: ././././Mathlib/Topology/UniformSpace/Basic.lean:1617:0: Imports increased by 23 to
warning: ././././Mathlib/Data/DFinsupp/Basic.lean:1603:0: Imports increased by 30 to
warning: ././././Mathlib/Algebra/Order/Floor.lean:1583:0: Imports increased by 12 to
warning: ././././Mathlib/SetTheory/Cardinal/Basic.lean:1576:0: Imports increased by 10 to
warning: ././././Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean:1493:0: Imports increased by 206 to
warning: ././././Mathlib/Analysis/Asymptotics/Asymptotics.lean:1470:0: Imports increased by 14 to
warning: ././././Mathlib/Topology/ContinuousMap/Bounded.lean:1390:0: Imports increased by 22 to
warning: ././././Mathlib/MeasureTheory/MeasurableSpace/Basic.lean:1388:0: Imports increased by 16 to
warning: ././././Mathlib/Topology/Category/Profinite/Nobeling.lean:1361:0: Imports increased by 127 to
warning: ././././Mathlib/Topology/Category/Profinite/Nobeling.lean:1356:0: Imports increased by 36 to

This is identifying files in Mathlib where an import is "newly used" very late in a file, and substantially increasing the number of transitive imports.

[Kim Morrison]

e.g. this is saying that up to line 2408(!!) of Mathlib/Topology/Algebra/Module/Basic.lean there is some import that has not been necessary so far in the file, but becomes necessary at this point and pulls in a total of 17 transitive imports.

[Kim Morrison]

I feel like these are great targets for splitting --- the overlap of "large files" and "files with lots of content that do not use some of the imports".

[Kim Morrison]

I'd love to see us make regular progress on reducing that 2408.

[Damiano Testa]

I wonder whether this should be a linter.

[Kim Morrison]

I don't think this makes sense as an always on linter. More a regular zulip bot.

[Damiano Testa]

Yes, I agree. It may probably also post what is the latest import.

[Damiano Testa]

I remember running a similar experiment while testing the linter, but I cannot find the thread now.

[Damiano Testa]

Found it.

[Notification Bot]

9 messages were moved here from #mathlib4 > Technical Debt Counters by Johan Commelin.

[Damiano Testa]

Is there a way to get this report without having to rebuild all of mathlib?

[Johan Commelin]

probably not

[Damiano Testa]

Often I have wanted to have an option for linters that they could be turned on "after the fact".

[Damiano Testa]

This is maybe not reasonable, but could there not be a version of a "weak linter" that is guaranteed to just log information and therefore does not require rebuilding?

[Damiano Testa]

Looking at the thread, it looks like Kim already suggested working this statistics into the tech-debts report and that I had volunteered to do it!

[Damiano Testa]

I guess that I better get to work! :smile:

[Damiano Testa]

I still do not understand how to set weak options.

I thought that running

lake build  -Kweak.linter.minImports=true

would build Mathlib setting the linter.minImports option to true. However, the build simply uses the available cache. What am I doing wrong?

[Kim Morrison]

I guess that -K options get ignored for computing the traces...

[Kim Morrison]

I was just adding the option in the lakefile.

[Kim Morrison]

(thereby invalidating the traces)

[Damiano Testa]

Ok, I thought that it would have been more principled to use the command-line option, but it seems like modifying the lakefile is the more robust way forward, thanks!

[Kevin Buzzard]

Naive question: can this information not be "read off from the oleans" in some way, rather than recompiling everything?

[Damiano Testa]

Most of it, probably yes, although I do not think that the oleans store any information about tactics used, for instance.

[Damiano Testa]

Or notation.

[Damiano Testa]

So, you can reconstruct information of how to write the explicit term of each proof, probably.

[Damiano Testa]

Ah, there is also the issue that I do not think that there is a meaningful ordering to the declarations appearing in the oleans, but I am less sure about this.

[Mario Carneiro]

this is true, but the oleans do have declaration ranges, so you can try to work out where in the file they were defined that way

[Damiano Testa]

Ok, thanks for confirming!

[Damiano Testa]

Also, the linter does make use of the environment, so it is using the oleans already for the purely expression part.

[Damiano Testa]

#18631 has a (primitive) CI workflow that could post something like what is below on Zulip.

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	17	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Matrix/Basic.lean	2260	80	[Mathlib.Algebra.Star.Module]
Mathlib/Data/Set/Lattice.lean	1810	75	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	66	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Topology/UniformSpace/Basic.lean	1617	22	[Mathlib.Topology.Compactness.Compact, Init.Data.List.Nat.Pairwise]
Mathlib/Algebra/Order/Floor.lean	1583	12	[Mathlib.Data.Int.Lemmas]
Mathlib/Topology/ContinuousMap/Bounded.lean	1390	24	[Mathlib.Analysis.CStarAlgebra.Basic]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1388	16	[Mathlib.Order.LiminfLimsup]
Mathlib/RingTheory/TensorProduct/Basic.lean	1270	84	[Mathlib.RingTheory.Finiteness]
Mathlib/RingTheory/Polynomial/Basic.lean	1233	13	[Mathlib.RingTheory.Polynomial.Content]
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean	1207	10	[Init.Data.ULift, Mathlib.LinearAlgebra.FiniteDimensional, Init.Data.Fin.Fold]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Order/Module/Defs.lean	1173	22	[Mathlib.Tactic.Positivity.Core]
Mathlib/GroupTheory/FreeGroup/Basic.lean	1145	31	[Mathlib.Data.Fintype.Basic]
Mathlib/Algebra/Module/LocalizedModule.lean	1141	97	[Mathlib.Algebra.Exact]
Mathlib/SetTheory/Ordinal/Notation.lean	1140	19	[Mathlib.Tactic.NormNum.Pow]

[Damiano Testa]

Does this look useful? The CI step also contains the full report, not just the "top offenders".

[Kim Morrison]

I think I'd prefer that the post to zulip only reports things with a "significant" (e.g. >=10) increase in number of transitive imports. Just adding one new import late in a file is not really a problem. (If it's just one transitive import, it is clearly introducing something that is very close in subject matter, so there's not going to be an interesting split available.)

[Damiano Testa]

Sure, that is an easy enough filter!

[Damiano Testa]

I updated the list above to only contain the first few "late-importers" that increased the number of imports by at least 10.

[Kim Morrison]

(Looks like the PR deleted build.yml?)

[Damiano Testa]

Yes, I deleted build so that it would only build mathlib once, with the linter.

[Damiano Testa]

I am planning to restore the usual CI and put this one in a cron job.

[Kim Morrison]

Sounds good. We can also hopefully run it manually, after PRs that improve the table.

[Damiano Testa]

Yes, I know that Bryan has a trick to make CI actions be activated manually: I'll look at how those are done.

[Kim Morrison]

Claiming

Mathlib/Data/Matrix/Basic.lean 2260 80 Mathlib.Algebra.Star.Module

[Bryan Gin-ge Chen]

Damiano Testa said:

Yes, I know that Bryan has a trick to make CI actions be activated manually: I'll look at how those are done.

You can just put workflow_dispatch as one of the triggers under the on: section (Random example). Generally this is only useful for workflows that are run on a schedule since for e.g. workflows run on push, the "workflow_dispatch" event won't contain data about the PR / commit.

[Damiano Testa]

I updated the PR:

• workflow dispatch should mean that the workflow can be run manually (not really sure how, though);
• it will post on Mondays on the same schedule as the Technical Debt Metrics, but in a separate channel (and later, since the workflow lasts longer).

[Damiano Testa]

Ok, so I did the right thing, without knowing what I am doing! :smile:

[Damiano Testa]

If you prefer that the report is run on a different day or posts to the same thread as the other one, let me know.

[Damiano Testa]

Otherwise, #18631 is ready!

[Damiano Testa]

It would be good is someone started the workflow manually, just to check that everything works as intended: there are many moving parts and lots of places for stuff to go wrong!

[Damiano Testa]

However, the run takes about 2 hours and I am about to go to bed!

[Bryan Gin-ge Chen]

What little I know about workflow_dispatch is the first two or three sentences here: https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#workflow_dispatch
(Reading further now for the first time, it looks like there are a bunch of fancy options I never knew about!)

[Damiano Testa]

Btw, I am not sure about whether all the preparation steps before lake build are really necessary: feel free to prune what is not needed!

[Damiano Testa]

I suspect that the workflow can only be dispatched if it is merged in master already?

[Bryan Gin-ge Chen]

Yeah, I think that's right.

[Damiano Testa]

OK, I am going to push a branch where the action is actually active and maybe in a couple of hours it will post a report: does that sound reasonable?

[Bryan Gin-ge Chen]

Yeah sure! I've started looking at the workflow code and will try and leave some comments for when you wake up again :wink:

[Damiano Testa]

This is the test PR: #18636.

[Kim Morrison]

Kim Morrison said:

Claiming

Mathlib/Data/Matrix/Basic.lean 2260 80 Mathlib.Algebra.Star.Module

#18643

[Johan Commelin]

That's a very reasonable split :peace_sign:

[Johan Commelin]

Claiming

Mathlib/RingTheory/TensorProduct/Basic.lean     1270    84  [Mathlib.RingTheory.Finiteness]

[Anne Baanen]

Here's one I came across organically: the file defining docs#Finset.prod imports docs#Finset.sym2 (8 extra imports) on line 2260. #18650

[Kim Morrison]

Anne Baanen said:

Here's one I came across organically: the file defining docs#Finset.prod imports docs#Finset.sym2 (8 extra imports) on line 2260. #18650

Nice, 2600 files with 6 fewer imports.

[Damiano Testa]

Once the dust settles, we may consider adding a CI step on PRs that flags late importers just among the modified files.

[Johan Commelin]

Johan Commelin said:

Claiming

Mathlib/RingTheory/TensorProduct/Basic.lean     1270    84  [Mathlib.RingTheory.Finiteness]

#18653

[Johan Commelin]

Claiming

Mathlib/Algebra/Module/LocalizedModule.lean     1141    97  [Mathlib.Algebra.Exact]

[Johan Commelin]

chore: split Algebra.Module.LocalizedModule #18657

[switching to #mathlib4 > Late importers report now]

[Kevin Buzzard]

I just moved a few declarations from the end of a 1000-line-long file (Mathlib/Algebra/Group/Submonoid/Operations.lean) into a short new file in #21067 with fewer imports (in preparation for a minor refactor which is of no relevance here) and then I imported the short file back into the long file (the short file compiled without needing to import the long file). Then lake shake got very excited. Turns out that a couple of files in mathlib (Mathlib/GroupTheory/GroupAction/Defs.lean, Mathlib/GroupTheory/OreLocalization/Basic.lean) were importing the entire 1000-line-long file just because they needed those few declarations which I moved. This to me feels like the opposite of "late imports", it's more like "late exports", i.e. "this mathlib file imported a huge thing but all it really wanted was the independent bit at the end, which it possibly used throughout". Could one write a variant of the ideas being used in this thread to look for other instances of this phenomenon? Is there a chance that it could also be used to e.g. decrease the longest pole?

[Johan Commelin]

Is this (roughly) what you are looking for:

• loop over all declarations in a file
• for each decl d, find its immediate dependencies, by inspecting its type and value
• if none of these dependencies are declared in the same file, then d is a "late export"
• get excited if a "late export" occurs at line number > 500

[Damiano Testa]

For the purpose of refactoring, any declaration that does not depend on the previous ones is a potential candidate for being moved to a different file. So, it may be useful to simply flag "exports", not necessarily late. Then it is up to the human to figure out a reasonable cut-off for what counts as being "late enough to warrant a separate file".

[Damiano Testa]

(Or maybe, 500 lines could be the default, but it could be useful that the user has the option of providing a different number.)

[Johan Commelin]

Yeah, I think we should just flag all of them. But of course there is no use in getting excited about the first decl in the file being flagged.

[Kevin Buzzard]

My experience in developing is that sometimes you're working on a leaf file, or a file near the leaves, and you find some missing API which you need and which clearly should not be in the leafy file, so you think "OK I'll be a good citizen and put it in the right place", and then you decide that the right place maybe 1000 lines into some 1500-line-long file so you write a couple of lemmas and bung them in randomly. I've certainly done this before. The question is whether actually moving those lemmas into a new file makes the import tree nicer and it's not immediately obvious that it does, but lake shake convinced me that in this one example above I did.

I guess one issue with Johan's proposal is that the last theorem in a file will always be a late export. Maybe it would be more interesting to find declarations which are (a) in large files (b) at least 500 lines from the end (c) are not used in the rest of the large file (so are candidates for removal) (d) are used in another file and (e) there are only two or three declarations from the large file used in the other file.

Maybe the most naive question is this: can we find a file which imports a large file and the reason it does so is for precisely one theorem (say), and this one theorem it can be moved from the large file into a new file which doesn't need to import the large file? In other words, can we find theorems for which there is evidence that the theorem is "in the wrong file"?

[Johan Commelin]

@Kevin Buzzard No, the first declaration will always be a late export. (Unless I'm misunderstanding the algorithm I wrote down.) What I intend is that decls get flagged if they don't use anything from the file they are in.

[Kim Morrison]

Here's some data, from running Mathlib with set_option linter.upstreamableDecl true globally.

Here are the files with declaration after line 500 that doesn't depend on anything in the file: https://gist.github.com/kim-em/5e40320da4e9962208b4285bf6218d21

Here's the full output: https://gist.github.com/kim-em/a020497289a0ebeb1de7e49abdb36758

(@Johan Commelin)

[Kim Morrison]

@Damiano Testa, the upstreamableDecl linter would be much more useful if it did not flag any defs. Could we have that?

[Kim Morrison]

Or I guess have two variants upstreamableDecl with the current behaviour, and upstreamableThm which only flags theorems.

[Kim Morrison]

@Damiano Testa, it would also be helpful to not flag private declarations.

[Kim Morrison]

and, @Damiano Testa, while we're here, a bug report: set_option linter.upstreamableDecl true flags docs#MeasureTheory.Measure.le_add_left as movable to Mathlib.Algebra.Order.Monoid.Canonical.Defs, but that is clearly impossible as the signature of the theorem mentions MeasurableSpace.

(Arguably, this theorem shouldn't exist because it is a needless specialization, but nevertheless this linter report is incorrect.)

[Kim Morrison]

(This problem seems quite widespread in the report.)

[Damiano Testa]

Unflagging defs and private declarations is very easy and I can look into that, though likely not before Wednesday.

[Damiano Testa]

As for the bug, I will have to look again at the implementation to see what is going on.

[Damiano Testa]

Most of the linter was written by @Anne Baanen: flagging you, in case you are not already watching this! :smile:

[Anne Baanen]

I have some time now to add a upstreamableThm mode. (private should be excluded from both versions, right?)

[Damiano Testa]

Anne, why not add two separate options, one for private and one for def?

[Damiano Testa]

That would allow users to make a choice, based on the situation.

[Damiano Testa]

I think that def and private are by default not linted, but can be opt-in.

[Anne Baanen]

True, but I think the best default is to exclude private. Since even if you might want to upstream it, the downstream breaks easily.

[Anne Baanen]

Kim Morrison said:

(This problem seems quite widespread in the report.)

This is unfortunately a limitation of the syntax linter approach: we don't see any implicit arguments. So since the MeasurableSpace isn't listed explicitly, the linter doesn't realize it's required. And if the linter worked by terms, then we'd have shake's issue of missing out on all the tactics and notation...

[Anne Baanen]

#21374 adds two options: for including defs and for private decls.

[Kim Morrison]

Anne Baanen said:

Kim Morrison said:

(This problem seems quite widespread in the report.)

This is unfortunately a limitation of the syntax linter approach: we don't see any implicit arguments. So since the MeasurableSpace isn't listed explicitly, the linter doesn't realize it's required. And if the linter worked by terms, then we'd have shake's issue of missing out on all the tactics and notation...

Can't we do both?

[Anne Baanen]

I don't know enough about the linter framework to do so, but if you have a stub I can surely fill it out.

[Damiano Testa]

Actually, for theorems (as opposed to defs), the inclusion mechanism takes care of doing this for you: the variables that you see when you start the proof, are exactly the ones that make it into the environment constant.

[Damiano Testa]

So, it is hard to get reliable information about the variables used by a definition that make it into the environment, but the (in progress) unusedVariableCommand linter does a pretty good job with variables used in theorems.

[Damiano Testa]

#17715 is the linter. Let me narrow it down to something more specific!

[Damiano Testa]

includedVariables is a TermElabM function for getting the unique names of variables that a theorem uses.

[Damiano Testa]

If I remember correctly, the environment records enough correspondences between unique variable names, variable usernames and syntax to figure out most of the rest.

[Kim Morrison]

@Damiano Testa, I don't think this has anything to do with variables. The problem is just that upstreamableDecl is not looking at the type signature of the definition.

[Damiano Testa]

Ah, I see.

[Anne Baanen]

I talked with Kim and they came up with an approach to also include the type signature: we already determine the name/ConstInfo of the declaration being linted, so we can take the union of the "syntactically required modules" with docs#Lean.Name.requiredModules or docs#Lean.NameSet.transitivelyRequiredModules, to feed into irredundantImports.

[Damiano Testa]

Great, thanks! I have very little lean time this week, so I could not really look into this seriously!

[Anne Baanen]

I'll try this out sometime later this week, when I'm waiting for concrete categories to compile :)

[Anne Baanen]

It looks like docs#Mathlib.Command.MinImports.getAllDependencies already tries to figure out the decl name and uses that to inspect the terms (see also docs#Mathlib.Command.MinImports.getVisited). So maybe the issue is more that it can't reliably figure out names for declarations?

[Anne Baanen]

Indeed, it thinks protected theorem le_add_left refers to docs#le_add_left instead of docs#MeasureTheory.Measure.le_add_left.

[Anne Baanen]

I had to reimplement some of the elaboration logic (since that is interwoven with updating the environment, and would complain that the declaration already exists), but now it seems to work much more reliably to figure out declaration names from a bit of syntax!

[Anne Baanen]

Kim Morrison said:

and, Damiano Testa, while we're here, a bug report: set_option linter.upstreamableDecl true flags docs#MeasureTheory.Measure.le_add_left as movable to Mathlib.Algebra.Order.Monoid.Canonical.Defs, but that is clearly impossible as the signature of the theorem mentions MeasurableSpace.

(Arguably, this theorem shouldn't exist because it is a needless specialization, but nevertheless this linter report is incorrect.)

This now reports:

import Mathlib.MeasureTheory.Measure.NullMeasurable
import Init.Data.List.Nat.Pairwise

which seems much more realistic!

[Anne Baanen]

After a bit more fixing in upstreamableDecl: #21505

[Kim Morrison]

@Anne Baanen, I think the lines

    let skipDef := !Linter.getLinterValue linter.upstreamableDecl.defs (← getOptions)
    let skipPrivate := !Linter.getLinterValue linter.upstreamableDecl.private (← getOptions)

in UpstreamableDecl.lean count as a bug. Using Linter.getLinterValue means that if someone sets set_option linter.all true, then these options will be turned on.

[Anne Baanen]

Aha! We might not even want the linter.upstreamableDecl itself to be activated on linter.all, since its output is probably not very actionable in general?

[Ruben Van de Velde]

Arguably, this isn't a linter, its output is informational