Late importers report

Stream: mathlib4

[github mathlib4 bot]

File	Line	Import increase	New imports

Reference commit 72befe9d26
Full report

[Johan Commelin]

$\varnothing$ :cry:

[Damiano Testa]

Ok, all this work, only to find out that there are no late importers...

[Damiano Testa]

Anyway, this was a test run: I consider it successful, since it posted something on Zulip!

[Damiano Testa]

Hopefully, in a couple of hours, there will be a second test posted here, with actual data in it!

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	17	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Set/Lattice.lean	1810	70	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	67	[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/Data/Ordmap/Ordnode.lean	1208	10	[Mathlib.Data.List.Defs]
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]

---

Reference commit aa207a6a96
Full report

[Ruben Van de Velde]

Is Logic.Pairwise expected to be heavy?

[Johan Commelin]

From the POV of Data.Set.Lattice: yeahmzzomewhat?

[Ruben Van de Velde]

Oh it's pulling in Tactic.Basic despite not using a single tactic in the entire file

[Johan Commelin]

chore: split Algebra.Module.LocalizedModule #18657

[Johan Commelin]

@Damiano Testa It seems that the full report isn't really sorted, right?

[Damiano Testa]

It is sorted by reverse line number, to isolate the "later importers"...

[Damiano Testa]

Ah, the full report!

[Damiano Testa]

True, I forgot to sort the "Full report"!

[Damiano Testa]

Still, it looks like a lot of moving parts moved synchronously!

[Damiano Testa]

Damiano Testa said:

True, I forgot to sort the "Full report"!

Actually, looking at the code and the output, isn't also the full report sorted by "latest line with an import bump"?

[Damiano Testa]

One thing that I think would be useful is if the bash column command were available in CI, since piping the Full report through | column -s'|' -o'|' -t would display as

|File                                                       |Line  |Import increase|New imports                                                           |
|:-                                                         |-:    |-:             |:-                                                                    |
|  Mathlib/Data/Finset/Basic.lean                           | 3085 | 1             |  [Mathlib.Logic.Equiv.Set]                                           |
|  Mathlib/Topology/Algebra/Module/Basic.lean               | 2527 | 17            |  [Mathlib.Topology.Algebra.Group.Quotient]                           |
|  Mathlib/Analysis/InnerProductSpace/Basic.lean            | 2439 | 2             |  [Mathlib.Analysis.Normed.Module.Completion]                         |
|  Mathlib/Data/Multiset/Basic.lean                         | 2352 | 6             |  [Mathlib.Order.Hom.Basic]                                           |
|  Mathlib/Computability/TuringMachine.lean                 | 2297 | 1             |  [Init.Control.Lawful.Instances]                                     |
|  Mathlib/Algebra/BigOperators/Group/Finset.lean           | 2260 | 8             |  [Mathlib.Data.Finset.Sym, Mathlib.Data.Sym.Sym2.Order]              |
|  Mathlib/Data/List/Basic.lean                             | 2182 | 3             |  [Mathlib.Data.Prod.Basic]                                           |
|  Mathlib/SetTheory/Ordinal/Arithmetic.lean                | 2150 | 1             |  [Mathlib.Data.Nat.SuccPred]                                         |
|  Mathlib/Topology/Separation/Basic.lean                   | 2109 | 2             |  [Mathlib.Topology.Compactness.Lindelof]                             |
|  Mathlib/Data/Matrix/Basic.lean                           | 2063 | 1             |  [Mathlib.Algebra.Algebra.Opposite]                                  |
|  Mathlib/MeasureTheory/Integral/Lebesgue.lean             | 2044 | 1             |  [Mathlib.Topology.IndicatorConstPointwise]                          |
|  Mathlib/RingTheory/UniqueFactorizationDomain.lean        | 1972 | 3             |  [Mathlib.Data.Nat.Factors]                                          |
|  Mathlib/Analysis/Asymptotics/Asymptotics.lean            | 1947 | 4             |  [Mathlib.Topology.PartialHomeomorph]                                |
|  Mathlib/MeasureTheory/Function/LpSpace.lean              | 1907 | 1             |  [Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov]         |

...

which is much more readable than the current view.

[Bryan Gin-ge Chen]

While we should be wary of installing too much stuff on the Hoskinson machines, I can’t imagine that column or whatever package it’s included in would be too heavy.

[Damiano Testa]

According to google, running apt-get install bsdmainutils should install it, but I am not really sure how much extra stuff this implies.

[Johan Commelin]

I think I would like to see a subset of the full report where $line >= 500 && $increase >= 50 or something like that.

[Johan Commelin]

Can we do that easily? Or do we need to run the whole thing again?

[Damiano Testa]

All these filters can be done easily, thanks to the "replay" feature that lake has.

[Damiano Testa]

But they can only be done in CI with forethought, since CI does not save the cache for the run.

[Damiano Testa]

However, the logs contain all the information, so it can also be done locally after the fact, downloading the logs.

[Damiano Testa]

There you go:

File	Line	Import increase	New imports
Mathlib/Data/Set/Lattice.lean	1810	70	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	67	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/RingTheory/TensorProduct/Basic.lean	1270	84	[Mathlib.RingTheory.Finiteness]
Mathlib/Algebra/Module/LocalizedModule.lean	1141	97	[Mathlib.Algebra.Exact]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	519	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Tactic/Ring/Basic.lean	982	95	[Mathlib.Tactic.NormNum.Inv]
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean	513	255	[Mathlib.RingTheory.Localization.AtPrime]
Mathlib/LinearAlgebra/LinearDisjoint.lean	510	53	[Mathlib.LinearAlgebra.Dimension.Finite]
Mathlib/LinearAlgebra/DFinsupp.lean	506	88	[Mathlib.LinearAlgebra.LinearIndependent]
Mathlib/Data/Stream/Init.lean	501	269	[Mathlib.Data.List.Basic]

[Bryan Gin-ge Chen]

Damiano Testa said:

According to google, running apt-get install bsdmainutils should install it, but I am not really sure how much extra stuff this implies.

Maybe apt-get install bsdextrautils now? https://packages.debian.org/sid/bsdextrautils

Looks like it's most likely <1MB after installing so I'd say just go for it.

[Damiano Testa]

Actually, could I simply install it in CI? Or would I need to be root to do that?

[Bryan Gin-ge Chen]

I think you should be able to install it in CI? I thought we had some apt-get steps in other workflows (maybe running on GitHub hosted runners though).

[Damiano Testa]

Ok, I'll run an experiment later and see if I can do that.

[Johan Commelin]

I don't think it is worth splitting Mathlib/MeasureTheory/Covering/Besicovitch.lean

[Damiano Testa]

Johan Commelin said:

I don't think it is worth splitting Mathlib/MeasureTheory/Covering/Besicovitch.lean

Presumably, this assessment will stay valid for a fair amount of time: should there be a structured way of keeping track of these things other than just posting here?

[Johan Commelin]

Probably, but I'm not sure yet what we want exactly

[Damiano Testa]

A side comment: I do not think that I can install column in CI.

apt-get install bsdextrautils

  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
E: Could not open lock file /var/lib/dpkg/lock-frontend - open (13: Permission denied)
E: Unable to acquire the dpkg frontend lock (/var/lib/dpkg/lock-frontend), are you root?

[Edward van de Meent]

if this is using lean to produce strings, docs#formatTable may be usable?

[Damiano Testa]

The table is produced already in the shell stdout, and I would then have to pass it back into lean for formatting. Since the table is already in markdown format, it may not be worth the extra complication and I am tempted to leave the full report as is.

[Damiano Testa]

Anyone who wants to use it would have to pass it through some for of further filtering/processing, at which stage it is probably irrelevant that it is nicely formatted anyway.

[Edward van de Meent]

ah

[Damiano Testa]

Conclusion: you get a rendered markdown for a small selection of late importers here on Zulip, a full report that is markdown formatted, but not rendered in CI and you can download that to your computer and process it as you please. It is not too bad as a situation.

[Damiano Testa]

Are there any further requests/improvements to the "Late importers report"? On my side, there are no loose ends at the moment.

[Kim Morrison]

I guess if we had infinite programmer time:

1. If a merged PR touched one of the files in the most recent report, trigger the workflow again.
2. Show the diff relative to the last report. (Using zulip as the persistent state?)
3. Filenames could be links to github.

But likely there are better things to work on. :-)

[Damiano Testa]

3 is probably very easy to implement and I can do that probably right now.

[Damiano Testa]

2 I can probably recycle most of what is already done for the comparing of the "Technical Debts report": maybe a little longer than 3, but comparable in time.

[Damiano Testa]

1 is the one for which there is the least automation already available, I think.

[Bryan Gin-ge Chen]

Damiano Testa said:

A side comment: I do not think that I can install column in CI.

apt-get install bsdextrautils

  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
E: Could not open lock file /var/lib/dpkg/lock-frontend - open (13: Permission denied)
E: Unable to acquire the dpkg frontend lock (/var/lib/dpkg/lock-frontend), are you root?

Perhaps @Wojciech Nawrocki can arrange to have this added to the setup for the Hoskinson machines when he has a chance?

[Kim Morrison]

I don't think we should try to split Mathlib/Topology/Category/Profinite/Nobeling.lean. It's a leaf, and coherent.

[Damiano Testa]

If formatting via column can be achieved easily, it would make the link to the Full report more human-friendly. But for me, it is not a priority.

[Damiano Testa]

Kim Morrison said:

I don't think we should try to split Mathlib/Topology/Category/Profinite/Nobeling.lean. It's a leaf, and coherent.

In the long term, I think that this information should be collected somewhere, since it is valuable and might even be used to decide which late importers to display and which ones to filter out.

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Logic/Equiv/Defs.lean	810	17	[Mathlib.Data.Quot]
Mathlib/Tactic/GeneralizeProofs.lean	472	619	[Mathlib.Lean.Expr.Basic]
Mathlib/Tactic/TermCongr.lean	451	42	[Mathlib.Lean.Meta.CongrTheorems]
Mathlib/Data/Nat/Defs.lean	425	11	[Mathlib.Tactic.GCongr.Core]
Mathlib/Tactic/Linter/FlexibleLinter.lean	372	94	[Lean.Elab.Command]
Mathlib/Order/RelClasses.lean	323	30	[Mathlib.Order.Basic]
Mathlib/Tactic/Variable.lean	243	102	[Lean.Elab.Frontend, Lean.Elab.InheritDoc, Lean.Meta.Tactic.TryThis]
Mathlib/Order/Max.lean	203	27	[Mathlib.Order.Synonym]
Mathlib/Data/FunLike/Basic.lean	202	16	[Mathlib.Logic.Basic]
Mathlib/Tactic/CongrExclamation.lean	187	686	[Mathlib.Lean.Meta.CongrTheorems]
Mathlib/Logic/Unique.lean	167	27	[Mathlib.Logic.IsEmpty]
Mathlib/Tactic/Basic.lean	159	609	[Mathlib.Tactic.PPWithUniv]
Mathlib/Logic/Relator.lean	147	10	[Mathlib.Logic.Function.Defs]
Mathlib/Tactic/Common.lean	136	71	[Aesop.Frontend.Tactic]
Mathlib/Tactic/ExtractGoal.lean	133	52	[Lean.Elab.Tactic.ElabTerm]

---

Reference commit b652c00b39
Full report

[Damiano Testa]

Ok, the links are "almost" ok

[Damiano Testa]

I missed out on removing a space at the start.

[Damiano Testa]

(The data provided above was collected by running the script on approx 400 files, rather than on all of mathlib. The same will be true of the incoming report.)

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Logic/Equiv/Defs.lean	810	17	[Mathlib.Data.Quot]
Mathlib/Tactic/GeneralizeProofs.lean	472	619	[Mathlib.Lean.Expr.Basic]
Mathlib/Tactic/TermCongr.lean	451	42	[Mathlib.Lean.Meta.CongrTheorems]
Mathlib/Data/Nat/Defs.lean	425	11	[Mathlib.Tactic.GCongr.Core]
Mathlib/Tactic/Linter/FlexibleLinter.lean	372	94	[Lean.Elab.Command]
Mathlib/Order/RelClasses.lean	323	30	[Mathlib.Order.Basic]
Mathlib/Tactic/Variable.lean	243	102	[Lean.Elab.Frontend, Lean.Elab.InheritDoc, Lean.Meta.Tactic.TryThis]
Mathlib/Order/Max.lean	203	27	[Mathlib.Order.Synonym]
Mathlib/Data/FunLike/Basic.lean	202	16	[Mathlib.Logic.Basic]
Mathlib/Tactic/CongrExclamation.lean	187	686	[Mathlib.Lean.Meta.CongrTheorems]
Mathlib/Logic/Unique.lean	167	27	[Mathlib.Logic.IsEmpty]
Mathlib/Tactic/Basic.lean	159	609	[Mathlib.Tactic.PPWithUniv]
Mathlib/Logic/Relator.lean	147	10	[Mathlib.Logic.Function.Defs]
Mathlib/Tactic/Common.lean	136	71	[Aesop.Frontend.Tactic]
Mathlib/Tactic/ExtractGoal.lean	133	52	[Lean.Elab.Tactic.ElabTerm]

---

Reference commit b2147850ed
Full report

[Damiano Testa]

The file links now work.

[Kim Morrison]

Might as well jump right to the line number. :-)

[Kim Morrison]

(I think talking to AIs too much has meant that I am more prone to asking for little tweaks. :-)

[Damiano Testa]

Am I being subjected to a Turing test right now?

[Damiano Testa]

Actually, the line number is a little trickier, since it seems that the link uses a commit hash.

[Mario Carneiro]

ooh, rejecting a request, I think you passed the test

[Damiano Testa]

Let me show you my deep understanding of human nature by answering "No" to a user prompt.

[Damiano Testa]

Anyway, I added your items 1 and 2 above as todos in the CI workflow, and I consider "links to files" as done! :check:

[Edward van de Meent]

saying "No" is hard, ok? even hoomans have trouble sometimes.

[Damiano Testa]

As is, the workflow should post about two hours later than the "Technical Debt Counter" does.

[Damiano Testa]

The difference being CI time linting mathlib.

[Kim Morrison]

So looking a little further at this table, I think we might want to bias in favour of early files in Mathlib.

[Damiano Testa]

I posted code some time ago that would sort imports in the obvious way, so I can get that relatively easily. How would you like to skew the output?

[Kim Morrison]

Mathlib/LinearAlgebra/LinearDisjoint.lean and things downstream of it are easily splittable, but it is only three files from the end of Mathlib.

[Kim Morrison]

I think it would be a positive change, but epsilon impact.

[Kim Morrison]

Reporting "# of downstream files" might help?

[Kim Morrison]

And then perhaps we can add a cutoff (>=10?)

[Damiano Testa]

Sorting imports

[Damiano Testa]

Would this information be something that could be beneficial also for linter.minImports itself, or just for the report?

[Damiano Testa]

In the former case, I would add an option to the linter to make it report this information as well.

[Damiano Testa]

In the latter, I would pass the flagged files to ImportGraph and extract the information only in CI.

[Kim Morrison]

I haven't missed this information in linter.minImports.

[Damiano Testa]

In about 2h30, there may be a further test post by the script.

[github mathlib4 bot]

File	Line	Import increase	Downstream files	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	17	1093	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Set/Lattice.lean	1810	70	3621	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	67	2	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Topology/UniformSpace/Basic.lean	1617	22	1274	[Mathlib.Topology.Compactness.Compact, Init.Data.List.Nat.Pairwise]
Mathlib/Algebra/Order/Floor.lean	1583	12	1848	[Mathlib.Data.Int.Lemmas]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1414	11	392	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousMap/Bounded.lean	1390	24	300	[Mathlib.Analysis.CStarAlgebra.Basic]
Mathlib/RingTheory/Polynomial/Basic.lean	1233	24	980	[Mathlib.RingTheory.Polynomial.Content]
Mathlib/Data/Ordmap/Ordnode.lean	1208	10	3	[Mathlib.Data.List.Defs]
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean	1207	10	36	[Init.Data.ULift, Mathlib.LinearAlgebra.FiniteDimensional, Init.Data.Fin.Fold]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	713	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Module/LocalizedModule.lean	1187	97	131	[Mathlib.Algebra.Exact]
Mathlib/Algebra/Order/Module/Defs.lean	1173	22	1887	[Mathlib.Tactic.Positivity.Core]
Mathlib/GroupTheory/FreeGroup/Basic.lean	1145	31	203	[Mathlib.Data.Fintype.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1140	19	2	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1092	18	2	[Mathlib.Data.Num.Lemmas]

---

Reference commit 94a35d642c
Full report

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bryan Gin-ge Chen said:

Damiano Testa said:

A side comment: I do not think that I can install column in CI.

apt-get install bsdextrautils

  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
E: Could not open lock file /var/lib/dpkg/lock-frontend - open (13: Permission denied)
E: Unable to acquire the dpkg frontend lock (/var/lib/dpkg/lock-frontend), are you root?

Perhaps Wojciech Nawrocki can arrange to have this added to the setup for the Hoskinson machines when he has a chance?

Should be done now.

[Damiano Testa]

Wojciech, thank you very much! I'll test it out later and will let you know if I have any problems!

[Damiano Testa]

The Downstrean files column of the latest report is still experimental: it is part of a test PR, but not of the "main" one.

[Damiano Testa]

Just a confirmation: column works and this is a sample report

| File                                                                                                                                    | Line | Import increase | New imports           |
| :-                                                                                                                                      | -:   | -:              | :-                    |
| [Mathlib/Tactic/Simps/NotationClass.lean](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Simps/NotationClass.html) | 48   | 42              | [Batteries.Lean.Expr] |
| [Mathlib/Init.lean](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init.html)                                             | 14   | 261             | [Lean.Parser.Command] |
---
Reference commit [fbab0d1c46](https://github.com/leanprover-community/mathlib4/commit/fbab0d1c46cf266cc07744160d87347000fb15f8)
[Full report](https://github.com/leanprover-community/mathlib4/actions/runs/11702874889)

Of course, the lines are really long, but at least the columns are aligned now!

[Bryan Gin-ge Chen]

Any other comments on the content / formatting of the report? Otherwise I think #18631 is ready.

[Kim Morrison]

:peace_sign:

[Damiano Testa]

The automatic posting of the report has just been merged! Ideally, on Monday, the bot will post here the outcome!

[Damiano Testa]

The script that has been merged is still not printing the number of downstream files that each entry has, since I'm still not convinced by the prototype that I have.

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	17	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/RingTheory/UniqueFactorizationDomain.lean	2015	140	[Mathlib.RingTheory.Noetherian]
Mathlib/Data/Set/Lattice.lean	1810	70	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	67	[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/MeasureTheory/MeasurableSpace/Basic.lean	1473	11	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousMap/Bounded.lean	1390	24	[Mathlib.Analysis.CStarAlgebra.Basic]
Mathlib/RingTheory/Polynomial/Basic.lean	1233	23	[Mathlib.RingTheory.Polynomial.Content]
Mathlib/Data/Ordmap/Ordnode.lean	1208	10	[Mathlib.Data.List.Defs]
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	23	[Mathlib.Tactic.Positivity.Core]
Mathlib/GroupTheory/FreeGroup/Basic.lean	1145	31	[Mathlib.Data.Fintype.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1140	19	[Mathlib.Tactic.NormNum.Pow]

---

Reference commit 006c0fc200
Full report

[Damiano Testa]

It worked!! :octopus:

[Anne Baanen]

Mathlib/RingTheory/UniqueFactorizationDomain.lean 2015 140 [Mathlib.RingTheory.Noetherian]

Fixed en passant in #18734 :)

[Ruben Van de Velde]

I'm looking at Polynomial

[Ruben Van de Velde]

Ruben Van de Velde said:

I'm looking at Polynomial

#18875

[Ruben Van de Velde]

And some more in #18883

[Damiano Testa]

The import summary that gets posted on each PR reports per-file information about the change in number of transitive imports. This is great for most PRs, however, for PRs that target specifically reducing the number of imports, it would probably also be useful to have a global number that would ideally decrease in such a PR.

[Damiano Testa]

Possibly the total number of "import edges" either including or excluding transitively implied edges in mathlib would be a good such measure?

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	18	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Set/Lattice.lean	1816	70	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	60	[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	11	[Mathlib.Data.Int.Lemmas]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1473	18	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousOn.lean	1409	12	[Mathlib.Algebra.Group.Indicator]
Mathlib/Topology/ContinuousMap/Bounded.lean	1390	29	[Mathlib.Analysis.CStarAlgebra.Basic]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Order/Module/Defs.lean	1173	23	[Mathlib.Tactic.Positivity.Core]
Mathlib/GroupTheory/FreeGroup/Basic.lean	1144	44	[Mathlib.Data.Fintype.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1141	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1092	18	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	542	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1066	44	[Mathlib.Data.Set.Pointwise.SMul]

---

Reference commit 25f427c356
Full report

[Kim Morrison]

Claiming ContinuousMap/Bounded ---> #19187

[Kim Morrison]

Claiming Topology/UniformSpace/Basic ---> #19194

[Ruben Van de Velde]

Is Besicovitch worthwhile?

[Johan Commelin]

Nope. Everything after Besicovitch depends on the 2nd half of the file.

[Ruben Van de Velde]

I guess at most the first half could be compiled in parallel with some of its imports, unless the first half needs them all

[Johan Commelin]

Hmmm, that might be true...

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	18	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Set/Lattice.lean	1816	84	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	57	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1472	18	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousOn.lean	1409	12	[Mathlib.Algebra.Group.Indicator]
Mathlib/Topology/UniformSpace/Basic.lean	1336	13	[Mathlib.Topology.ContinuousOn]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	23	[Mathlib.Tactic.Positivity.Core]
Mathlib/GroupTheory/FreeGroup/Basic.lean	1144	45	[Mathlib.Data.Fintype.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1092	18	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	550	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1057	29	[Mathlib.Data.Set.Pointwise.SMul]

---

Reference commit 386ab515e2
Full report

[Johan Commelin]

There doesn't seem to be much low-hanging fruit in this table anymore.

[Damiano Testa]

Maybe the bot should somehow report different parts of the full report?

[Johan Commelin]

If the new import is a tactic, I'm doubtful we should split for that reason.

[Johan Commelin]

And if we can have a mechanism to whitelist some entries (like Besicovitch) that would also improve the list.

[Damiano Testa]

Manually adding exceptions via PRs to the shell script should be straightforward.

[Kim Morrison]

I don't know... without actually looking at the files:

• does FreeGroup/Basic have a natural split where we started thinking about finiteness?
• UniformSpace/Basic is still a huge file, surely it splits? Similarly for MeasurableSpace/Basic?
• why not split off material about quotients from Topology/Algebra/Module/Basic?
• Data/Set/Lattice could have material about intervals or disjointness moved to a separate file

[Johan Commelin]

You are right. We should still split, if only because the files are really long. But the "import increase" is no longer a very exciting number. (Except for the FreeGroup/Basic entry. That one is certainly a target.)

[Johan Commelin]

I'll work on FreeGroup/Basic now.

[Johan Commelin]

#19501

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	18	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Data/Set/Lattice.lean	1816	84	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1756	58	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1472	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousOn.lean	1409	12	[Mathlib.Algebra.Group.Indicator]
Mathlib/Topology/UniformSpace/Basic.lean	1336	13	[Mathlib.Topology.ContinuousOn]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	23	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1092	19	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	472	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1057	29	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/Tactic/Ring/Basic.lean	982	99	[Mathlib.Tactic.NormNum.Inv]

---

Reference commit dde4f2ecae
Full report

[Ruben Van de Velde]

The fact that Mathlib/Topology/Algebra/Module/Basic.lean even has a line 2527 suggests it might be worth splitting :)

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	18	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Computability/TuringMachine.lean	2128	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1818	84	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	58	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1584	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/ContinuousOn.lean	1409	12	[Mathlib.Algebra.Group.Indicator]
Mathlib/Topology/UniformSpace/Basic.lean	1340	13	[Mathlib.Topology.ContinuousOn]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	42	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1094	19	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	474	[Mathlib.MeasureTheory.Covering.Differentiation]

---

Reference commit 65c00859d0
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Algebra/Module/Basic.lean	2527	18	[Mathlib.Topology.Algebra.Group.Quotient]
Mathlib/Computability/TuringMachine.lean	2128	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1818	85	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	58	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1584	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	19	[Mathlib.Order.LiminfLimsup]
Mathlib/FieldTheory/Adjoin.lean	1289	11	[Mathlib.FieldTheory.Separable]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	21	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	42	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1094	19	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	449	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1057	30	[Mathlib.Data.Set.Pointwise.SMul]

---

Reference commit 3f813de52d
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Computability/TuringMachine.lean	2127	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1864	85	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	58	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1584	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Order/Basic.lean	1373	10	[Mathlib.Algebra.Group.ZeroOne]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	42	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1094	19	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1073	444	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1057	30	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1055	35	[Mathlib.LinearAlgebra.Projection]

---

Reference commit e820917259
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Computability/TuringMachine.lean	2127	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1864	85	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	74	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1584	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Order/Basic.lean	1380	10	[Mathlib.Algebra.Group.ZeroOne]
Mathlib/Data/Ordmap/Ordnode.lean	1208	11	[Mathlib.Data.List.Defs]
Mathlib/Topology/PartialHomeomorph.lean	1191	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	42	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1142	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1094	19	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1072	443	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1057	30	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1055	35	[Mathlib.LinearAlgebra.Projection]

---

Reference commit b4e6697e70
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Data/Multiset/Basic.lean	2360	10	[Mathlib.Order.Hom.Basic]
Mathlib/Computability/TuringMachine.lean	2128	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1864	86	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1834	74	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean	1613	179	[Mathlib.Analysis.Convex.Normed]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1491	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Order/Basic.lean	1390	10	[Mathlib.Algebra.Group.ZeroOne]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1368	30	[Mathlib.Analysis.Calculus.Deriv.Comp, Mathlib.Analysis.Calculus.Deriv.Mul, Mathlib.Analysis.Normed.Module.Dual]
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	1349	10	[Mathlib.Algebra.GroupWithZero.Units.Basic]
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean	1243	12	[Mathlib.Topology.MetricSpace.Polish, Mathlib.MeasureTheory.Measure.Haar.Unique]
Mathlib/MeasureTheory/Function/L1Space.lean	1222	20	[Mathlib.MeasureTheory.Function.LpSpace]
Mathlib/Topology/PartialHomeomorph.lean	1216	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Analysis/Calculus/MeanValue.lean	1191	168	[Mathlib.Analysis.Convex.Normed]
Mathlib/Analysis/Normed/Group/Basic.lean	1185	15	[Mathlib.Topology.Sequences, Mathlib.Topology.Metrizable.Uniformity, Mathlib.Algebra.Group.Subgroup.Ker]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	24	[Mathlib.Algebra.Star.SelfAdjoint]

---

Reference commit 95cdc7a6ab
Full report

[Ruben Van de Velde]

Should Data.Multiset.Basic import from Order? I wonder if @Yaël Dillies has thoughts on that

[Yaël Dillies]

My thoughts: #19775

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Data/List/Basic.lean	2221	65	[Mathlib.Data.Prod.Basic]
Mathlib/Computability/TuringMachine.lean	2128	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/Data/Set/Lattice.lean	1869	87	[Mathlib.Logic.Pairwise]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1834	76	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Data/Set/Basic.lean	1703	14	[Mathlib.Tactic.Tauto]
Mathlib/Geometry/Manifold/IsManifold.lean	1675	182	[Mathlib.Analysis.Convex.Normed]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1491	19	[Mathlib.Order.LiminfLimsup]
Mathlib/Order/Basic.lean	1390	10	[Mathlib.Algebra.Group.ZeroOne]
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	1349	10	[Mathlib.Algebra.GroupWithZero.Units.Basic]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1322	25	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1216	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Analysis/Normed/Group/Basic.lean	1185	15	[Mathlib.Topology.Sequences, Mathlib.Topology.Metrizable.Uniformity, Mathlib.Algebra.Group.Subgroup.Ker]
Mathlib/Analysis/Calculus/MeanValue.lean	1182	171	[Mathlib.Analysis.Convex.Normed]
Mathlib/Tactic/ToAdditive/Frontend.lean	1179	56	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	26	[Mathlib.Algebra.Star.SelfAdjoint]

---

Reference commit 039d0c7642
Full report

[Damiano Testa]

There reports spurred some very productive activity when they started. However, it seems that all the "easy" splits have been made and not many new easy splits have surfaced.

[Damiano Testa]

Is there some suggestion for some change to make these reports more useful? The full report contains more ideas of files to split, but is "hidden" behind the link.

[Damiano Testa]

Though maybe there are some small tweaks to the heuristics for the report that would expose some more useful data?

[Anne Baanen]

Mathlib/Data/List/Basic.lean 2221 65 [Mathlib.Data.Prod.Basic]

This seems like a very good candidate with some nice downstream effects too.

[Anne Baanen]

I had been ignoring the report because nothing appeared particularly exciting. And some files like [Mathlib/MeasureTheory/Covering/Besicovitch.lean](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Covering/Besicovitch.html) were deemed to be already ok. So the report stayed the same for a while. But now everything seems to have changed quite a bit in the past weeks. Do we already have a nolint equivalent for this report, that excludes Besicovich.lean?

[Damiano Testa]

There is no "nolints" for this report. Part of the reason for this is that I was not sure what to use:

• a nolint, excluding manually files that have already been considered to be ok,
• report the difference with the previous week, so that each "old" file gets a chance every other week to be split, and each modified file also gets a chance.

Pros of the manual nolint is that you can avoid seeing a file "forever".
Pros of the "display the difference" is that there is no human intervention needed.

[Damiano Testa]

Of course, implementing both is also an option, but they can be independent of each other.

[Anne Baanen]

Anne Baanen said:

Mathlib/Data/List/Basic.lean 2221 65 [Mathlib.Data.Prod.Basic]

This seems like a very good candidate with some nice downstream effects too.

Opened #20702 but shaking only gives a very modest import reduction of 3 instead of 65 transitive imports (which the minImports linter agrees with). Or how should I be interpreting this?

[Johan Commelin]

@Damiano Testa I like your "automated" proposal. Of course it requires maintaining a bit of state... how easy is it to scrape last weeks report? Or would you just recompute it?

[Damiano Testa]

I was thinking of reusing some of the infrastructure for the tech debts report that also compares the previous week's report to this week's. I do not remember how that one works, though... :man_facepalming:

[Damiano Testa]

In the case of this linter, recomputing it is not a viable option: the linter runs for a good 2-3hrs to generate the report.

[Damiano Testa]

I misremember: the tech debt report computes the old and the new absolute values and compares the two. Those checks are very cheap.

[Damiano Testa]

In this case, I would probably try to write a script that reads off the "Full report" that the linter outputs as a CI step and compare the old CI run with the new one.

[Anne Baanen]

Mathlib/Data/Set/Lattice.lean 1869 87 [Mathlib.Logic.Pairwise]

This one is because Logic.Pairwise unnecessarily imports Tactic.Common. Let me see if I can shake those imports...

[Kim Morrison]

I think I prefer a manual nolint, but would prefer if we could store that data outside the repo.

[Kim Morrison]

Can we just scrape a wiki page (and include the link in the report)?

[Anne Baanen]

Anne Baanen said:

This one is because Logic.Pairwise unnecessarily imports Tactic.Common. Let me see if I can shake those imports...

#20710 gets some big exciting reductions by delaying the import of Tactic.Common.

[Yaël Dillies]

Do we really want to delay importing Tactic.Common? Without it, we can't do things like #min_imports which I find quite incapacitating

[Johan Commelin]

I really wish one could have an "import overlay".
If I open a file in my editor, then Lean is going to elaborate it anyway. So it should just append import Mathlib.Tactic.Common to the imports, and maybe a few other things as well.

[Johan Commelin]

That way we can store the actual minimal dependencies of a file, but still have nice search tactics and other goodies available while editing.

[Violeta Hernández]

There should be a way to silence a file appearing on the report, I think. For instance, SetTheory/Ordinal/Notation makes very little sense to split. It defines a basic data structure which intends to match the ordinals, then proves that it matches them, of course it's going to import ordinals near the very end!

[Violeta Hernández]

(of course we could split data and proofs here, but this file has always been intended as a self-contained leaf file, so I think this doesn't make much sense)

[Kim Morrison]

I disagree, there is a natural split into Basic and Repr, at line 1158.

On the other hand, this file has been a leaf file since 2018.

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Data/Multiset/Basic.lean	2245	10	[Mathlib.Order.Hom.Basic]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1834	79	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Geometry/Manifold/IsManifold.lean	1675	186	[Mathlib.Analysis.Convex.Normed]
Mathlib/Computability/TuringMachine.lean	1546	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1491	18	[Mathlib.Order.LiminfLimsup]
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	1361	10	[Mathlib.Algebra.GroupWithZero.Units.Basic]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1322	25	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/MeasureTheory/Function/L1Space.lean	1232	19	[Mathlib.MeasureTheory.Function.LpSpace]
Mathlib/Topology/PartialHomeomorph.lean	1216	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Analysis/Normed/Group/Basic.lean	1185	15	[Mathlib.Topology.Sequences, Mathlib.Topology.Metrizable.Uniformity, Mathlib.Algebra.Group.Subgroup.Ker]
Mathlib/Analysis/Calculus/MeanValue.lean	1182	173	[Mathlib.Analysis.Convex.Normed]
Mathlib/Tactic/ToAdditive/Frontend.lean	1179	56	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	26	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean	1168	18	[Mathlib.Topology.UniformSpace.Compact]

---

Reference commit 14f0a13820
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Data/Multiset/Basic.lean	2245	10	[Mathlib.Order.Hom.Basic]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1834	79	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/Geometry/Manifold/IsManifold.lean	1727	187	[Mathlib.Analysis.Convex.Normed]
Mathlib/Data/Set/Basic.lean	1717	14	[Mathlib.Tactic.Tauto]
Mathlib/Computability/TuringMachine.lean	1549	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1491	20	[Mathlib.Order.LiminfLimsup]
Mathlib/Order/UpperLower/Basic.lean	1383	93	[Mathlib.Order.Interval.Set.OrdConnected]
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	1360	10	[Mathlib.Algebra.GroupWithZero.Units.Basic]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1339	25	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/MeasureTheory/Function/L1Space.lean	1271	20	[Mathlib.MeasureTheory.Function.LpSpace]
Mathlib/Topology/PartialHomeomorph.lean	1216	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Analysis/Calculus/MeanValue.lean	1182	173	[Mathlib.Analysis.Convex.Normed]
Mathlib/Tactic/ToAdditive/Frontend.lean	1179	56	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	26	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]

---

Reference commit a02b5327b9
Full report

[Johan Commelin]

Looks like

Mathlib/Order/UpperLower/Basic.lean -- 1383 -- 93 -- [Mathlib.Order.Interval.Set.OrdConnected]

is a new entry on the list, where we can get some substantial gains.

[Yaël Dillies]

It was recently introduced by @Bhavik Mehta. There are plenty of ways to reduce the imports back

[Bhavik Mehta]

Interesting - the change I made added 14 new imports to a file, I'm surprised that's making it show up on this list. But I agree there are substantial gains available around this.

[Yaël Dillies]

Basically the issue is that Algebra.Group.Support imports Order.Cover (fine) which itself imports Data.Set.OrdConnected (not fine, at least in the presence of the previous import)

[Yaël Dillies]

It would help a lot if we could sort the Order folder into broad categories, similar to how we got Algebra.Group, Algebra.GroupWithZero, Algebra.Ring, Algebra.Field. Eg maybe we could have

• Preorder, PartialOrder, LinearOrder (CovBy would live here)
• Lattice, BooleanAlgebra
• CompleteLattice, CompleteBooleanAlgebra (Set.OrdConnected would live here)

[Bhavik Mehta]

Why would Set.OrdConnected be in Complete*? I'd guess that belongs in the first category - intervals in an order don't seem to depend on any sSup or sInf properties

[Yaël Dillies]

Right. I guess what would belong in that last category are the lemmas about Set.OrdConnected + Set.iUnion

[Bhavik Mehta]

Yaël Dillies said:

Basically the issue is that Algebra.Group.Support imports Order.Cover (fine) which itself imports Data.Set.OrdConnected (not fine, at least in the presence of the previous import)

Interesting - what's the reason then that my 14 new imports caused a jump of 90 imports in the report above?

[Yaël Dillies]

... because there were already 76 late importers?

[Damiano Testa]

Bhavik Mehta said:

Interesting - the change I made added 14 new imports to a file, I'm surprised that's making it show up on this list. But I agree there are substantial gains available around this.

The criteria for admission in this list are:

• the last import increase exceeds 10 imports;
• the file appears in the top '15' exceptions, ranked by biggest line where the last import bump appears.

The Full report has neither of these filters.

[Bhavik Mehta]

I'm not sure I follow - in the previous Full report, that file had 3 late importers, and in the new report it has 93, ie a change of 90.

[Damiano Testa]

One thing that I am thinking now, is that this is based on the minImports linter that was required to disable Elab.async to work.

[Damiano Testa]

I wonder if this could have created some issues with the CI run as well.

[Bhavik Mehta]

Yaël Dillies said:

... because there were already 76 late importers?

Specifically the previous Full report shows that line 1383 causes an import increase of 3, but the new one shows that line 1383 causes an import increase of 93. And my question is how increasing the imports to a file by 14 can cause this change. Could you explain for me where the 76 comes from?

[Damiano Testa]

I specifically added a #import_bumps command that sets both the minImports option and the Elab.sync option to the correct values, but I do not think that this has had any effect on the CI run.

[Damiano Testa]

using #import_bumps on the file, the last report is

Basic.lean:1378:0
Imports increased by 4 to
[Mathlib.Order.Interval.Set.OrdConnected, Mathlib.Order.Interval.Set.OrderIso]

New imports: [Mathlib.Order.Interval.Set.OrdConnected]

Now redundant: [Mathlib.Order.Interval.Set.OrderEmbedding, Mathlib.Data.Set.Lattice, Mathlib.Data.SetLike.Basic]

[Damiano Testa]

So, I suspect that the run above of the report may have been affected by Elab.async (besides whatever further possible issues may have happened in the meanwhile).

[Damiano Testa]

If you decide to modify some file based on the output above, place #import_bumps at the beginning of the file, before blindly believing the report!

[Damiano Testa]

(If you use set_option linter.minImports true you should get a warning to use #import_bumps, so as long as you remember one of the commands, you are good!)

[Damiano Testa]

#21147 should make the weekly report use Elab.async to get the "correct" late importer information.

[Damiano Testa]

The workflow with Elab.async has been merged and I just manually triggered it in CI: in a few hours, the bot should post the message again, this time hopefully with correct information.

[Damiano Testa]

You can follow its process here (although it is not terribly exciting...)

[Bhavik Mehta]

Huh, interestingly that's different still. The corresponding line from the earlier discussion seems to be:

2025-01-28T00:22:01.4229388Z warning: ././././Mathlib/Order/UpperLower/Basic.lean:1378:0: Imports increased by 4 to
2025-01-28T00:22:01.4229795Z [Mathlib.Order.Interval.Set.OrdConnected, Mathlib.Order.Interval.Set.OrderIso]
2025-01-28T00:22:01.4230028Z
2025-01-28T00:22:01.4230157Z New imports: [Mathlib.Order.Interval.Set.OrdConnected]

Note that the new import of Mathlib.Order.Interval.Set.OrdConnected is the one that was causing an increase of 93 before.

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	79	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1580	12	[Mathlib.Data.Set.Countable]
Mathlib/Computability/TuringMachine.lean	1549	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	20	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/PartialHomeomorph.lean	1191	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1179	56	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	26	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1132	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1090	22	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1077	431	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1058	30	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1055	38	[Mathlib.LinearAlgebra.Projection]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	75	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]
Mathlib/Order/OmegaCompletePartialOrder.lean	990	38	[Mathlib.Dynamics.FixedPoints.Basic]

---

Reference commit ffa9869ea0
Full report

[Damiano Testa]

Bhavik, at least "your" file is no longer in the spotlight!

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	82	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1580	12	[Mathlib.Data.Set.Countable]
Mathlib/Computability/TuringMachine.lean	1549	11	[Mathlib.Data.Fintype.Option, Mathlib.Data.Fintype.Pi, Mathlib.Data.Fintype.Prod]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1474	20	[Mathlib.Order.LiminfLimsup]
Mathlib/Algebra/Order/Floor.lean	1374	11	[Mathlib.Data.Int.Lemmas]
Mathlib/Topology/PartialHomeomorph.lean	1191	20	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1179	56	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	28	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1132	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Computability/TMToPartrec.lean	1090	22	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1080	435	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1058	30	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1055	32	[Mathlib.LinearAlgebra.Projection]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	75	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]

---

Reference commit 8926633ff2
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean	1903	44	[Mathlib.Algebra.Order.Ring.Nat]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	83	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1580	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1479	20	[Mathlib.Order.LiminfLimsup]
Mathlib/Algebra/Order/Floor.lean	1365	11	[Mathlib.Data.Int.Lemmas]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1266	27	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1191	23	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1183	57	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	28	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1132	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1093	32	[Mathlib.LinearAlgebra.Projection]
Mathlib/Analysis/Normed/Group/Basic.lean	1093	35	[Mathlib.Data.NNReal.Basic]
Mathlib/Computability/TMToPartrec.lean	1090	22	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1080	438	[Mathlib.MeasureTheory.Covering.Differentiation]

---

Reference commit e2ee0aa168
Full report

[Damiano Testa]

Welcome back!

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean	1903	44	[Mathlib.Algebra.Order.Ring.Nat]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	83	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1580	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1496	20	[Mathlib.Order.LiminfLimsup]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1266	27	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1191	25	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1183	57	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1174	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Analysis/Normed/Group/Basic.lean	1108	36	[Mathlib.Data.NNReal.Basic]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	32	[Mathlib.LinearAlgebra.Projection]
Mathlib/Computability/TMToPartrec.lean	1090	22	[Mathlib.Data.Num.Lemmas]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1080	441	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Data/Fintype/Card.lean	1078	38	[Mathlib.Data.Finset.Union]

---

Reference commit c6a7350729
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean	1903	44	[Mathlib.Algebra.Order.Ring.Nat]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	84	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1580	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1495	20	[Mathlib.Order.LiminfLimsup]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1266	28	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1218	25	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1183	57	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1177	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Analysis/Normed/Group/Basic.lean	1108	36	[Mathlib.Data.NNReal.Basic]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	32	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1080	444	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1059	32	[Mathlib.Data.Set.Pointwise.SMul]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	81	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]

---

Reference commit 5e2e7342a4
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean	1904	46	[Mathlib.Algebra.Order.Ring.Nat]
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	85	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1592	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1495	25	[Mathlib.Order.LiminfLimsup]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1266	28	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1229	25	[Mathlib.Topology.Sets.Opens]
Mathlib/Data/DFinsupp/Defs.lean	1195	12	[Mathlib.Algebra.Group.Prod]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1185	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Tactic/ToAdditive/Frontend.lean	1183	57	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Analysis/Normed/Group/Basic.lean	1108	37	[Mathlib.Data.NNReal.Basic]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	33	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1086	448	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1059	28	[Mathlib.Data.Set.Pointwise.SMul]

---

Reference commit 45a9aacac4
Full report

[Anne Baanen]

I think it's time to tackle Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean, given that it is very long and also seems to be used all over the place. And Mathlib/Data/DFinsupp/Defs.lean is a good file to split in any case.

[Yaël Dillies]

I'll look at the pointwise file

[Yaël Dillies]

Actually, I am already splitting it up in #22333

[Johan Commelin]

That needs a few more fix commits (-;

[Yaël Dillies]

It's close to being mergeable! Anyone for a review?

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	85	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1623	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1507	22	[Mathlib.Order.LiminfLimsup]
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean	1266	28	[Mathlib.Analysis.Calculus.Deriv.Mul]
Mathlib/Topology/PartialHomeomorph.lean	1229	25	[Mathlib.Topology.Sets.Opens]
Mathlib/Data/DFinsupp/Defs.lean	1212	11	[Mathlib.Algebra.Group.Prod]
Mathlib/Tactic/ToAdditive/Frontend.lean	1185	59	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1185	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	33	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1086	452	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/Order/Filter/Pointwise.lean	1059	13	[Mathlib.Algebra.Group.Action.Pointwise.Set.Basic]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	77	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]
Mathlib/Tactic/Ring/Basic.lean	983	58	[Mathlib.Tactic.NormNum.Inv]

---

Reference commit 63a7be57d4
Full report

[David Loeffler]

I am working on a PR to split up MeasureTheory.Integral.FundThmCalculus. (The file is over-long anyway, and has a natural splitting point, but ironically the late import is one of the last few lemmas in the first half; fortunately the proof can be rejigged to avoid the extra import.)

[David Loeffler]

PR #22788 – ready for review now.

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1754	87	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/SetTheory/Cardinal/Basic.lean	1623	12	[Mathlib.Data.Set.Countable]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1505	22	[Mathlib.Order.LiminfLimsup]
Mathlib/Topology/PartialHomeomorph.lean	1230	25	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1185	59	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1185	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	33	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1086	468	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	77	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]
Mathlib/Tactic/Ring/Basic.lean	983	58	[Mathlib.Tactic.NormNum.Inv]
Mathlib/GroupTheory/Perm/Cycle/Basic.lean	971	11	[Mathlib.Algebra.Module.BigOperators]
Mathlib/Analysis/Normed/Lp/PiLp.lean	962	36	[Mathlib.LinearAlgebra.Matrix.Basis]
Mathlib/Topology/Algebra/Group/Basic.lean	943	119	[Init.Data.List.Nat.Pairwise, Mathlib.Algebra.Order.Archimedean.Basic]

---

Reference commit d27bbbade6
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	81	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1505	22	[Mathlib.Order.LiminfLimsup]
Mathlib/Computability/Primrec.lean	1333	22	[Mathlib.Logic.Encodable.Pi]
Mathlib/Topology/PartialHomeomorph.lean	1230	24	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1185	59	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1185	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	44	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Basic.lean	1158	63	[Mathlib.SetTheory.Cardinal.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	35	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1086	495	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	76	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]
Mathlib/Tactic/Ring/Basic.lean	983	54	[Mathlib.Tactic.NormNum.Inv]
Mathlib/Analysis/Normed/Lp/PiLp.lean	983	37	[Mathlib.LinearAlgebra.Matrix.Basis]
Mathlib/GroupTheory/Perm/Cycle/Basic.lean	971	11	[Mathlib.Algebra.Module.BigOperators]

---

Reference commit 524e5aa6c2
Full report

[github mathlib4 bot]

File	Line	Import increase	New imports
Mathlib/Topology/Category/Profinite/Nobeling.lean	1755	81	[Mathlib.Algebra.Category.ModuleCat.Free]
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean	1505	23	[Mathlib.Order.LiminfLimsup]
Mathlib/Computability/Primrec.lean	1333	23	[Mathlib.Logic.Encodable.Pi]
Mathlib/Topology/PartialHomeomorph.lean	1230	24	[Mathlib.Topology.Sets.Opens]
Mathlib/Tactic/ToAdditive/Frontend.lean	1185	59	[Batteries.Tactic.Trans, Mathlib.Tactic.Eqns, Lean.Elab.Tactic.Ext, Lean.Meta.Tactic.Rfl, Lean.Meta.Tactic.Symm, Mathlib.Tactic.Simps.Basic]
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean	1185	31	[Mathlib.Algebra.Star.SelfAdjoint]
Mathlib/Algebra/Order/Module/Defs.lean	1173	48	[Mathlib.Tactic.Positivity.Core]
Mathlib/SetTheory/Ordinal/Basic.lean	1158	61	[Mathlib.SetTheory.Cardinal.Basic]
Mathlib/SetTheory/Ordinal/Notation.lean	1134	18	[Mathlib.Tactic.NormNum.Pow]
Mathlib/Topology/Algebra/Module/LinearMap.lean	1095	35	[Mathlib.LinearAlgebra.Projection]
Mathlib/MeasureTheory/Covering/Besicovitch.lean	1086	495	[Mathlib.MeasureTheory.Covering.Differentiation]
Mathlib/CategoryTheory/Monoidal/Functor.lean	992	76	[Mathlib.CategoryTheory.Adjunction.FullyFaithful]
Mathlib/Tactic/Ring/Basic.lean	983	51	[Mathlib.Tactic.NormNum.Inv]
Mathlib/Analysis/Normed/Lp/PiLp.lean	983	37	[Mathlib.LinearAlgebra.Matrix.Basis]
Mathlib/GroupTheory/Perm/Cycle/Basic.lean	961	11	[Mathlib.Algebra.Module.BigOperators]

---

Reference commit f8f8d42d40
Full report

[Damiano Testa]

The bot was silent this week.