Zulip Chat Archive

Stream: mathlib4

Topic: The long pole in mathlib


Bolton Bailey (Apr 01 2024 at 21:03):

@Scott Morrison has a PR for this #8361, and there has been some additional discussion of this in this thread. I got this working again and got the longest pole for the most recent version of mathlib:

file                                                  | instructions | parallelism
----------------------------------------------------- | ------------ | -----------
Mathlib                                               | 6724535      | x16.34
Mathlib.NumberTheory.Cyclotomic.PID                   | 6717048      | x7.42
Mathlib.NumberTheory.Cyclotomic.Rat                   | 6708512      | x7.39
...
Mathlib.Logic.Basic                                   | 173409       | x4.06
Mathlib.Init.Function                                 | 164218       | x4.05
Mathlib.Tactic.Basic                                  | 161557       | x4.06
Mathlib.Tactic.TypeStar                               | 157514       | x4.14
Std                                                   | 156385       | x4.15
Std.Data.UnionFind                                    | 155614       | x1.27
Std.Data.UnionFind.Lemmas                             | 154967       | x1.27
Std.Data.UnionFind.Basic                              | 145102       | x1.29
Std.Data.Array.Lemmas                                 | 121792       | x1.29
Std.Data.List.Lemmas                                  | 86157        | x1.35
Std.Data.List.Basic                                   | 30986        | x1.00

6.7M instructions seems like a pretty good improvement, since in the previous thread from a few months ago, it was 7.3M. It also looks like Data.List.Basic is gone, which is cool, since there have been a few PRs spinning files off of that file.

Yury G. Kudryashov (Apr 01 2024 at 21:50):

What's behind ...?

Bolton Bailey (Apr 01 2024 at 23:00):

Zulip is telling me I can't make a post that long

Bolton Bailey (Apr 01 2024 at 23:00):

Analyzing Mathlib at 16f050086b364e6b67ec3793ef652238271f5411
file                                                  | instructions | parallelism
----------------------------------------------------- | ------------ | -----------
Mathlib                                               | 6724535      | x16.34
Mathlib.NumberTheory.Cyclotomic.PID                   | 6717048      | x7.42
Mathlib.NumberTheory.Cyclotomic.Rat                   | 6708512      | x7.39
Mathlib.NumberTheory.Cyclotomic.Discriminant          | 6572320      | x7.52
Mathlib.NumberTheory.NumberField.Discriminant         | 6527517      | x7.41
Mathlib.NumberTheory.NumberField.CanonicalEmbedding   | 6227667      | x7.70
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls  | 5830610      | x6.74
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup  | 5764077      | x6.79
Mathlib.Analysis.SpecialFunctions.Gaussian            | 5727699      | x6.83
Mathlib.Analysis.Fourier.PoissonSummation             | 5588962      | x6.65
Mathlib.Analysis.Distribution.SchwartzSpace           | 5551742      | x6.38
Mathlib.Analysis.SpecialFunctions.JapaneseBracket     | 5399452      | x6.46
Mathlib.MeasureTheory.Integral.Layercake              | 5339962      | x6.49
Mathlib.Analysis.SpecialFunctions.Integrals           | 5313393      | x6.52
Mathlib.Analysis.SpecialFunctions.NonIntegrable       | 5199809      | x6.53
Mathlib.MeasureTheory.Integral.FundThmCalculus        | 5185849      | x6.17
Mathlib.MeasureTheory.Integral.DominatedConvergence   | 5104778      | x5.97
Mathlib.MeasureTheory.Integral.IntervalIntegral       | 5077810      | x6.00
Mathlib.MeasureTheory.Integral.SetIntegral            | 5003059      | x5.66
Mathlib.MeasureTheory.Integral.Bochner                | 4902616      | x5.74
Mathlib.MeasureTheory.Integral.SetToL1                | 4674004      | x5.98
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp      | 4412502      | x6.27
Mathlib.MeasureTheory.Function.L1Space                | 4311017      | x6.40
Mathlib.MeasureTheory.Function.LpOrder                | 4223349      | x6.51
Mathlib.MeasureTheory.Function.LpSpace                | 4212933      | x6.52
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp  | 4009883      | x6.73
Mathlib.MeasureTheory.Integral.MeanInequalities       | 3985244      | x6.20
Mathlib.Analysis.MeanInequalities                     | 3948943      | x6.01
Mathlib.Analysis.SpecialFunctions.Pow.NNReal          | 3893988      | x5.83
Mathlib.Analysis.SpecialFunctions.Pow.Real            | 3857867      | x5.87
Mathlib.Analysis.SpecialFunctions.Pow.Complex         | 3817991      | x5.92
Mathlib.Analysis.SpecialFunctions.Complex.Log         | 3799711      | x5.95
Mathlib.Analysis.SpecialFunctions.Complex.Arg         | 3782074      | x5.96
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle | 3739233      | x6.01
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | 3690905      | x5.93
Mathlib.Analysis.SpecialFunctions.Exp                 | 3623406      | x6.02
Mathlib.Analysis.Complex.Basic                        | 3604885      | x5.97
Mathlib.Data.Complex.Module                           | 3536249      | x5.71
Mathlib.FieldTheory.Tower                             | 3442738      | x5.05
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix        | 3432206      | x5.07
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition  | 3410216      | x5.09
Mathlib.LinearAlgebra.Charpoly.Basic                  | 3401236      | x5.10
Mathlib.FieldTheory.Minpoly.Field                     | 3387788      | x5.11
Mathlib.RingTheory.Algebraic                          | 3358245      | x5.14
Mathlib.RingTheory.IntegralClosure                    | 3324918      | x5.18
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap       | 3238551      | x5.24
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff           | 3199658      | x5.29
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic           | 3113608      | x5.34
Mathlib.RingTheory.PolynomialAlgebra                  | 3094619      | x4.99
Mathlib.RingTheory.MatrixAlgebra                      | 3057938      | x4.95
Mathlib.RingTheory.TensorProduct.Basic                | 3025048      | x4.99
Mathlib.LinearAlgebra.FiniteDimensional               | 2793401      | x5.25
Mathlib.LinearAlgebra.Dimension.DivisionRing          | 2695110      | x5.40
Mathlib.LinearAlgebra.Dimension.Constructions         | 2638543      | x5.44
Mathlib.Algebra.Module.Torsion                        | 2560830      | x5.53
Mathlib.GroupTheory.Torsion                           | 2482285      | x5.64
Mathlib.GroupTheory.PGroup                            | 2465115      | x5.67
Mathlib.GroupTheory.SpecificGroups.Cyclic             | 2439380      | x5.63
Mathlib.GroupTheory.Exponent                          | 2402998      | x5.26
Mathlib.Data.Nat.Factorization.Basic                  | 2377262      | x5.10
Mathlib.NumberTheory.Padics.PadicVal                  | 2318516      | x5.20
Mathlib.RingTheory.Int.Basic                          | 2299289      | x5.18
Mathlib.RingTheory.PrincipalIdealDomain               | 2283730      | x5.18
Mathlib.RingTheory.UniqueFactorizationDomain          | 2261252      | x5.22
Mathlib.RingTheory.Noetherian                         | 2162416      | x5.40
Mathlib.RingTheory.Nilpotent                          | 2026743      | x5.53
Mathlib.LinearAlgebra.Matrix.ToLin                    | 2009704      | x5.55
Mathlib.Algebra.Algebra.Subalgebra.Tower              | 1869400      | x5.70
Mathlib.Algebra.Algebra.Subalgebra.Basic              | 1859830      | x5.71
Mathlib.RingTheory.Ideal.Operations                   | 1789788      | x5.89
Mathlib.Algebra.Algebra.Operations                    | 1658742      | x5.67
Mathlib.Algebra.Algebra.Bilinear                      | 1565294      | x4.99
Mathlib.LinearAlgebra.TensorProduct.Basic             | 1545527      | x4.51
Mathlib.Algebra.Module.Submodule.Bilinear             | 1337524      | x5.03
Mathlib.LinearAlgebra.Span                            | 1321405      | x5.01
Mathlib.LinearAlgebra.Basic                           | 1259256      | x4.87
Mathlib.Algebra.Module.Submodule.Ker                  | 1189156      | x5.09
Mathlib.Algebra.Module.Submodule.Map                  | 1164777      | x5.17
Mathlib.Algebra.Module.Submodule.Lattice              | 1126149      | x5.30
Mathlib.Algebra.Module.Submodule.Basic                | 1093883      | x5.11

Bolton Bailey (Apr 01 2024 at 23:00):

Mathlib.GroupTheory.Submonoid.Membership              | 1067502      | x4.28
Mathlib.Data.Finset.NoncommProd                       | 1038551      | x4.25
Mathlib.Algebra.BigOperators.Basic                    | 1018066      | x4.31
Mathlib.Data.Finset.Preimage                          | 907117       | x4.47
Mathlib.Data.Set.Finite                               | 900846       | x4.50
Mathlib.Data.Finite.Basic                             | 858174       | x4.66
Mathlib.Data.Fintype.Sigma                            | 854982       | x4.42
Mathlib.Data.Finset.Sigma                             | 834043       | x4.46
Mathlib.Data.Finset.Lattice                           | 825364       | x4.48
Mathlib.Data.Finset.Prod                              | 756249       | x4.63
Mathlib.Data.Finset.Card                              | 733394       | x4.75
Mathlib.Data.Finset.Image                             | 715327       | x4.84
Mathlib.Data.Finset.Basic                             | 692607       | x4.86
Mathlib.Data.Multiset.FinsetOps                       | 622502       | x4.88
Mathlib.Data.Multiset.Dedup                           | 614858       | x4.93
Mathlib.Data.Multiset.Nodup                           | 610623       | x4.95
Mathlib.Data.Multiset.Bind                            | 600021       | x4.96
Mathlib.Algebra.BigOperators.Multiset.Basic           | 583196       | x5.04
Mathlib.Data.Multiset.Basic                           | 569694       | x5.14
Mathlib.Data.List.Perm                                | 498692       | x5.61
Mathlib.Data.List.Dedup                               | 480633       | x5.51
Mathlib.Data.List.Nodup                               | 477272       | x4.71
Mathlib.Data.Set.Pairwise.Basic                       | 465889       | x4.41
Mathlib.Data.Set.Function                             | 456630       | x3.99
Mathlib.Data.Set.Prod                                 | 430524       | x4.17
Mathlib.Data.Set.Image                                | 405136       | x4.37
Mathlib.Data.Set.Basic                                | 384570       | x4.46
Mathlib.Order.SymmDiff                                | 335960       | x4.56
Mathlib.Order.BooleanAlgebra                          | 319024       | x4.59
Mathlib.Order.Heyting.Basic                           | 294815       | x4.89
Mathlib.Order.PropInstances                           | 265583       | x5.32
Mathlib.Order.Disjoint                                | 263152       | x5.36
Mathlib.Order.BoundedOrder                            | 252537       | x4.41
Mathlib.Order.Lattice                                 | 244722       | x4.46
Mathlib.Order.Monotone.Basic                          | 228304       | x4.62
Mathlib.Order.RelClasses                              | 217151       | x4.31
Mathlib.Order.Basic                                   | 209198       | x4.24
Mathlib.Tactic.Convert                                | 191938       | x3.81
Mathlib.Tactic.Congr!                                 | 188556       | x3.86
Mathlib.Logic.Basic                                   | 173409       | x4.06
Mathlib.Init.Function                                 | 164218       | x4.05
Mathlib.Tactic.Basic                                  | 161557       | x4.06
Mathlib.Tactic.TypeStar                               | 157514       | x4.14
Std                                                   | 156385       | x4.15
Std.Data.UnionFind                                    | 155614       | x1.27
Std.Data.UnionFind.Lemmas                             | 154967       | x1.27
Std.Data.UnionFind.Basic                              | 145102       | x1.29
Std.Data.Array.Lemmas                                 | 121792       | x1.29
Std.Data.List.Lemmas                                  | 86157        | x1.35
Std.Data.List.Basic                                   | 30986        | x1.00

Mario Carneiro (Apr 01 2024 at 23:55):

Maybe we should ban import Std in mathlib after all, for similar reasons as lean banning import Init. We can just import CodeAction and the tactics (that haven't already been upstreamed); everything else (data structures and theorems) should just be imported normally like everything else in mathlib

Mario Carneiro (Apr 01 2024 at 23:59):

(this calculus might change if we start shipping Std precompiled, but right now it's eating up precious build parallelism)

Mario Carneiro (Apr 02 2024 at 00:01):

Has anyone had a go at making Finset.Defs? There are so many things in mathlib that want to talk about finiteness that are limited by the stack leading to Finset, even though you could define Multiset and Finset in less than 30 lines

Mario Carneiro (Apr 02 2024 at 00:02):

(regarding the remark that Data.List.Basic is off the long pole: are you sure it hasn't just had its content moved to Std.Data.List.Basic, which is on the long pole?)

Bolton Bailey (Apr 02 2024 at 00:26):

Mario Carneiro said:

(regarding the remark that Data.List.Basic is off the long pole: are you sure it hasn't just had its content moved to Std.Data.List.Basic, which is on the long pole?)

Not sure - I was thinking of #11662, #11542, and #10337 which I think moved things to other files in Mathlib

Johan Commelin (Apr 02 2024 at 01:27):

Mario, fyi, @Yaël Dillies is working hard to golf the path to Finset

Yaël Dillies (Apr 02 2024 at 07:34):

Mario Carneiro said:

Has anyone had a go at making Finset.Defs?

Yes, as Johan says, I'm working on this. All relevant PRs are linked in #11757 and reviews are welcome :pray:

Yaël Dillies (Apr 02 2024 at 07:35):

Well, I'm not quite working towards having the definition of Finset in 30 lines, but rather having all the basic API without any mentions to algebra and order theory

Anne Baanen (Apr 02 2024 at 12:48):

Observation at first glance: does Mathlib.FieldTheory.Tower really warrant all these transitive imports?

Anne Baanen (Apr 02 2024 at 12:49):

(Not sure if the issue is in Tower itself needing to be split, or that its transitive dependencies are too strong.)

Anne Baanen (Apr 02 2024 at 12:52):

Also the bit around Mathlib.Data.Nat.Factorization.Basic importing Mathlib.NumberTheory.Padics.PadicVal seems like it can be optimized.

Eric Rodriguez (Apr 02 2024 at 12:55):

That's just related to the several ways to write factorizations mess

Johan Commelin (Apr 03 2024 at 04:20):

I think Padics.PadicsVal can be quite basic, even though the name sounds heavy

Eric Wieser (Apr 03 2024 at 22:57):

Mario Carneiro said:

Maybe we should ban import Std in mathlib after all, for similar reasons as lean banning import Init. We can just import CodeAction and the tactics (that haven't already been upstreamed); everything else (data structures and theorems) should just be imported normally like everything else in mathlib

After #11876, there is only one import Std in Mathlib; though it is in Tactic.Basic where it is probably intended to prevent any downstream code from having to think about Std.

Mario Carneiro (Apr 04 2024 at 02:41):

It's not about how many times import Std is used; obviously once is enough. The clear intent behind putting import Std in an early file is to have all of std available in all of mathlib, but my point is that this is an unnecessary build bottleneck, and it will get worse as Std grows. Seeing Std.Data.UnionFind in the dependencies of Mathlib.Init.Function was what gave me this impression: there are lots of Std things which are useful for specific use cases but aren't necessarily worth the "convenience" of having available with no (additional) imports.

There are four main reasons mathlib wants to have Std imported, all related to metaprogramming:

  • code actions (e.g. "fill out this inductive pattern match")
  • tactics/commands like #where and alias
  • syntax linters like the unused tactic linter
  • environment linters like simpNF

So why not just import these things in the relevant early mathlib file, instead of importing everything? I think it is perfectly reasonable for downstream mathlib code to be importing files like Std.Data.HashMap.Lemmas only when needed, and I'm sure if we do this there will be some std files that are not used in mathlib at all (like UnionFind). We may want to put import Std in Mathlib.lean so that the full Std cache is available in CI, but there is no need for it to be asked for any earlier than that.

Mario Carneiro (Apr 04 2024 at 02:59):

Note: re: import Std in Mathlib.Tactic.TypeStar, this is definitely deliberate, a case of a file which is imported by literally everything in mathlib and which itself has no mathlib imports which would make it unsuitable as a "first file". This is what makes Mathlib.Tactic.Basic a bad "first file" - it has too many mathlib imports - which means that if you are in a dependency of Mathlib.Tactic.Basic then you don't get Std. We should really just have a "first file" or "first folder", but the obvious name for this is Mathlib.Init and it's taken right now. How about we rename Mathlib.Init to Mathlib.Lean3Cruft and make Mathlib.Init actually useful per its name?

Yaël Dillies (Apr 04 2024 at 05:48):

Let me advertise #10709 as a PR that would reduce said cruft

Yaël Dillies (Apr 04 2024 at 05:55):

I'm willing to try reducing the Mathlib.Init folder, but I need support on the merging side

Yaël Dillies (Apr 04 2024 at 06:48):

#11882 for another one

Eric Wieser (Apr 04 2024 at 07:09):

Mario Carneiro said:

We may want to put import Std in Mathlib.lean so that the full Std cache is available in CI, but there is no need for it to be asked for any earlier than that.

This sounds good to me, but our current CI scripts will reject the attempt to add this import

Yaël Dillies (Apr 04 2024 at 07:10):

Also note that if we want to carve out Algebra, Data and Order sublibraries (as per #11757) then we will need some sublibrary living just above Std, which we might call MathlibInit, containing a few basic things, like the content of Data.Nat.Defs and Data.Int.Defs and also a few tactics. It could act as a buffer zone for things that could go to Std

Yaël Dillies (Apr 04 2024 at 07:10):

Eric Wieser said:

our current CI scripts will reject the attempt to add this import

We could just add a file Mathlib.Std containing import Std and all would be well again

Number Eighteen (Apr 04 2024 at 13:58):

Johan Commelin said:

I think Padics.PadicsVal can be quite basic, even though the name sounds heavy

I remember a very old Number Theory textbook starting the Prelude with "...let pp be prime and nn an integer such that vp(n)>0v_p(n) > 0"... :melting_face:

Bolton Bailey (Apr 04 2024 at 21:16):

I reformatted the table a bit so that you can see which files contribute the most instructions to the total.
Here's a recent origin/master:

Analyzing Mathlib at 89a00da8c4971f8ed447d45fcae246634308dc73
file                                                  | instructions | (cumulative) | parallelism
----------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                               |         7493 |      6434115 | x17.26
Mathlib.NumberTheory.Cyclotomic.PID                   |         8543 |      6426621 | x7.30
Mathlib.NumberTheory.Cyclotomic.Rat                   |       136308 |      6418078 | x7.27
Mathlib.NumberTheory.Cyclotomic.Discriminant          |        44893 |      6281770 | x7.40
Mathlib.NumberTheory.NumberField.Discriminant         |       291794 |      6236876 | x7.28
Mathlib.NumberTheory.NumberField.CanonicalEmbedding   |       397262 |      5945081 | x7.53
Mathlib.NumberTheory.NumberField.Embeddings           |       122132 |      5547819 | x7.17
Mathlib.Analysis.Complex.Polynomial                   |        25565 |      5425686 | x7.03
Mathlib.Analysis.Complex.Liouville                    |        16110 |      5400121 | x6.75
Mathlib.Analysis.Complex.CauchyIntegral               |        47260 |      5384010 | x6.77
Mathlib.MeasureTheory.Integral.CircleIntegral         |        69606 |      5336750 | x6.62
Mathlib.Analysis.SpecialFunctions.NonIntegrable       |        13991 |      5267143 | x6.63
Mathlib.MeasureTheory.Integral.FundThmCalculus        |        81098 |      5253152 | x6.27
Mathlib.MeasureTheory.Integral.DominatedConvergence   |        27147 |      5172053 | x6.10
Mathlib.MeasureTheory.Integral.IntervalIntegral       |        74808 |      5144906 | x6.13
Mathlib.MeasureTheory.Integral.SetIntegral            |       113097 |      5070097 | x5.86
Mathlib.MeasureTheory.Integral.Bochner                |       228661 |      4957000 | x5.76
Mathlib.MeasureTheory.Integral.SetToL1                |       262713 |      4728338 | x5.99
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp      |       102206 |      4465625 | x6.28
Mathlib.MeasureTheory.Function.L1Space                |        90571 |      4363418 | x6.41
Mathlib.MeasureTheory.Function.LpOrder                |        10424 |      4272847 | x6.52
Mathlib.MeasureTheory.Function.LpSpace                |       203155 |      4262422 | x6.53
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp  |        24632 |      4059266 | x6.74
Mathlib.MeasureTheory.Integral.MeanInequalities       |        36290 |      4034633 | x6.21
Mathlib.Analysis.MeanInequalities                     |        54955 |      3998343 | x6.02
Mathlib.Analysis.SpecialFunctions.Pow.NNReal          |        36148 |      3943388 | x5.84
Mathlib.Analysis.SpecialFunctions.Pow.Real            |        39883 |      3907239 | x5.88
Mathlib.Analysis.SpecialFunctions.Pow.Complex         |        18323 |      3867355 | x5.93
Mathlib.Analysis.SpecialFunctions.Complex.Log         |        17650 |      3849032 | x5.95
Mathlib.Analysis.SpecialFunctions.Complex.Arg         |        42854 |      3831381 | x5.97
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle |        48331 |      3788526 | x6.02
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |        69457 |      3740194 | x5.93
Mathlib.Analysis.SpecialFunctions.Exp                 |        18556 |      3670737 | x6.03
Mathlib.Analysis.Complex.Basic                        |        68601 |      3652181 | x5.98
Mathlib.Data.Complex.Module                           |        93488 |      3583580 | x5.69
Mathlib.FieldTheory.Tower                             |        10542 |      3490091 | x5.04
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix        |        21999 |      3479548 | x5.05
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition  |         8985 |      3457549 | x5.07
Mathlib.LinearAlgebra.Charpoly.Basic                  |        13453 |      3448563 | x5.08
Mathlib.FieldTheory.Minpoly.Field                     |        29799 |      3435109 | x5.10
Mathlib.RingTheory.Algebraic                          |        33322 |      3405309 | x5.13
Mathlib.RingTheory.IntegralClosure                    |        86363 |      3371987 | x5.16
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap       |        38920 |      3285624 | x5.22
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff           |        86035 |      3246703 | x5.27
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic           |        18998 |      3160668 | x5.32
Mathlib.RingTheory.PolynomialAlgebra                  |        36691 |      3141669 | x4.97
Mathlib.RingTheory.MatrixAlgebra                      |        32898 |      3104978 | x4.93
Mathlib.RingTheory.TensorProduct.Basic                |       231778 |      3072079 | x4.97
Mathlib.LinearAlgebra.FiniteDimensional               |        98361 |      2840301 | x5.23
Mathlib.LinearAlgebra.Dimension.DivisionRing          |        58382 |      2741940 | x5.38
Mathlib.LinearAlgebra.Dimension.Constructions         |        77698 |      2683558 | x5.42
Mathlib.Algebra.Module.Torsion                        |        78447 |      2605860 | x5.50
Mathlib.GroupTheory.Torsion                           |        17171 |      2527412 | x5.61
Mathlib.GroupTheory.PGroup                            |        25746 |      2510240 | x5.64
Mathlib.GroupTheory.SpecificGroups.Cyclic             |        36378 |      2484494 | x5.59
Mathlib.GroupTheory.Exponent                          |        25738 |      2448115 | x5.21
Mathlib.Data.Nat.Factorization.Basic                  |        58753 |      2422377 | x5.05
Mathlib.NumberTheory.Padics.PadicVal                  |        19259 |      2363623 | x5.15
Mathlib.RingTheory.Int.Basic                          |        15560 |      2344364 | x5.13
Mathlib.RingTheory.PrincipalIdealDomain               |        22481 |      2328803 | x5.13
Mathlib.RingTheory.UniqueFactorizationDomain          |        98834 |      2306321 | x5.17
Mathlib.RingTheory.Noetherian                         |       137178 |      2207487 | x5.34
Mathlib.RingTheory.Nilpotent                          |        17036 |      2070309 | x5.47
Mathlib.LinearAlgebra.Matrix.ToLin                    |       140511 |      2053272 | x5.48
Mathlib.Algebra.Algebra.Subalgebra.Tower              |         9575 |      1912761 | x5.63
Mathlib.Algebra.Algebra.Subalgebra.Basic              |        70044 |      1903185 | x5.64
Mathlib.RingTheory.Ideal.Operations                   |       131145 |      1833140 | x5.81
Mathlib.Algebra.Algebra.Operations                    |        93853 |      1701994 | x5.59
Mathlib.Algebra.Algebra.Bilinear                      |        19768 |      1608141 | x4.92
Mathlib.LinearAlgebra.TensorProduct.Basic             |       208022 |      1588372 | x4.45
Mathlib.Algebra.Module.Submodule.Bilinear             |        16125 |      1380349 | x4.95

Bolton Bailey (Apr 04 2024 at 21:16):

Mathlib.LinearAlgebra.Span                            |        62150 |      1364224 | x4.93
Mathlib.LinearAlgebra.Basic                           |        70265 |      1302073 | x4.79
Mathlib.Algebra.Module.Submodule.Ker                  |        24506 |      1231808 | x4.99
Mathlib.Algebra.Module.Submodule.Map                  |        38645 |      1207301 | x5.08
Mathlib.Algebra.Module.Submodule.Lattice              |        32269 |      1168656 | x5.20
Mathlib.Algebra.Module.Submodule.Basic                |        26383 |      1136387 | x5.00
Mathlib.GroupTheory.Submonoid.Membership              |        28939 |      1110004 | x4.20
Mathlib.Data.Finset.NoncommProd                       |        20489 |      1081064 | x4.14
Mathlib.Algebra.BigOperators.Basic                    |       110922 |      1060574 | x4.20
Mathlib.Data.Finset.Preimage                          |         6269 |       949652 | x4.29
Mathlib.Data.Set.Finite                               |        42663 |       943382 | x4.31
Mathlib.Data.Finite.Basic                             |         3190 |       900719 | x4.46
Mathlib.Data.Fintype.Sigma                            |        20937 |       897529 | x4.23
Mathlib.Data.Finset.Sigma                             |         8679 |       876592 | x4.26
Mathlib.Data.Finset.Lattice                           |        69115 |       867912 | x4.28
Mathlib.Data.Finset.Prod                              |        22856 |       798796 | x4.22
Mathlib.Data.Finset.Card                              |        18064 |       775940 | x4.31
Mathlib.Data.Finset.Image                             |        22720 |       757875 | x4.39
Mathlib.Data.Finset.Union                             |         9040 |       735155 | x4.37
Mathlib.Data.Finset.Basic                             |        70102 |       726114 | x4.32
Mathlib.Data.Multiset.FinsetOps                       |         7681 |       656012 | x4.58
Mathlib.Data.Multiset.Dedup                           |         4234 |       648330 | x4.62
Mathlib.Data.Multiset.Nodup                           |        10579 |       644096 | x4.65
Mathlib.Data.Multiset.Range                           |         2692 |       633516 | x4.71
Mathlib.Data.Multiset.Basic                           |        70996 |       630823 | x4.72
Mathlib.Data.List.Perm                                |        18045 |       559826 | x5.19
Mathlib.Data.List.Permutation                         |         8155 |       541781 | x5.29
Mathlib.Data.List.Join                                |         5506 |       533626 | x5.36
Mathlib.Algebra.BigOperators.List.Basic               |        36210 |       528120 | x5.40
Mathlib.Data.List.Rotate                              |        11071 |       491909 | x4.48
Mathlib.Data.List.Nodup                               |        11471 |       480838 | x4.53
Mathlib.Data.Set.Pairwise.Basic                       |         9255 |       469367 | x4.39
Mathlib.Data.Set.Function                             |        26221 |       460111 | x3.97
Mathlib.Data.Set.Prod                                 |        25380 |       433890 | x4.15
Mathlib.Data.Set.Image                                |        20562 |       408510 | x4.34
Mathlib.Data.Set.Basic                                |        48609 |       387948 | x4.44
Mathlib.Order.SymmDiff                                |        16936 |       339339 | x4.53
Mathlib.Order.BooleanAlgebra                          |        24206 |       322402 | x4.56
Mathlib.Order.Heyting.Basic                           |        29233 |       298196 | x4.85
Mathlib.Order.PropInstances                           |         2429 |       268963 | x5.27
Mathlib.Order.Disjoint                                |        10608 |       266533 | x5.31
Mathlib.Order.BoundedOrder                            |         7813 |       255925 | x4.37
Mathlib.Order.Lattice                                 |        16408 |       248111 | x4.42
Mathlib.Order.Monotone.Basic                          |        11155 |       231703 | x4.58
Mathlib.Order.RelClasses                              |         7947 |       220547 | x4.27
Mathlib.Order.Basic                                   |        17256 |       212600 | x4.19
Mathlib.Tactic.Convert                                |         3380 |       195344 | x3.77
Mathlib.Tactic.Congr!                                 |        15146 |       191963 | x3.82
Mathlib.Logic.Basic                                   |         9192 |       176817 | x4.01
Mathlib.Init.Function                                 |         2658 |       167624 | x3.99
Mathlib.Tactic.Basic                                  |         4041 |       164965 | x4.01
Mathlib.Tactic.TypeStar                               |         1127 |       160924 | x4.08
Std                                                   |          770 |       159797 | x4.09
Std.Data.UnionFind                                    |          645 |       159027 | x1.26
Std.Data.UnionFind.Lemmas                             |         9872 |       158381 | x1.26
Std.Data.UnionFind.Basic                              |        23305 |       148509 | x1.28
Std.Data.Array.Lemmas                                 |        38010 |       125204 | x1.27
Std.Data.List.Lemmas                                  |        55034 |        87193 | x1.34
Std.Data.List.Basic                                   |        32159 |        32159 | x1.00

Bolton Bailey (Apr 04 2024 at 21:17):

And here it is after spitting the longest file in #11873

Analyzing Mathlib at 860785ff08f395da41a31713466a42ad324f075c
file                                                  | instructions | (cumulative) | parallelism
----------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                               |         7473 |      6230844 | x17.78
Mathlib.NumberTheory.Cyclotomic.PID                   |         8518 |      6223371 | x7.50
Mathlib.NumberTheory.Cyclotomic.Rat                   |       136278 |      6214853 | x7.47
Mathlib.NumberTheory.Cyclotomic.Discriminant          |        44868 |      6078574 | x7.61
Mathlib.NumberTheory.NumberField.Discriminant         |       291784 |      6033706 | x7.49
Mathlib.NumberTheory.NumberField.CanonicalEmbedding   |       195755 |      5741922 | x7.76
Mathlib.NumberTheory.NumberField.Embeddings           |       122107 |      5546166 | x7.16
Mathlib.Analysis.Complex.Polynomial                   |        25542 |      5424058 | x7.03
Mathlib.Analysis.Complex.Liouville                    |        16084 |      5398516 | x6.75
Mathlib.Analysis.Complex.CauchyIntegral               |        47232 |      5382431 | x6.76
Mathlib.MeasureTheory.Integral.CircleIntegral         |        69583 |      5335198 | x6.62
Mathlib.Analysis.SpecialFunctions.NonIntegrable       |        13966 |      5265615 | x6.63
Mathlib.MeasureTheory.Integral.FundThmCalculus        |        81064 |      5251648 | x6.27
Mathlib.MeasureTheory.Integral.DominatedConvergence   |        27123 |      5170584 | x6.10
Mathlib.MeasureTheory.Integral.IntervalIntegral       |        74783 |      5143460 | x6.12
Mathlib.MeasureTheory.Integral.SetIntegral            |       113081 |      5068676 | x5.86
Mathlib.MeasureTheory.Integral.Bochner                |       228637 |      4955595 | x5.75
Mathlib.MeasureTheory.Integral.SetToL1                |       262697 |      4726957 | x5.98
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp      |       102179 |      4464259 | x6.28
Mathlib.MeasureTheory.Function.L1Space                |        90551 |      4362080 | x6.40
Mathlib.MeasureTheory.Function.LpOrder                |        10403 |      4271528 | x6.52
Mathlib.MeasureTheory.Function.LpSpace                |       203127 |      4261125 | x6.53
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp  |        24611 |      4057997 | x6.74
Mathlib.MeasureTheory.Integral.MeanInequalities       |        36267 |      4033386 | x6.21
Mathlib.Analysis.MeanInequalities                     |        54934 |      3997118 | x6.01
Mathlib.Analysis.SpecialFunctions.Pow.NNReal          |        36133 |      3942184 | x5.83
Mathlib.Analysis.SpecialFunctions.Pow.Real            |        39868 |      3906051 | x5.87
Mathlib.Analysis.SpecialFunctions.Pow.Complex         |        18303 |      3866183 | x5.93
Mathlib.Analysis.SpecialFunctions.Complex.Log         |        17631 |      3847879 | x5.95
Mathlib.Analysis.SpecialFunctions.Complex.Arg         |        42841 |      3830248 | x5.96
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle |        48324 |      3787407 | x6.01
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |        69434 |      3739082 | x5.93
Mathlib.Analysis.SpecialFunctions.Exp                 |        18533 |      3669648 | x6.02
Mathlib.Analysis.Complex.Basic                        |        68572 |      3651114 | x5.97
Mathlib.Data.Complex.Module                           |        93459 |      3582542 | x5.69
Mathlib.FieldTheory.Tower                             |        10523 |      3489082 | x5.03
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix        |        21977 |      3478558 | x5.04
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition  |         8967 |      3456581 | x5.06
Mathlib.LinearAlgebra.Charpoly.Basic                  |        13435 |      3447614 | x5.07
Mathlib.FieldTheory.Minpoly.Field                     |        29779 |      3434179 | x5.09
Mathlib.RingTheory.Algebraic                          |        33303 |      3404400 | x5.12
Mathlib.RingTheory.IntegralClosure                    |        86341 |      3371097 | x5.16
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap       |        38896 |      3284755 | x5.21
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff           |        86015 |      3245859 | x5.26
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic           |        18977 |      3159844 | x5.31
Mathlib.RingTheory.PolynomialAlgebra                  |        36669 |      3140867 | x4.96
Mathlib.RingTheory.MatrixAlgebra                      |        32874 |      3104197 | x4.93
Mathlib.RingTheory.TensorProduct.Basic                |       231765 |      3071323 | x4.97
Mathlib.LinearAlgebra.FiniteDimensional               |        98334 |      2839557 | x5.22
Mathlib.LinearAlgebra.Dimension.DivisionRing          |        58359 |      2741223 | x5.37
Mathlib.LinearAlgebra.Dimension.Constructions         |        77677 |      2682863 | x5.41
Mathlib.Algebra.Module.Torsion                        |        78428 |      2605186 | x5.49
Mathlib.GroupTheory.Torsion                           |        17150 |      2526757 | x5.60
Mathlib.GroupTheory.PGroup                            |        25726 |      2509607 | x5.63
Mathlib.GroupTheory.SpecificGroups.Cyclic             |        36350 |      2483880 | x5.58
Mathlib.GroupTheory.Exponent                          |        25714 |      2447530 | x5.20
Mathlib.Data.Nat.Factorization.Basic                  |        58724 |      2421815 | x5.05
Mathlib.NumberTheory.Padics.PadicVal                  |        19232 |      2363090 | x5.14
Mathlib.RingTheory.Int.Basic                          |        15539 |      2343858 | x5.12
Mathlib.RingTheory.PrincipalIdealDomain               |        22461 |      2328319 | x5.12
Mathlib.RingTheory.UniqueFactorizationDomain          |        98812 |      2305857 | x5.16
Mathlib.RingTheory.Noetherian                         |       137540 |      2207045 | x5.33
Mathlib.RingTheory.Nilpotent                          |        17016 |      2069504 | x5.46
Mathlib.LinearAlgebra.Matrix.ToLin                    |       140479 |      2052488 | x5.47
Mathlib.Algebra.Algebra.Subalgebra.Tower              |         9555 |      1912008 | x5.62
Mathlib.Algebra.Algebra.Subalgebra.Basic              |        70030 |      1902452 | x5.63
Mathlib.RingTheory.Ideal.Operations                   |       131120 |      1832422 | x5.80
Mathlib.Algebra.Algebra.Operations                    |        93833 |      1701301 | x5.58
Mathlib.Algebra.Algebra.Bilinear                      |        19748 |      1607468 | x4.91
Mathlib.LinearAlgebra.TensorProduct.Basic             |       208012 |      1587720 | x4.44
Mathlib.Algebra.Module.Submodule.Bilinear             |        16093 |      1379707 | x4.94

Bolton Bailey (Apr 04 2024 at 21:17):

Mathlib.LinearAlgebra.Span                            |        62130 |      1363613 | x4.92
Mathlib.LinearAlgebra.Basic                           |        70239 |      1301483 | x4.78
Mathlib.Algebra.Module.Submodule.Ker                  |        24462 |      1231244 | x4.98
Mathlib.Algebra.Module.Submodule.Map                  |        38623 |      1206782 | x5.06
Mathlib.Algebra.Module.Submodule.Lattice              |        32251 |      1168158 | x5.18
Mathlib.Algebra.Module.Submodule.Basic                |        26364 |      1135907 | x4.99
Mathlib.GroupTheory.Submonoid.Membership              |        28924 |      1109543 | x4.19
Mathlib.Data.Finset.NoncommProd                       |        20468 |      1080618 | x4.13
Mathlib.Algebra.BigOperators.Basic                    |       110892 |      1060150 | x4.19
Mathlib.Data.Finset.Preimage                          |         6251 |       949257 | x4.28
Mathlib.Data.Set.Finite                               |        42633 |       943005 | x4.30
Mathlib.Data.Finite.Basic                             |         3172 |       900371 | x4.45
Mathlib.Data.Fintype.Sigma                            |        20913 |       897199 | x4.21
Mathlib.Data.Finset.Sigma                             |         8660 |       876285 | x4.25
Mathlib.Data.Finset.Lattice                           |        69092 |       867625 | x4.26
Mathlib.Data.Finset.Prod                              |        22835 |       798533 | x4.20
Mathlib.Data.Finset.Card                              |        18033 |       775698 | x4.29
Mathlib.Data.Finset.Image                             |        22698 |       757664 | x4.37
Mathlib.Data.Finset.Union                             |         9023 |       734966 | x4.35
Mathlib.Data.Finset.Basic                             |        70058 |       725942 | x4.30
Mathlib.Data.Multiset.FinsetOps                       |         7661 |       655884 | x4.56
Mathlib.Data.Multiset.Dedup                           |         4215 |       648222 | x4.60
Mathlib.Data.Multiset.Nodup                           |        10559 |       644006 | x4.63
Mathlib.Data.Multiset.Range                           |         2674 |       633447 | x4.69
Mathlib.Data.Multiset.Basic                           |        70972 |       630773 | x4.70
Mathlib.Data.List.Perm                                |        18030 |       559800 | x5.16
Mathlib.Data.List.Permutation                         |         8174 |       541770 | x5.27
Mathlib.Data.List.Join                                |         5488 |       533595 | x5.33
Mathlib.Algebra.BigOperators.List.Basic               |        36192 |       528106 | x5.38
Mathlib.Data.List.Rotate                              |        11077 |       491913 | x4.45
Mathlib.Data.List.Nodup                               |        11451 |       480836 | x4.51
Mathlib.Data.Set.Pairwise.Basic                       |         9235 |       469384 | x4.35
Mathlib.Data.Set.Function                             |        26218 |       460149 | x3.98
Mathlib.Data.Set.Prod                                 |        25378 |       433930 | x4.16
Mathlib.Data.Set.Image                                |        20558 |       408551 | x4.36
Mathlib.Data.Set.Basic                                |        48565 |       387993 | x4.45
Mathlib.Order.SymmDiff                                |        16934 |       339428 | x4.54
Mathlib.Order.BooleanAlgebra                          |        24198 |       322493 | x4.58
Mathlib.Order.Heyting.Basic                           |        29232 |       298295 | x4.87
Mathlib.Order.PropInstances                           |         2428 |       269063 | x5.29
Mathlib.Order.Disjoint                                |        10607 |       266634 | x5.33
Mathlib.Order.BoundedOrder                            |         7813 |       256027 | x4.37
Mathlib.Order.Lattice                                 |        16406 |       248214 | x4.42
Mathlib.Order.Monotone.Basic                          |        11153 |       231807 | x4.57
Mathlib.Order.RelClasses                              |         7947 |       220653 | x4.26
Mathlib.Order.Basic                                   |        17255 |       212706 | x4.19
Mathlib.Tactic.Convert                                |         3380 |       195450 | x3.77
Mathlib.Tactic.Congr!                                 |        15146 |       192069 | x3.81
Mathlib.Logic.Basic                                   |         9289 |       176923 | x4.01
Mathlib.Init.Function                                 |         2659 |       167634 | x3.99
Mathlib.Tactic.Basic                                  |         4041 |       164975 | x4.01
Mathlib.Tactic.TypeStar                               |         1127 |       160933 | x4.08
Std                                                   |          770 |       159806 | x4.09
Std.Data.UnionFind                                    |          645 |       159036 | x1.26
Std.Data.UnionFind.Lemmas                             |         9874 |       158391 | x1.26
Std.Data.UnionFind.Basic                              |        23305 |       148517 | x1.28
Std.Data.Array.Lemmas                                 |        38013 |       125211 | x1.27
Std.Data.List.Lemmas                                  |        55039 |        87198 | x1.34
Std.Data.List.Basic                                   |        32158 |        32158 | x1.00

Bolton Bailey (Apr 04 2024 at 21:29):

Hmm, I'm a bit confused by this, Mathlib.NumberTheory.NumberField.Discriminant doesn't import Mathlib.NumberTheory.NumberField. CanonicalEmbedding directly in 860785ff08f395da41a31713466a42ad324f075c, Update: I think I see - the code gets the import graph from the current branch.

Jon Eugster (Apr 05 2024 at 06:22):

Bolton Bailey said:

Scott Morrison has a PR for this #8361, and there has been some additional discussion of this in this thread. I got this working again and [...]

I commented on the PR, if the code only depends on Std it could make sense to move it to the repo where lake exe graph, #find_home, etc. live.

Ruben Van de Velde (Apr 05 2024 at 09:35):

Anne Baanen said:

Also the bit around Mathlib.Data.Nat.Factorization.Basic importing Mathlib.NumberTheory.Padics.PadicVal seems like it can be optimized.

#11919 lightens Mathlib.NumberTheory.Padics.PadicVal a bit

Ruben Van de Velde (Apr 05 2024 at 11:57):

I experimented a bit more at https://github.com/leanprover-community/mathlib4/compare/wip-padic-reduce-imports . Dropping the dependency on big operators might be worthwhile, but a bit more work than I'm planning to take on right now (mostly splitting out things about factorials). Feel free to pick up anything if you think it's useful.

I've made #11923 for the Nat.ModEq change because it looks simple, but on its own it doesn't help much with PadicVal

Bolton Bailey (Apr 07 2024 at 22:02):

Ok here is the hopefully less buggy pole now that that PR is merged

Analyzing Mathlib at 9aded8e01ba2ac52c5e6864d9847cf26c6aaa015
file                                                           | instructions | (cumulative) | parallelism
-------------------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                                        |         7498 |      6529833 | x17.04
Mathlib.NumberTheory.Cyclotomic.PID                            |         8587 |      6522334 | x7.76
Mathlib.NumberTheory.Cyclotomic.Rat                            |       137087 |      6513747 | x7.74
Mathlib.NumberTheory.Cyclotomic.Discriminant                   |        46695 |      6376660 | x7.87
Mathlib.NumberTheory.NumberField.Discriminant                  |       289819 |      6329964 | x7.76
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody |       200295 |      6040144 | x8.07
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls           |        67084 |      5839849 | x6.93
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup           |        35701 |      5772764 | x6.99
Mathlib.Analysis.SpecialFunctions.Gaussian                     |       140785 |      5737063 | x7.03
Mathlib.Analysis.Fourier.PoissonSummation                      |        38129 |      5596277 | x6.84
Mathlib.Analysis.Distribution.SchwartzSpace                    |       171595 |      5558148 | x6.56
Mathlib.Analysis.SpecialFunctions.JapaneseBracket              |        72311 |      5386552 | x6.67
Mathlib.MeasureTheory.Integral.Layercake                       |        32061 |      5314241 | x6.72
Mathlib.Analysis.SpecialFunctions.Integrals                    |       115445 |      5282179 | x6.75
Mathlib.Analysis.SpecialFunctions.NonIntegrable                |        14038 |      5166734 | x6.77
Mathlib.MeasureTheory.Integral.FundThmCalculus                 |        82623 |      5152695 | x6.40
Mathlib.MeasureTheory.Integral.DominatedConvergence            |        27155 |      5070071 | x6.22
Mathlib.MeasureTheory.Integral.IntervalIntegral                |        74826 |      5042916 | x6.25
Mathlib.MeasureTheory.Integral.SetIntegral                     |       114938 |      4968090 | x5.98
Mathlib.MeasureTheory.Integral.Bochner                         |       228199 |      4853152 | x5.87
Mathlib.MeasureTheory.Integral.SetToL1                         |       262871 |      4624952 | x6.11
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp               |       102223 |      4362081 | x6.42
Mathlib.MeasureTheory.Function.L1Space                         |        90936 |      4259857 | x6.55
Mathlib.MeasureTheory.Function.LpOrder                         |        10425 |      4168921 | x6.67
Mathlib.MeasureTheory.Function.LpSpace                         |       202461 |      4158496 | x6.69
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp           |        24587 |      3956035 | x6.91
Mathlib.MeasureTheory.Integral.MeanInequalities                |        35974 |      3931447 | x6.36
Mathlib.Analysis.MeanInequalities                              |        54169 |      3895472 | x6.17
Mathlib.Analysis.SpecialFunctions.Pow.NNReal                   |        35267 |      3841303 | x5.98
Mathlib.Analysis.SpecialFunctions.Pow.Real                     |        39861 |      3806035 | x6.03
Mathlib.Analysis.SpecialFunctions.Pow.Complex                  |        18269 |      3766174 | x6.08
Mathlib.Analysis.SpecialFunctions.Complex.Log                  |        17681 |      3747905 | x6.11
Mathlib.Analysis.SpecialFunctions.Complex.Arg                  |        42822 |      3730223 | x6.12
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle          |        48465 |      3687400 | x6.17
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic          |        69788 |      3638935 | x6.09
Mathlib.Analysis.SpecialFunctions.Exp                          |        18755 |      3569147 | x6.19
Mathlib.Analysis.Complex.Basic                                 |        70413 |      3550392 | x6.14
Mathlib.Data.Complex.Module                                    |        94305 |      3479978 | x5.85
Mathlib.FieldTheory.Tower                                      |        10483 |      3385673 | x5.18
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                 |        21986 |      3375189 | x5.20
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition           |         9078 |      3353203 | x5.22
Mathlib.LinearAlgebra.Charpoly.Basic                           |        13481 |      3344124 | x5.23
Mathlib.FieldTheory.Minpoly.Field                              |        30077 |      3330643 | x5.25
Mathlib.RingTheory.Algebraic                                   |        33056 |      3300565 | x5.28
Mathlib.RingTheory.IntegralClosure                             |        85731 |      3267509 | x5.32
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                |        38087 |      3181777 | x5.38
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                    |        86962 |      3143689 | x5.43
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                    |        19035 |      3056726 | x5.49
Mathlib.RingTheory.PolynomialAlgebra                           |        36592 |      3037691 | x5.13
Mathlib.RingTheory.MatrixAlgebra                               |        33432 |      3001098 | x5.09
Mathlib.RingTheory.TensorProduct.Basic                         |       231997 |      2967665 | x5.14
Mathlib.LinearAlgebra.FiniteDimensional                        |        99016 |      2735668 | x5.41
Mathlib.LinearAlgebra.Dimension.DivisionRing                   |        57448 |      2636651 | x5.58
Mathlib.LinearAlgebra.Dimension.Constructions                  |        77616 |      2579203 | x5.62
Mathlib.Algebra.Module.Torsion                                 |        78504 |      2501586 | x5.71
Mathlib.GroupTheory.Torsion                                    |        17214 |      2423082 | x5.83
Mathlib.GroupTheory.PGroup                                     |        25650 |      2405867 | x5.87
Mathlib.GroupTheory.SpecificGroups.Cyclic                      |        36439 |      2380217 | x5.82
Mathlib.GroupTheory.Exponent                                   |        25685 |      2343778 | x5.43
Mathlib.Data.Nat.Factorization.Basic                           |        56279 |      2318092 | x5.27
Mathlib.RingTheory.Int.Basic                                   |        15617 |      2261812 | x5.30
Mathlib.RingTheory.PrincipalIdealDomain                        |        22467 |      2246195 | x5.30
Mathlib.RingTheory.UniqueFactorizationDomain                   |        98901 |      2223728 | x5.35
Mathlib.RingTheory.Noetherian                                  |       138260 |      2124826 | x5.53
Mathlib.RingTheory.Nilpotent                                   |        16963 |      1986565 | x5.68
Mathlib.LinearAlgebra.Matrix.ToLin                             |       137541 |      1969602 | x5.70
Mathlib.Algebra.Algebra.Subalgebra.Tower                       |         9468 |      1832060 | x5.86
Mathlib.Algebra.Algebra.Subalgebra.Basic                       |        70064 |      1822592 | x5.87
Mathlib.RingTheory.Ideal.Operations                            |       131287 |      1752527 | x6.06
Mathlib.LinearAlgebra.Basis                                    |       121153 |      1621240 | x5.62
Mathlib.LinearAlgebra.LinearIndependent                        |       100974 |      1500087 | x5.46
Mathlib.LinearAlgebra.Finsupp                                  |       114425 |      1399112 | x5.38
Mathlib.LinearAlgebra.Span                                     |        61802 |      1284686 | x5.16

Bolton Bailey (Apr 07 2024 at 22:02):

Mathlib.LinearAlgebra.Basic                                    |        70224 |      1222884 | x5.01
Mathlib.Algebra.Module.Submodule.Ker                           |        24234 |      1152659 | x5.24
Mathlib.Algebra.Module.Submodule.Map                           |        38621 |      1128425 | x5.34
Mathlib.Algebra.Module.Submodule.Lattice                       |        32241 |      1089803 | x5.47
Mathlib.Algebra.Module.Submodule.Basic                         |        26357 |      1057561 | x5.27
Mathlib.GroupTheory.Submonoid.Membership                       |        28986 |      1031203 | x4.39
Mathlib.Data.Finset.NoncommProd                                |        20422 |      1002216 | x4.28
Mathlib.Algebra.BigOperators.Basic                             |       103835 |       981794 | x4.35
Mathlib.Data.Finset.Preimage                                   |         6250 |       877958 | x4.56
Mathlib.Data.Set.Finite                                        |        42637 |       871707 | x4.59
Mathlib.Data.Finite.Basic                                      |         3171 |       829070 | x4.76
Mathlib.Data.Fintype.Sigma                                     |        20912 |       825899 | x4.51
Mathlib.Data.Finset.Sigma                                      |         8657 |       804986 | x4.55
Mathlib.Data.Finset.Lattice                                    |        69089 |       796329 | x4.58
Mathlib.Data.Finset.Prod                                       |        22763 |       727239 | x4.56
Mathlib.Data.Finset.Card                                       |        18015 |       704475 | x4.67
Mathlib.Data.Finset.Image                                      |        22384 |       686460 | x4.77
Mathlib.Data.Finset.Union                                      |         8709 |       664076 | x4.49
Mathlib.Data.Finset.Basic                                      |        66898 |       655366 | x4.12
Mathlib.Data.Multiset.FinsetOps                                |         7217 |       588467 | x4.37
Mathlib.Data.Multiset.Dedup                                    |         3840 |       581250 | x4.41
Mathlib.Data.Multiset.Nodup                                    |        10156 |       577409 | x4.43
Mathlib.Data.Multiset.Range                                    |         2494 |       567253 | x4.43
Mathlib.Data.Multiset.Basic                                    |        66419 |       564759 | x4.45
Mathlib.Data.List.Perm                                         |        15192 |       498339 | x4.44
Mathlib.Data.List.Dedup                                        |         3342 |       483146 | x4.48
Mathlib.Data.List.Nodup                                        |        11453 |       479804 | x4.51
Mathlib.Data.Set.Pairwise.Basic                                |         9326 |       468350 | x4.34
Mathlib.Data.Set.Function                                      |        26219 |       459024 | x3.98
Mathlib.Data.Set.Prod                                          |        25378 |       432804 | x4.16
Mathlib.Data.Set.Image                                         |        20557 |       407426 | x4.36
Mathlib.Data.Set.Basic                                         |        48565 |       386869 | x4.46
Mathlib.Order.SymmDiff                                         |        16933 |       338303 | x4.55
Mathlib.Order.BooleanAlgebra                                   |        24200 |       321370 | x4.59
Mathlib.Order.Heyting.Basic                                    |        29231 |       297170 | x4.88
Mathlib.Order.PropInstances                                    |         2428 |       267938 | x5.30
Mathlib.Order.Disjoint                                         |        10607 |       265509 | x5.34
Mathlib.Order.BoundedOrder                                     |         7813 |       254902 | x4.38
Mathlib.Order.Lattice                                          |        16407 |       247088 | x4.43
Mathlib.Order.Monotone.Basic                                   |        11154 |       230681 | x4.58
Mathlib.Order.RelClasses                                       |         7947 |       219526 | x4.27
Mathlib.Order.Basic                                            |        17257 |       211578 | x4.21
Mathlib.Tactic.Convert                                         |         3380 |       194320 | x3.79
Mathlib.Tactic.Congr!                                          |        15146 |       190940 | x3.84
Mathlib.Logic.Basic                                            |         9289 |       175793 | x4.03
Mathlib.Init.Function                                          |         2659 |       166503 | x4.02
Mathlib.Tactic.Basic                                           |         4041 |       163844 | x4.03
Std                                                            |          770 |       159803 | x4.09
Std.Data.UnionFind                                             |          645 |       159033 | x1.26
Std.Data.UnionFind.Lemmas                                      |         9872 |       158387 | x1.26
Std.Data.UnionFind.Basic                                       |        23305 |       148515 | x1.28
Std.Data.Array.Lemmas                                          |        38014 |       125209 | x1.27
Std.Data.List.Lemmas                                           |        55036 |        87195 | x1.34
Std.Data.List.Basic                                            |        32158 |        32158 | x1.00

Yaël Dillies (Apr 11 2024 at 22:19):

FieldTheory.Tower -> Data.Complex.Module looks bogus to mz

Yaël Dillies (Apr 11 2024 at 22:19):

FieldTheory.Tower -> Data.Complex.Module looks bogus to mz

Yaël Dillies (Apr 11 2024 at 22:19):

FieldTheory.Tower -> Data.Complex.Module looks bogus to me

Yaël Dillies (Apr 11 2024 at 22:20):

Oh sorry, consecutive lines don't correspond to imports

Bolton Bailey (Apr 11 2024 at 22:57):

Data.Complex.Module imports FieldTheory.Tower, seems like the (first?) reason is that the former has instance : FiniteDimensional ℝ ℂ and FiniteDimensional is defined in the latter.

Anne Baanen (Apr 12 2024 at 07:18):

In Data.Complex.Module we can replace FieldTheory.Tower with LinearAlgebra.FiniteDimensional and still have everything work, except for docs#FiniteDimensional.complexToReal which relies on docs#FiniteDimensional.trans

Anne Baanen (Apr 12 2024 at 07:21):

Actually, looks like there would be no issue moving docs#FiniteDimensional.trans to LinearAlgebra.FiniteDimensional, since it's just a copy of docs#Module.Finite.trans which is defined much higher up the import hierarchy.

Anne Baanen (Apr 12 2024 at 07:33):

#12079

Anne Baanen (Apr 12 2024 at 12:59):

Updated pole:

file                                                           | instructions | parallelism
-------------------------------------------------------------- | ------------ | -----------
Mathlib                                                        | 6296980      | x17.66
Mathlib.NumberTheory.Cyclotomic.PID                            | 6289474      | x8.03
Mathlib.NumberTheory.Cyclotomic.Rat                            | 6280882      | x8.00
Mathlib.NumberTheory.Cyclotomic.Discriminant                   | 6144735      | x8.15
Mathlib.NumberTheory.NumberField.Discriminant                  | 6096480      | x8.04
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody | 5818365      | x8.36
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls           | 5618402      | x7.18
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup           | 5551180      | x7.24
Mathlib.Analysis.SpecialFunctions.Gaussian                     | 5515474      | x7.28
Mathlib.Analysis.Fourier.PoissonSummation                      | 5374842      | x7.10
Mathlib.Analysis.Distribution.SchwartzSpace                    | 5336524      | x6.81
Mathlib.Analysis.SpecialFunctions.JapaneseBracket              | 5165411      | x6.93
Mathlib.MeasureTheory.Integral.Layercake                       | 5093004      | x6.99
Mathlib.Analysis.SpecialFunctions.Integrals                    | 5060935      | x7.03
Mathlib.Analysis.SpecialFunctions.NonIntegrable                | 4945455      | x7.05
Mathlib.MeasureTheory.Integral.FundThmCalculus                 | 4931397      | x6.71
Mathlib.MeasureTheory.Integral.DominatedConvergence            | 4848810      | x6.52
Mathlib.MeasureTheory.Integral.IntervalIntegral                | 4821643      | x6.55
Mathlib.MeasureTheory.Integral.SetIntegral                     | 4746730      | x6.27
Mathlib.MeasureTheory.Integral.Bochner                         | 4633296      | x6.17
Mathlib.MeasureTheory.Integral.SetToL1                         | 4405112      | x6.44
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp               | 4142309      | x6.78
Mathlib.MeasureTheory.Function.L1Space                         | 4040222      | x6.93
Mathlib.MeasureTheory.Function.LpOrder                         | 3949895      | x7.07
Mathlib.MeasureTheory.Function.LpSpace                         | 3939481      | x7.08
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp           | 3737001      | x7.34
Mathlib.MeasureTheory.Function.LpSeminorm.Basic                | 3712412      | x7.27
Mathlib.MeasureTheory.Function.AEEqFun                         | 3657664      | x6.95
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic        | 3624519      | x6.96
Mathlib.Topology.Algebra.Module.FiniteDimension                | 3558210      | x6.06
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                 | 3465216      | x5.07
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition           | 3443228      | x5.09
Mathlib.LinearAlgebra.Charpoly.Basic                           | 3434149      | x5.10
Mathlib.FieldTheory.Minpoly.Field                              | 3420667      | x5.12
Mathlib.RingTheory.Algebraic                                   | 3390598      | x5.15
Mathlib.RingTheory.IntegralClosure                             | 3357514      | x5.18
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                | 3271188      | x5.24
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                    | 3233094      | x5.29
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                    | 3146112      | x5.34
Mathlib.RingTheory.PolynomialAlgebra                           | 3127078      | x4.99
Mathlib.RingTheory.MatrixAlgebra                               | 3090546      | x4.95
Mathlib.RingTheory.TensorProduct.Basic                         | 3057062      | x4.99
Mathlib.LinearAlgebra.FiniteDimensional                        | 2825299      | x5.25
Mathlib.LinearAlgebra.Dimension.DivisionRing                   | 2725676      | x5.40
Mathlib.LinearAlgebra.Dimension.Constructions                  | 2668226      | x5.44
Mathlib.Algebra.Module.Torsion                                 | 2590606      | x5.53
Mathlib.GroupTheory.Torsion                                    | 2512105      | x5.64
Mathlib.GroupTheory.PGroup                                     | 2494895      | x5.67
Mathlib.GroupTheory.SpecificGroups.Cyclic                      | 2469244      | x5.62
Mathlib.GroupTheory.Exponent                                   | 2432809      | x5.22
Mathlib.Data.Nat.Factorization.Basic                           | 2407125      | x5.07
Mathlib.RingTheory.Int.Basic                                   | 2350843      | x5.10
Mathlib.RingTheory.PrincipalIdealDomain                        | 2335226      | x5.10
Mathlib.RingTheory.UniqueFactorizationDomain                   | 2312759      | x5.14
Mathlib.RingTheory.Noetherian                                  | 2213855      | x5.30
Mathlib.RingTheory.Finiteness                                  | 2075469      | x5.49
Mathlib.RingTheory.Nilpotent                                   | 1986404      | x5.68
Mathlib.LinearAlgebra.Matrix.ToLin                             | 1969444      | x5.69
Mathlib.Algebra.Algebra.Subalgebra.Tower                       | 1831905      | x5.85
Mathlib.Algebra.Algebra.Subalgebra.Basic                       | 1822436      | x5.86
Mathlib.RingTheory.Ideal.Operations                            | 1752364      | x6.05
Mathlib.LinearAlgebra.Basis                                    | 1621158      | x5.61
Mathlib.LinearAlgebra.LinearIndependent                        | 1499996      | x5.45
Mathlib.LinearAlgebra.Finsupp                                  | 1399018      | x5.38
Mathlib.LinearAlgebra.Span                                     | 1284597      | x5.15
Mathlib.LinearAlgebra.Basic                                    | 1222798      | x5.02
Mathlib.Algebra.Module.Submodule.Ker                           | 1152575      | x5.26
Mathlib.Algebra.Module.Submodule.Map                           | 1128338      | x5.35
Mathlib.Algebra.Module.Submodule.Lattice                       | 1089713      | x5.48
Mathlib.Algebra.Module.Submodule.Basic                         | 1057470      | x5.29
Mathlib.GroupTheory.Submonoid.Membership                       | 1031111      | x4.40
Mathlib.Data.Finset.NoncommProd                                | 1002127      | x4.29
Mathlib.Algebra.BigOperators.Basic                             | 981701       | x4.36
Mathlib.Data.Finset.Preimage                                   | 877849       | x4.57
Mathlib.Data.Set.Finite                                        | 871596       | x4.60
Mathlib.Data.Finite.Basic                                      | 828959       | x4.77
Mathlib.Data.Fintype.Sigma                                     | 825786       | x4.53
Mathlib.Data.Finset.Sigma                                      | 804870       | x4.57
Mathlib.Data.Finset.Lattice                                    | 796211       | x4.59
Mathlib.Data.Finset.Prod                                       | 727121       | x4.58
Mathlib.Data.Finset.Card                                       | 704357       | x4.69
Mathlib.Data.Finset.Image                                      | 686340       | x4.79
Mathlib.Data.Finset.Union                                      | 663957       | x4.51
Mathlib.Data.Finset.Basic                                      | 655244       | x4.14
Mathlib.Data.Multiset.FinsetOps                                | 588337       | x4.39
Mathlib.Data.Multiset.Dedup                                    | 581116       | x4.43
Mathlib.Data.Multiset.Nodup                                    | 577272       | x4.46
Mathlib.Data.Multiset.Range                                    | 567113       | x4.45
Mathlib.Data.Multiset.Basic                                    | 564617       | x4.47
Mathlib.Data.List.Perm                                         | 498193       | x4.46
Mathlib.Data.List.Dedup                                        | 482999       | x4.51
Mathlib.Data.List.Nodup                                        | 479654       | x4.53
Mathlib.Data.Set.Pairwise.Basic                                | 468199       | x4.35
Mathlib.Data.Set.Function                                      | 458872       | x3.98
Mathlib.Data.Set.Prod                                          | 432996       | x4.16
Mathlib.Data.Set.Image                                         | 407617       | x4.36
Mathlib.Data.Set.Basic                                         | 387059       | x4.45
Mathlib.Order.SymmDiff                                         | 338474       | x4.55
Mathlib.Order.BooleanAlgebra                                   | 321537       | x4.58
Mathlib.Order.Heyting.Basic                                    | 297337       | x4.88
Mathlib.Order.PropInstances                                    | 268096       | x5.30
Mathlib.Order.Disjoint                                         | 265667       | x5.34
Mathlib.Order.BoundedOrder                                     | 255059       | x4.38
Mathlib.Order.Lattice                                          | 247245       | x4.43
Mathlib.Order.Monotone.Basic                                   | 230837       | x4.58
Mathlib.Order.RelClasses                                       | 219587       | x4.27
Mathlib.Order.Basic                                            | 211638       | x4.21
Mathlib.Tactic.Convert                                         | 194380       | x3.79
Mathlib.Tactic.Congr!                                          | 190999       | x3.83
Mathlib.Logic.Basic                                            | 175852       | x4.03
Mathlib.Init.Function                                          | 166502       | x4.02
Mathlib.Tactic.Basic                                           | 163842       | x4.03
...

Anne Baanen (Apr 12 2024 at 12:59):

...
Std                                                            | 159801       | x4.09
Std.Data.UnionFind                                             | 159031       | x1.26
Std.Data.UnionFind.Lemmas                                      | 158386       | x1.26
Std.Data.UnionFind.Basic                                       | 148518       | x1.28
Std.Data.Array.Lemmas                                          | 125213       | x1.27
Std.Data.List.Lemmas                                           | 87194        | x1.34
Std.Data.List.Basic                                            | 32157        | x1.00

Anne Baanen (Apr 12 2024 at 13:04):

Mathlib.RingTheory.IntegralClosureMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap looks a bit weird. Apparently needed to prove docs#Module.End.isIntegral and to state docs#IsIntegral.det. Probably the whole file can be split apart.

Anne Baanen (Apr 12 2024 at 13:20):

Oh I see, this import was used in 8dba065d to generalize to the noncommutative case. I guess it's fine then.

Anne Baanen (Apr 12 2024 at 14:36):

I did some splitting so we can get rid of the import RingTheory.Ideal.OperationsLinearAlgebra.Quotient: #12090

Yaël Dillies (Apr 12 2024 at 17:45):

Yaël Dillies said:

Oh sorry, consecutive lines don't correspond to imports

Nevermind, I misread

Yaël Dillies (Apr 12 2024 at 17:45):

RingTheory.Int.Basic -> Data.Nat.Factorization.Basic is suspicious

Yaël Dillies (Apr 12 2024 at 17:51):

Topology.Algebra.Module.FiniteDimension -> MeasureTheory.Function.StronglyMeasurable also looks a bit weird

Ruben Van de Velde (Apr 12 2024 at 18:23):

Yaël Dillies said:

RingTheory.Int.Basic -> Data.Nat.Factorization.Basic is suspicious

Yeah, I'm looking into this one. theorem factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p goes through UFDs

Ruben Van de Velde (Apr 12 2024 at 19:14):

Ruben Van de Velde said:

Yaël Dillies said:

RingTheory.Int.Basic -> Data.Nat.Factorization.Basic is suspicious

Yeah, I'm looking into this one. theorem factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p goes through UFDs

https://github.com/leanprover-community/mathlib4/compare/wip-factors_count_eq , will try to PR tomorrow

David Loeffler (Apr 12 2024 at 19:51):

I'm coming late to this discussion here; but if the aim here is to shorten the "long pole", then some shortening could be achieved near the very top end by splitting up Analysis.SpecialFunctions.Gaussian. Some of the results in that file require Poisson summation, Schwartz functions, etc; but these aren't the ones needed for the last few files in the "long pole", which (I think) only depend on the first half (ish) of Analysis.SpecialFunctions.Gaussian (which requires slightly less imports).

Ruben Van de Velde (Apr 12 2024 at 19:54):

I don't think the aim is necessarily dogmatically attacking the long pole, but more reviewing if there's any dependencies in the list that look questionable

Yaël Dillies (Apr 12 2024 at 20:07):

Yes, I don't really care about the long pole in itself. I do however care about having a reasonably stratified library

Eric Wieser (Apr 12 2024 at 23:02):

The longest pole is the limiting factor (assuming sufficient compute) for things like:

  • Time taken to wait for a benchmark
  • Time taken to get a build to test a lean nightly

so it is a reasonable think to optimize for in itself

Jireh Loreaux (Apr 12 2024 at 23:45):

Eric, that assumes that files compile in equal time, which is definitely not the case.

Eric Wieser (Apr 12 2024 at 23:49):

Oh, I assumed we were measuring pole length in instructions, not number of files (edit: from the columns in the table above, I think that is what we're doing?)

Eric Wieser (Apr 12 2024 at 23:50):

(unless your point is that instructions are not a great proxy for wall time)

Jireh Loreaux (Apr 13 2024 at 01:22):

Oh, maybe I misunderstood. I thought it was the longest chain of files, but we measured the instructions in the chain. I think you're right though.

David Loeffler (Apr 13 2024 at 07:46):

Eric Wieser said:

The longest pole is the limiting factor (assuming sufficient compute) for things like:

  • Time taken to wait for a benchmark
  • Time taken to get a build to test a lean nightly

so it is a reasonable think to optimize for in itself

On these grounds I have made a PR #12104 which should shorten the long pole somewhat, by removing Mathlib.Analysis.Fourier.PoissonSummation, Mathlib.Analysis.Distribution.SchwartzSpace, and a large fraction of what was formerly in Mathlib.Analysis.SpecialFunctions.Gaussian from the critical path.

David Loeffler (Apr 13 2024 at 07:48):

(I don't know how to benchmark the effect of this change – is the script that generates these long-pole lists public?)

Ruben Van de Velde (Apr 13 2024 at 10:11):

Ruben Van de Velde said:

Ruben Van de Velde said:

Yaël Dillies said:

RingTheory.Int.Basic -> Data.Nat.Factorization.Basic is suspicious

Yeah, I'm looking into this one. theorem factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p goes through UFDs

https://github.com/leanprover-community/mathlib4/compare/wip-factors_count_eq , will try to PR tomorrow

#12105 if someone wants to review

Bolton Bailey (Apr 13 2024 at 16:22):

David Loeffler said:

(I don't know how to benchmark the effect of this change – is the script that generates these long-pole lists public?)

Currently it resides in PR #8361. The quickest process I know to be able to run the script on a pr is:

  1. Merge this PR into the one you want to measure.
  2. Run !bench in GitHub so speed.lean-fro.org benchmarks it.
  3. Once that is done, run the script while in the commit that was benchmarked.

Bolton Bailey (Apr 13 2024 at 16:30):

If you can wait until after your pr is merged, you can also just merge master into the longest_pole branch then do !bench on that.

Bolton Bailey (Apr 13 2024 at 16:32):

Or, perhaps even more simply, someone could just merge #8361 to master and then it would be possible to get the pole in any PR by default without any additional merging.

Kim Morrison (Apr 13 2024 at 19:53):

My memory is that this is counting instructions, retrieved from the speed center, but I haven't looked at the code recently!

Kim Morrison (Apr 13 2024 at 19:54):

It's intended to be a proxy for build time assuming infinite parallelism.

Kim Morrison (Apr 13 2024 at 19:56):

Hopefully as we shorten the pole it re-routes through different parts of the library (i.e. helping us avoid over optimizing on some areas).

Bolton Bailey (Apr 13 2024 at 22:07):

Kim Morrison said:

My memory is that this is counting instructions, retrieved from the speed center, but I haven't looked at the code recently!

Yes this is right, it gets the instruction counts from speed center and it gets the import graph from ImportGraph. You can ask speedcenter to give you a graph for a different commit, but unfortunately I don't know enough about ImportGraph to know if it can give me an import graph for a different commit.

Jon Eugster (Apr 14 2024 at 16:23):

As far as I know, ImportGraph gets the project structure from the built oleans, so I think the answer is "no", unless you check out and download cache for that commit manually.

Mario Carneiro (Apr 14 2024 at 17:02):

If ImportGraph is only looking at file-to-file imports, it should be easy to get that from the .lean files instead of .olean's, would that be useful?

Anne Baanen (Apr 19 2024 at 12:54):

Anne Baanen said:

I did some splitting so we can get rid of the import RingTheory.Ideal.OperationsLinearAlgebra.Quotient: #12090

I was going to do this next but I got ill, so please enjoy this delayed deletion of the import Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations: #12267

Ruben Van de Velde (Apr 19 2024 at 13:10):

Hope you're feeling better! You may be interested in #12184 as well (which #12090 will bitrot slightly)

Bolton Bailey (Apr 28 2024 at 00:42):

Analyzing Mathlib at 02bb10d877e8044bcc5e429b43db03a7868fff29
file                                                           | instructions | (cumulative) | parallelism
-------------------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                                        |         7557 |      6075834 | x18.54
Mathlib.NumberTheory.Cyclotomic.PID                            |         8571 |      6068277 | x8.12
Mathlib.NumberTheory.Cyclotomic.Rat                            |       133971 |      6059706 | x8.10
Mathlib.NumberTheory.Cyclotomic.Discriminant                   |        48246 |      5925734 | x8.25
Mathlib.NumberTheory.NumberField.Discriminant                  |       276543 |      5877488 | x8.13
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody |       199477 |      5600944 | x8.47
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic      |       218422 |      5401467 | x8.33
Mathlib.NumberTheory.NumberField.Embeddings                    |       108135 |      5183044 | x7.72
Mathlib.Analysis.Complex.Polynomial                            |        26471 |      5074908 | x7.56
Mathlib.Analysis.Complex.Liouville                             |        16349 |      5048437 | x7.26
Mathlib.Analysis.Complex.CauchyIntegral                        |        46224 |      5032088 | x7.28
Mathlib.MeasureTheory.Integral.CircleIntegral                  |        67000 |      4985863 | x7.13
Mathlib.Analysis.SpecialFunctions.NonIntegrable                |        14098 |      4918862 | x7.15
Mathlib.MeasureTheory.Integral.FundThmCalculus                 |        85436 |      4904764 | x6.80
Mathlib.MeasureTheory.Integral.DominatedConvergence            |        27318 |      4819328 | x6.62
Mathlib.MeasureTheory.Integral.IntervalIntegral                |        74961 |      4792010 | x6.65
Mathlib.MeasureTheory.Integral.SetIntegral                     |       114757 |      4717048 | x6.37
Mathlib.MeasureTheory.Integral.Bochner                         |       228811 |      4602290 | x6.26
Mathlib.MeasureTheory.Integral.SetToL1                         |       262883 |      4373479 | x6.54
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp               |       102235 |      4110595 | x6.89
Mathlib.MeasureTheory.Function.L1Space                         |        91289 |      4008359 | x7.04
Mathlib.MeasureTheory.Function.LpOrder                         |        10455 |      3917070 | x7.18
Mathlib.MeasureTheory.Function.LpSpace                         |       202478 |      3906615 | x7.20
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp           |        24632 |      3704137 | x7.46
Mathlib.MeasureTheory.Function.LpSeminorm.Basic                |        54788 |      3679504 | x7.40
Mathlib.MeasureTheory.Function.AEEqFun                         |        33177 |      3624716 | x7.08
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic        |        66353 |      3591538 | x7.09
Mathlib.Topology.Algebra.Module.FiniteDimension                |        93030 |      3525185 | x6.17
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                 |        21912 |      3432155 | x5.17
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition           |         9129 |      3410242 | x5.19
Mathlib.LinearAlgebra.Charpoly.Basic                           |        13678 |      3401113 | x5.20
Mathlib.FieldTheory.Minpoly.Field                              |        30154 |      3387434 | x5.22
Mathlib.RingTheory.Algebraic                                   |        33527 |      3357279 | x5.25
Mathlib.RingTheory.IntegralClosure                             |        87882 |      3323752 | x5.29
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                |        38388 |      3235869 | x5.35
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                    |        87282 |      3197481 | x5.40
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                    |        19108 |      3110199 | x5.45
Mathlib.RingTheory.PolynomialAlgebra                           |        36681 |      3091090 | x5.10
Mathlib.RingTheory.MatrixAlgebra                               |        33650 |      3054409 | x5.06
Mathlib.RingTheory.TensorProduct.Basic                         |       279177 |      3020758 | x5.11
Mathlib.LinearAlgebra.FiniteDimensional                        |       101642 |      2741581 | x5.45
Mathlib.LinearAlgebra.Dimension.DivisionRing                   |        47963 |      2639938 | x5.62
Mathlib.LinearAlgebra.Dimension.RankNullity                    |        27173 |      2591974 | x5.67
Mathlib.LinearAlgebra.Dimension.Constructions                  |        89051 |      2564801 | x5.69
Mathlib.Algebra.Module.Torsion                                 |        79516 |      2475749 | x5.80
Mathlib.GroupTheory.Torsion                                    |        17471 |      2396233 | x5.93
Mathlib.GroupTheory.PGroup                                     |        25768 |      2378762 | x5.97
Mathlib.GroupTheory.SpecificGroups.Cyclic                      |        36693 |      2352993 | x5.92
Mathlib.GroupTheory.Exponent                                   |        25889 |      2316299 | x5.50
Mathlib.Data.Nat.Factorization.Basic                           |        56391 |      2290409 | x5.34
Mathlib.RingTheory.Int.Basic                                   |        15653 |      2234017 | x5.38
Mathlib.RingTheory.PrincipalIdealDomain                        |        22817 |      2218364 | x5.38
Mathlib.RingTheory.UniqueFactorizationDomain                   |        97989 |      2195546 | x5.42
Mathlib.RingTheory.Noetherian                                  |       137500 |      2097557 | x5.60
Mathlib.RingTheory.Finiteness                                  |        89730 |      1960057 | x5.82
Mathlib.RingTheory.Nilpotent                                   |        17076 |      1870326 | x6.04
Mathlib.LinearAlgebra.Matrix.ToLin                             |       142896 |      1853249 | x5.85
Mathlib.Algebra.Algebra.Subalgebra.Tower                       |         9393 |      1710353 | x5.60
Mathlib.Algebra.Algebra.Subalgebra.Basic                       |        50649 |      1700959 | x5.62
Mathlib.Algebra.Algebra.Operations                             |        92569 |      1650310 | x5.76
Mathlib.Algebra.Algebra.Bilinear                               |        20234 |      1557740 | x5.06
Mathlib.LinearAlgebra.TensorProduct.Basic                      |       214317 |      1537506 | x4.52
Mathlib.Algebra.Module.Submodule.Bilinear                      |        13848 |      1323188 | x5.07

Bolton Bailey (Apr 28 2024 at 00:42):

Mathlib.LinearAlgebra.Span                                     |        62342 |      1309340 | x5.04
Mathlib.LinearAlgebra.Basic                                    |        70639 |      1246998 | x4.91
Mathlib.Algebra.Module.Submodule.Ker                           |        24499 |      1176358 | x5.13
Mathlib.Algebra.Module.Submodule.Map                           |        38777 |      1151859 | x5.22
Mathlib.Algebra.Module.Submodule.Lattice                       |        32691 |      1113081 | x5.35
Mathlib.Algebra.Module.Equiv                                   |        50562 |      1080390 | x3.93
Mathlib.Algebra.Module.LinearMap.End                           |        37265 |      1029827 | x4.07
Mathlib.Algebra.Module.LinearMap.Basic                         |       110905 |       992562 | x4.19
Mathlib.GroupTheory.GroupAction.Hom                            |        55618 |       881656 | x4.52
Mathlib.Algebra.Module.Basic                                   |        48234 |       826038 | x4.72
Mathlib.Tactic.Abel                                            |        25440 |       777803 | x4.79
Mathlib.Tactic.NormNum                                         |         1924 |       752362 | x4.91
Mathlib.Tactic.NormNum.DivMod                                  |        11035 |       750437 | x4.86
Mathlib.Tactic.NormNum.Ineq                                    |        26623 |       739402 | x4.92
Mathlib.Tactic.NormNum.Eq                                      |         7355 |       712778 | x5.04
Mathlib.Tactic.NormNum.Inv                                     |        16749 |       705423 | x5.08
Mathlib.Data.Rat.Cast.CharZero                                 |         4956 |       688673 | x5.07
Mathlib.Data.Rat.Cast.Defs                                     |        10168 |       683717 | x5.00
Mathlib.Data.Rat.Field                                         |         2953 |       673548 | x4.99
Mathlib.Algebra.Order.Nonneg.Field                             |        16181 |       670594 | x4.77
Mathlib.Algebra.Order.Nonneg.Ring                              |        33701 |       654413 | x4.72
Mathlib.Order.CompleteLatticeIntervals                         |        12349 |       620711 | x3.92
Mathlib.Order.ConditionallyCompleteLattice.Basic               |        30199 |       608362 | x3.89
Mathlib.Data.Set.Lattice                                       |        43130 |       578162 | x4.03
Mathlib.Order.CompleteBooleanAlgebra                           |        26474 |       535032 | x3.89
Mathlib.Order.CompleteLattice                                  |        34588 |       508558 | x4.04
Mathlib.Order.Hom.Set                                          |         3291 |       473969 | x4.04
Mathlib.Logic.Equiv.Set                                        |        14805 |       470677 | x3.93
Mathlib.Data.Set.Function                                      |        25877 |       455872 | x4.02
Mathlib.Data.Set.Prod                                          |        25370 |       429995 | x4.20
Mathlib.Data.Set.Image                                         |        20536 |       404624 | x4.40
Mathlib.Data.Set.Subsingleton                                  |         4475 |       384087 | x4.50
Mathlib.Data.Set.Basic                                         |        44493 |       379612 | x4.54
Mathlib.Order.SymmDiff                                         |        16941 |       335118 | x4.61
Mathlib.Order.BooleanAlgebra                                   |        24199 |       318177 | x4.65
Mathlib.Order.Heyting.Basic                                    |        29241 |       293978 | x4.95
Mathlib.Order.PropInstances                                    |         2431 |       264736 | x5.38
Mathlib.Order.Disjoint                                         |        10608 |       262305 | x5.42
Mathlib.Order.BoundedOrder                                     |         7817 |       251697 | x4.45
Mathlib.Order.Lattice                                          |        16411 |       243880 | x4.50
Mathlib.Order.Monotone.Basic                                   |        11254 |       227468 | x4.67
Mathlib.Order.RelClasses                                       |         7951 |       216214 | x4.36
Mathlib.Order.Basic                                            |        17261 |       208263 | x4.29
Mathlib.Tactic.Convert                                         |         3383 |       191001 | x3.87
Mathlib.Tactic.Congr!                                          |        15149 |       187618 | x3.92
Mathlib.Logic.Basic                                            |         9200 |       172468 | x4.13
Mathlib.Init.Function                                          |         2661 |       163267 | x4.12
Mathlib.Tactic.Basic                                           |         4043 |       160606 | x4.14
Std                                                            |          772 |       156563 | x4.20
Std.Data.UnionFind                                             |          645 |       155791 | x1.29
Std.Data.UnionFind.Lemmas                                      |         9868 |       155145 | x1.29
Std.Data.UnionFind.Basic                                       |        23302 |       145277 | x1.31
Std.Data.Array.Lemmas                                          |        34812 |       121974 | x1.31
Std.Data.List.Lemmas                                           |        55003 |        87162 | x1.35
Std.Data.List.Basic                                            |        32159 |        32159 | x1.00

Bolton Bailey (Apr 28 2024 at 00:43):

Pretty cool to see the top-line cumulative instruction count come down over the past few weeks!

Yaël Dillies (Apr 28 2024 at 06:22):

@Ruben Van de Velde, did you open a PR for the RingTheory.Int.Basic -> Data.Nat.Factorization.Basic import?

Bolton Bailey (Apr 28 2024 at 06:48):

#12105, I think.

Ruben Van de Velde (Apr 28 2024 at 07:34):

Juggling too many things - looks like Kim put it on the bors queue

Ruben Van de Velde (Apr 28 2024 at 07:35):

I'm hoping #12311 will help a little too

Ruben Van de Velde (Apr 28 2024 at 07:37):

How is RingTheory.Nilpotent still in the list after #12184, though?

Yaël Dillies (Apr 28 2024 at 08:08):

Also I should advertise the trio #11986, #11863, #11855 that will clean up things slightly off the pole

Yaël Dillies (Apr 28 2024 at 08:15):

So I believe we should make it so that `GroupTheory.Torsion does not transitively import Algebra.Module.Submodule.Basic. Is that the case after #12105 ?

Ruben Van de Velde (Apr 28 2024 at 08:18):

No, it's not yet the case. Let me see what the path is

Ruben Van de Velde (Apr 28 2024 at 08:19):

It is defined in Mathlib.Algebra.Module.Submodule.Basic,
  which is imported by Mathlib.Algebra.Module.Submodule.Lattice,
  which is imported by Mathlib.Algebra.Module.Submodule.Map,
  which is imported by Mathlib.Algebra.Module.Submodule.Ker,
  which is imported by Mathlib.Algebra.Algebra.Basic,
  which is imported by Mathlib.Algebra.Algebra.Hom,
  which is imported by Mathlib.Algebra.Algebra.NonUnitalHom,
  which is imported by Mathlib.Algebra.Algebra.Bilinear,
  which is imported by Mathlib.Algebra.Algebra.Operations,
  which is imported by Mathlib.RingTheory.Ideal.Operations,
  which is imported by Mathlib.Data.ZMod.Basic,
  which is imported by Mathlib.Data.ZMod.Quotient,
  which is imported by Mathlib.GroupTheory.Exponent,
  which is imported by Mathlib.GroupTheory.SpecificGroups.Cyclic,
  which is imported by Mathlib.GroupTheory.PGroup,
  which is imported by this file.

Much appreciation to whoever added that to assert_not_exists

Ruben Van de Velde (Apr 28 2024 at 08:19):

Data.ZMod.Basic seems like a good target

Ruben Van de Velde (Apr 28 2024 at 08:28):

#12478 is a start, but I probably won't continue with it for now

Ruben Van de Velde (Apr 28 2024 at 08:34):

Yaël Dillies said:

So I believe we should make it so that `GroupTheory.Torsion does not transitively import Algebra.Module.Submodule.Basic. Is that the case after #12105 ?

There's still other paths too;

  • Mathlib.Algebra.Group.UniqueProdsMathlib.LinearAlgebra.Basis.VectorSpace
  • Mathlib.GroupTheory.Exponent → Mathlib.Data.ZMod.Quotient → Mathlib.RingTheory.Int.Basic/Mathlib.RingTheory.Ideal.QuotientOperations
  • Mathlib.Algebra.FreeAlgebra → Mathlib.RingTheory.Adjoin.Basic/Mathlib.Algebra.Algebra.Subalgebra.Basic

Yaël Dillies (Apr 28 2024 at 09:19):

Ruben Van de Velde said:

Much appreciation to whoever added that to assert_not_exists

I asked for it but I don't actually know who implemented it

Michael Rothgang (Apr 28 2024 at 10:38):

Ruben Van de Velde said:

#12478 is a start, but I probably won't continue with it for now

I had some time and finished it - reviews welcome. (Sorry, not sorry for adding some documentation in the process.)

Kim Morrison (Apr 28 2024 at 21:57):

Has anyone looked recently at the stretch:

Mathlib.GroupTheory.Exponent
Mathlib.Data.Nat.Factorization.Basic
Mathlib.RingTheory.Int.Basic
Mathlib.RingTheory.PrincipalIdealDomain
Mathlib.RingTheory.UniqueFactorizationDomain
Mathlib.RingTheory.Noetherian

I would hope one could at least define group-theoretic exponents without knowing what a Noetherian ring is.

Yaël Dillies (Apr 28 2024 at 22:02):

It's comprised within my comment above but I haven't tried anything with it yet (nor will I have the time, most likely

Bolton Bailey (Apr 28 2024 at 22:05):

Analyzing Mathlib at 28c802f9bf63b6766003fe0cfcd1830f9d3692e1
file                                                           | instructions | (cumulative) | parallelism
-------------------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                                        |         7581 |      5896677 | x18.98
Mathlib.NumberTheory.Cyclotomic.PID                            |         8519 |      5889095 | x8.32
Mathlib.NumberTheory.Cyclotomic.Rat                            |       127515 |      5880576 | x8.29
Mathlib.NumberTheory.Cyclotomic.Discriminant                   |        45372 |      5753060 | x8.45
Mathlib.NumberTheory.NumberField.Discriminant                  |       257639 |      5707687 | x8.32
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody |       196404 |      5450048 | x8.66
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic      |       215976 |      5253643 | x8.52
Mathlib.NumberTheory.NumberField.Embeddings                    |       104846 |      5037667 | x7.90
Mathlib.Analysis.Complex.Polynomial                            |        25863 |      4932821 | x7.75
Mathlib.Analysis.Complex.Liouville                             |        15996 |      4906957 | x7.44
Mathlib.Analysis.Complex.CauchyIntegral                        |        46078 |      4890961 | x7.46
Mathlib.MeasureTheory.Integral.CircleIntegral                  |        65734 |      4844882 | x7.31
Mathlib.Analysis.SpecialFunctions.NonIntegrable                |        14013 |      4779148 | x7.33
Mathlib.MeasureTheory.Integral.FundThmCalculus                 |        83110 |      4765134 | x6.98
Mathlib.MeasureTheory.Integral.DominatedConvergence            |        26598 |      4682023 | x6.80
Mathlib.MeasureTheory.Integral.IntervalIntegral                |        73067 |      4655424 | x6.83
Mathlib.MeasureTheory.Integral.SetIntegral                     |       111542 |      4582357 | x6.55
Mathlib.MeasureTheory.Integral.Bochner                         |       224061 |      4470814 | x6.44
Mathlib.MeasureTheory.Integral.SetToL1                         |       258830 |      4246753 | x6.73
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp               |        95663 |      3987923 | x7.10
Mathlib.MeasureTheory.Function.L1Space                         |        92186 |      3892259 | x7.25
Mathlib.MeasureTheory.Function.LpOrder                         |        10468 |      3800072 | x7.40
Mathlib.MeasureTheory.Function.LpSpace                         |       197232 |      3789604 | x7.42
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp           |        24411 |      3592371 | x7.70
Mathlib.MeasureTheory.Function.LpSeminorm.Basic                |        53842 |      3567959 | x7.63
Mathlib.MeasureTheory.Function.AEEqFun                         |        33186 |      3514116 | x7.31
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic        |        64680 |      3480930 | x7.32
Mathlib.Topology.Algebra.Module.FiniteDimension                |        92236 |      3416250 | x6.39
Mathlib.LinearAlgebra.FreeModule.Finite.Matrix                 |        21302 |      3324013 | x5.36
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition           |         9143 |      3302711 | x5.38
Mathlib.LinearAlgebra.Charpoly.Basic                           |        13703 |      3293567 | x5.39
Mathlib.FieldTheory.Minpoly.Field                              |        30203 |      3279864 | x5.41
Mathlib.RingTheory.Algebraic                                   |        32977 |      3249661 | x5.45
Mathlib.RingTheory.IntegralClosure                             |        86918 |      3216683 | x5.49
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap                |        37973 |      3129765 | x5.55
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                    |        83945 |      3091792 | x5.61
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                    |        18850 |      3007846 | x5.66

Bolton Bailey (Apr 28 2024 at 22:05):

Mathlib.RingTheory.PolynomialAlgebra                           |        36431 |      2988995 | x5.30
Mathlib.RingTheory.MatrixAlgebra                               |        32923 |      2952564 | x5.26
Mathlib.RingTheory.TensorProduct.Basic                         |       279572 |      2919640 | x5.31
Mathlib.LinearAlgebra.FiniteDimensional                        |       100402 |      2640068 | x5.77
Mathlib.LinearAlgebra.Dimension.DivisionRing                   |        46884 |      2539665 | x5.95
Mathlib.LinearAlgebra.Dimension.RankNullity                    |        27125 |      2492781 | x6.00
Mathlib.LinearAlgebra.Dimension.Constructions                  |        85723 |      2465655 | x6.03
Mathlib.Algebra.Module.Torsion                                 |        77407 |      2379932 | x6.16
Mathlib.GroupTheory.Torsion                                    |        17375 |      2302525 | x6.29
Mathlib.GroupTheory.PGroup                                     |        25647 |      2285149 | x6.34
Mathlib.GroupTheory.SpecificGroups.Cyclic                      |        36279 |      2259502 | x6.29
Mathlib.GroupTheory.Exponent                                   |        25350 |      2223223 | x5.76
Mathlib.Data.ZMod.Quotient                                     |        20200 |      2197873 | x5.75
Mathlib.RingTheory.Int.Basic                                   |        15479 |      2177672 | x5.53
Mathlib.RingTheory.PrincipalIdealDomain                        |        22823 |      2162193 | x5.53
Mathlib.RingTheory.UniqueFactorizationDomain                   |        97990 |      2139369 | x5.57
Mathlib.RingTheory.Noetherian                                  |       135236 |      2041379 | x5.77
Mathlib.RingTheory.Nilpotent.Lemmas                            |         6812 |      1906143 | x5.93
Mathlib.LinearAlgebra.Matrix.ToLin                             |       143061 |      1899331 | x5.74
Mathlib.Algebra.Algebra.Subalgebra.Tower                       |         9400 |      1756269 | x5.50
Mathlib.Algebra.Algebra.Subalgebra.Basic                       |        50664 |      1746868 | x5.51
Mathlib.Algebra.Algebra.Operations                             |        92843 |      1696204 | x5.64
Mathlib.Algebra.Algebra.Bilinear                               |        20237 |      1603361 | x4.96
Mathlib.LinearAlgebra.TensorProduct.Basic                      |       244766 |      1583123 | x4.43
Mathlib.Algebra.Module.Submodule.Bilinear                      |        13851 |      1338357 | x5.03
Mathlib.LinearAlgebra.Span                                     |        62259 |      1324505 | x5.01
Mathlib.LinearAlgebra.Basic                                    |        51556 |      1262245 | x4.87
Mathlib.Algebra.Module.Submodule.Range                         |        23542 |      1210689 | x5.02
Mathlib.Algebra.Module.Submodule.Ker                           |        24509 |      1187146 | x5.10
Mathlib.Algebra.Module.Submodule.Map                           |        38798 |      1162637 | x5.19
Mathlib.Algebra.Module.Submodule.Lattice                       |        32691 |      1123839 | x5.32
Mathlib.Algebra.Module.Equiv                                   |        50598 |      1091148 | x3.91
Mathlib.Algebra.Module.LinearMap.End                           |        37313 |      1040549 | x4.05
Mathlib.Algebra.Module.LinearMap.Basic                         |       110901 |      1003235 | x4.16
Mathlib.GroupTheory.GroupAction.Hom                            |        55621 |       892333 | x4.49
Mathlib.Algebra.Module.Basic                                   |        48022 |       836712 | x4.69
Mathlib.Tactic.Abel                                            |        25450 |       788689 | x4.75
Mathlib.Tactic.NormNum                                         |         1926 |       763239 | x4.87
Mathlib.Tactic.NormNum.DivMod                                  |        11050 |       761313 | x4.82
Mathlib.Tactic.NormNum.Ineq                                    |        26626 |       750262 | x4.88
Mathlib.Tactic.NormNum.Eq                                      |         7369 |       723635 | x4.99
Mathlib.Tactic.NormNum.Inv                                     |        16769 |       716266 | x5.03
Mathlib.Data.Rat.Cast.CharZero                                 |         4967 |       699496 | x5.02
Mathlib.Data.Rat.Cast.Defs                                     |        15473 |       694529 | x4.95
Mathlib.Data.Rat.Field                                         |         3013 |       679055 | x4.97
Mathlib.Algebra.Order.Nonneg.Field                             |        20924 |       676042 | x4.75
Mathlib.Algebra.Order.Nonneg.Ring                              |        33702 |       655118 | x4.72
Mathlib.Order.CompleteLatticeIntervals                         |        12349 |       621415 | x3.91
Mathlib.Order.ConditionallyCompleteLattice.Basic               |        30198 |       609066 | x3.88
Mathlib.Data.Set.Lattice                                       |        43130 |       578868 | x4.03
Mathlib.Order.CompleteBooleanAlgebra                           |        26912 |       535737 | x3.89
Mathlib.Order.CompleteLattice                                  |        34587 |       508824 | x4.04
Mathlib.Order.Hom.Set                                          |         3291 |       474237 | x4.04
Mathlib.Logic.Equiv.Set                                        |        14804 |       470945 | x3.93
Mathlib.Data.Set.Function                                      |        25877 |       456141 | x4.02
Mathlib.Data.Set.Prod                                          |        25370 |       430263 | x4.20
Mathlib.Data.Set.Image                                         |        20538 |       404892 | x4.40
Mathlib.Data.Set.Subsingleton                                  |         4476 |       384354 | x4.50
Mathlib.Data.Set.Basic                                         |        44491 |       379877 | x4.54
Mathlib.Order.SymmDiff                                         |        17197 |       335386 | x4.61
Mathlib.Order.BooleanAlgebra                                   |        24200 |       318189 | x4.65
Mathlib.Order.Heyting.Basic                                    |        29242 |       293988 | x4.95
Mathlib.Order.PropInstances                                    |         2431 |       264746 | x5.38
Mathlib.Order.Disjoint                                         |        10607 |       262314 | x5.43
Mathlib.Order.BoundedOrder                                     |         7818 |       251707 | x4.45
Mathlib.Order.Lattice                                          |        16412 |       243889 | x4.51
Mathlib.Order.Monotone.Basic                                   |        11254 |       227476 | x4.67
Mathlib.Order.RelClasses                                       |         7951 |       216222 | x4.36
Mathlib.Order.Basic                                            |        17262 |       208270 | x4.30
Mathlib.Tactic.Convert                                         |         3383 |       191008 | x3.87
Mathlib.Tactic.Congr!                                          |        15149 |       187624 | x3.92
Mathlib.Logic.Basic                                            |         9201 |       172474 | x4.13
Mathlib.Init.Function                                          |         2661 |       163272 | x4.12
Mathlib.Tactic.Basic                                           |         4043 |       160611 | x4.14
Std                                                            |          772 |       156568 | x4.20
Std.Data.UnionFind                                             |          645 |       155795 | x1.29
Std.Data.UnionFind.Lemmas                                      |         9870 |       155150 | x1.29
Std.Data.UnionFind.Basic                                       |        23303 |       145280 | x1.31
Std.Data.Array.Lemmas                                          |        34811 |       121976 | x1.31
Std.Data.List.Lemmas                                           |        55006 |        87164 | x1.35
Std.Data.List.Basic                                            |        32158 |        32158 | x1.00

Bolton Bailey (Apr 28 2024 at 22:06):

Now with the RingTheory.Int.Basic -> Data.Nat.Factorization.Basic import removed, the pole has gone down by another ~3%

Bolton Bailey (Apr 28 2024 at 22:08):

@Kim Morrison would you like to merge the #8361 PR? It would be much easier to assess other PRs with this executable if it was in master. It's delegated but I don't think I can merge it because I am not technically the owner.

Ruben Van de Velde (Jun 10 2024 at 12:51):

Update:

Analyzing Mathlib at fe5e871112c20e1471ba2a80c6c75eba41fe8417
file                                                           | instructions | (cumulative) | parallelism
-------------------------------------------------------------- | ------------ | ------------ | -----------
Mathlib                                                        |         7998 |      5636164 | x21.45
Mathlib.NumberTheory.Cyclotomic.Three                          |        33249 |      5628166 | x9.10
Mathlib.NumberTheory.Cyclotomic.Rat                            |       116385 |      5594916 | x9.08
Mathlib.NumberTheory.Cyclotomic.Discriminant                   |        42628 |      5478531 | x9.24
Mathlib.NumberTheory.NumberField.Discriminant                  |       216400 |      5435902 | x9.16
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody |       188716 |      5219502 | x9.48
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls           |        63478 |      5030785 | x7.68
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup           |        37620 |      4967307 | x7.74
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral    |        38273 |      4929686 | x7.79
Mathlib.Analysis.SpecialFunctions.Gamma.Basic                  |        39222 |      4891413 | x7.83
Mathlib.Analysis.MellinTransform                               |        40460 |      4852190 | x7.89
Mathlib.Analysis.SpecialFunctions.ImproperIntegrals            |        15869 |      4811730 | x7.93
Mathlib.Analysis.SpecialFunctions.JapaneseBracket              |        98533 |      4795861 | x7.70
Mathlib.MeasureTheory.Integral.Layercake                       |        29849 |      4697327 | x7.81
Mathlib.Analysis.SpecialFunctions.Integrals                    |       115401 |      4667478 | x7.85
Mathlib.Analysis.SpecialFunctions.NonIntegrable                |        14974 |      4552077 | x7.89
Mathlib.MeasureTheory.Integral.FundThmCalculus                 |        90501 |      4537102 | x7.49
Mathlib.MeasureTheory.Integral.DominatedConvergence            |        28183 |      4446601 | x7.29
Mathlib.MeasureTheory.Integral.IntervalIntegral                |        77246 |      4418417 | x7.33
Mathlib.MeasureTheory.Integral.SetIntegral                     |       119067 |      4341171 | x7.01
Mathlib.MeasureTheory.Integral.Bochner                         |       242278 |      4222103 | x6.83
Mathlib.MeasureTheory.Integral.SetToL1                         |       309259 |      3979824 | x7.19
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp               |       103970 |      3670565 | x7.71
Mathlib.MeasureTheory.Function.L1Space                         |       106081 |      3566594 | x7.90
Mathlib.MeasureTheory.Function.LpOrder                         |        11050 |      3460512 | x8.11
Mathlib.MeasureTheory.Function.LpSpace                         |       231233 |      3449462 | x8.14
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp           |        26568 |      3218229 | x8.55
Mathlib.MeasureTheory.Function.LpSeminorm.Basic                |        58634 |      3191660 | x8.48
Mathlib.MeasureTheory.Function.AEEqFun                         |        35299 |      3133026 | x8.15
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic        |        71337 |      3097727 | x8.17
Mathlib.Analysis.NormedSpace.BoundedLinearMaps                 |        95827 |      3026389 | x6.51
Mathlib.Analysis.NormedSpace.Multilinear.Basic                 |       355228 |      2930562 | x6.46
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace          |        75087 |      2575334 | x7.09
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear             |       160601 |      2500246 | x7.26
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic                |       106216 |      2339645 | x7.69
Mathlib.Analysis.LocallyConvex.WithSeminorms                   |       105751 |      2233429 | x7.89
Mathlib.Topology.Algebra.Equicontinuity                        |         7248 |      2127677 | x7.35
Mathlib.Topology.Algebra.UniformConvergence                    |        32781 |      2120428 | x7.38
Mathlib.Analysis.LocallyConvex.Bounded                         |        40104 |      2087647 | x7.46
Mathlib.Analysis.Seminorm                                      |       172620 |      2047542 | x7.38
Mathlib.Analysis.LocallyConvex.Basic                           |        38838 |      1874921 | x7.86
Mathlib.Analysis.NormedSpace.Basic                             |        29705 |      1836083 | x7.58
Mathlib.Analysis.Normed.MulAction                              |        18352 |      1806377 | x7.66
Mathlib.Analysis.Normed.Field.Basic                            |        88589 |      1788024 | x7.73
Mathlib.Analysis.Normed.Group.Basic                            |       101645 |      1699435 | x6.83
Mathlib.Topology.MetricSpace.IsometricSMul                     |        30951 |      1597789 | x6.51
Mathlib.Topology.MetricSpace.Isometry                          |        13635 |      1566837 | x5.39
Mathlib.Topology.MetricSpace.Antilipschitz                     |         8227 |      1553201 | x5.43
Mathlib.Topology.MetricSpace.Bounded                           |        14045 |      1544974 | x5.43
Mathlib.Topology.MetricSpace.ProperSpace                       |         5495 |      1530928 | x5.47
Mathlib.Topology.Algebra.Order.Compact                         |        27904 |      1525433 | x4.17
Mathlib.Topology.Order.IntermediateValue                       |        51399 |      1497529 | x4.12
Mathlib.Topology.Order.DenselyOrdered                          |        86087 |      1446129 | x4.22
Mathlib.Topology.Order.IsLUB                                   |        15668 |      1360042 | x4.42
Mathlib.Topology.Order.LeftRightNhds                           |        32992 |      1344373 | x4.46
Mathlib.Topology.Order.Basic                                   |        36970 |      1311380 | x4.53
Mathlib.Topology.Order.OrderClosed                             |        30423 |      1274410 | x4.16
Mathlib.Topology.Separation                                    |        45321 |      1243987 | x4.23
Mathlib.Topology.Compactness.SigmaCompact                      |         8107 |      1198665 | x4.19
Mathlib.Topology.Compactness.LocallyCompact                    |         5462 |      1190558 | x4.22
Mathlib.Topology.Compactness.Compact                           |        28692 |      1185095 | x4.23
Mathlib.Topology.Bases                                         |        31552 |      1156403 | x4.29
Mathlib.Topology.ContinuousOn                                  |        28725 |      1124850 | x4.39
Mathlib.Topology.Constructions                                 |        37151 |      1096125 | x4.48
Mathlib.Topology.Maps                                          |        12106 |      1058973 | x4.59
Mathlib.Topology.Order                                         |        17094 |      1046867 | x4.63
Mathlib.Topology.Defs.Induced                                  |         3502 |      1029772 | x4.69
Mathlib.Topology.Basic                                         |        30405 |      1026269 | x4.71
Mathlib.Topology.Defs.Filter                                   |         8021 |       995863 | x4.81
Mathlib.Order.Filter.Ultrafilter                               |        12329 |       987842 | x4.72
Mathlib.Order.Filter.Cofinite                                  |         6144 |       975512 | x4.70
Mathlib.Order.Filter.AtTopBot                                  |        64243 |       969367 | x4.71
Mathlib.Order.Filter.Bases                                     |        21730 |       905123 | x4.58
Mathlib.Order.Filter.Prod                                      |        16155 |       883393 | x4.29
Mathlib.Order.Filter.Basic                                     |        62918 |       867238 | x4.35
Mathlib.Data.Set.Finite                                        |        35271 |       804320 | x4.46
Mathlib.Data.Finite.Basic                                      |         3253 |       769048 | x4.61
Mathlib.Data.Fintype.Sigma                                     |        15609 |       765794 | x4.41
Mathlib.Data.Finset.Sigma                                      |         8128 |       750184 | x4.38
Mathlib.Data.Finset.Lattice                                    |        63068 |       742056 | x4.41
Mathlib.Data.Finset.Prod                                       |        11430 |       678987 | x4.30
Mathlib.Data.Finset.Card                                       |        17104 |       667556 | x4.36
Mathlib.Data.Finset.Image                                      |        19607 |       650452 | x4.45
Mathlib.Data.Finset.Union                                      |         8282 |       630845 | x4.52
Mathlib.Data.Finset.Basic                                      |        57940 |       622563 | x4.38
Mathlib.Data.Multiset.FinsetOps                                |         7371 |       564622 | x4.62
Mathlib.Data.Multiset.Dedup                                    |         3867 |       557251 | x4.67
Mathlib.Data.Multiset.Nodup                                    |         9031 |       553384 | x4.69
Mathlib.Data.Multiset.Range                                    |         2708 |       544352 | x4.67
Mathlib.Data.Multiset.Basic                                    |        61187 |       541643 | x4.69

Ruben Van de Velde (Jun 10 2024 at 12:51):

Mathlib.Data.List.Perm                                         |        14304 |       480456 | x4.45
Mathlib.Data.List.Dedup                                        |         3417 |       466151 | x4.49
Mathlib.Data.List.Nodup                                        |         9244 |       462733 | x4.52
Mathlib.Data.Set.Pairwise.Basic                                |        10099 |       453488 | x4.42
Mathlib.Data.Set.Function                                      |        26640 |       443389 | x4.02
Mathlib.Data.Set.Prod                                          |        23810 |       416748 | x4.21
Mathlib.Data.Set.Image                                         |        20318 |       392938 | x4.40
Mathlib.Data.Set.Subsingleton                                  |         4596 |       372620 | x4.50
Mathlib.Data.Set.Basic                                         |        44342 |       368023 | x4.55
Mathlib.Order.SymmDiff                                         |        19102 |       323680 | x4.61
Mathlib.Order.BooleanAlgebra                                   |        27774 |       304577 | x4.62
Mathlib.Order.Heyting.Basic                                    |        31978 |       276803 | x4.99
Mathlib.Order.PropInstances                                    |         2494 |       244824 | x5.51
Mathlib.Order.Disjoint                                         |        11213 |       242330 | x5.55
Aesop                                                          |         1083 |       231116 | x2.18
Aesop.Main                                                     |         3343 |       230032 | x2.18
Aesop.Search.Main                                              |        44186 |       226689 | x2.07
Aesop.Search.ExpandSafePrefix                                  |         4130 |       182503 | x1.91
Aesop.Search.Expansion                                         |        17580 |       178372 | x1.92
Aesop.Search.Expansion.Norm                                    |         9867 |       160792 | x2.03
Aesop.Search.RuleSelection                                     |         1891 |       150925 | x1.80
Aesop.Search.SearchM                                           |         3085 |       149033 | x1.81
Aesop.Search.Queue.Class                                       |         1013 |       145947 | x1.70
Aesop.Tree                                                     |          984 |       144933 | x1.70
Aesop.Tree.Check                                               |         8002 |       143949 | x1.54
Aesop.Tree.State                                               |         3391 |       135947 | x1.53
Aesop.Tree.Traversal                                           |         2174 |       132556 | x1.54
Aesop.Tree.Data                                                |         5461 |       130382 | x1.55
Aesop.Tree.UnsafeQueue                                         |         1502 |       124920 | x1.58
Aesop.Rule                                                     |         1831 |       123418 | x1.58
Aesop.Index                                                    |         6487 |       121586 | x1.59
Aesop.Rule.Basic                                               |         1190 |       115098 | x1.62
Aesop.RuleTac.Basic                                            |         1968 |       113908 | x1.62
Aesop.Index.Basic                                              |         1524 |       111939 | x1.39
Aesop.RulePattern                                              |         6485 |       110415 | x1.40
Aesop.Tracing                                                  |         3663 |       103929 | x1.41
Aesop.Util.Basic                                               |         8512 |       100266 | x1.42
Batteries.Data.String                                          |          683 |        91753 | x1.27
Batteries.Data.String.Lemmas                                   |        22974 |        91070 | x1.25
Batteries.Data.List.Lemmas                                     |        28384 |        68095 | x1.09
Batteries.Data.List.Basic                                      |        24837 |        39711 | x1.02
Batteries.Tactic.Alias                                         |         6052 |        14874 | x1.04
Batteries.CodeAction.Deprecated                                |         2602 |         8821 | x1.07
Batteries.CodeAction.Basic                                     |         4100 |         6218 | x1.00
Batteries.CodeAction.Attr                                      |         2118 |         2118 | x1.00
Lean.Server.CodeActions                                        |            0 |            0 | xNaN
Lean.Server.CodeActions.Attr                                   |            0 |            0 | xNaN
Lean.Server.CodeActions.Basic                                  |            0 |            0 | xNaN
Lean.Server.FileWorker.RequestHandling                         |            0 |            0 | xNaN
Lean.DeclarationRange                                          |            0 |            0 | xNaN
Lean.MonadEnv                                                  |            0 |            0 | xNaN
Lean.Environment                                               |            0 |            0 | xNaN
Init.Control.StateRef                                          |            0 |            0 | xNaN
Init.System.IO                                                 |            0 |            0 | xNaN
Init.Control.Reader                                            |            0 |            0 | xNaN
Init.Control.Basic                                             |            0 |            0 | xNaN
Init.Core                                                      |            0 |            0 | xNaN
Init.Prelude                                                   |            0 |            0 | xNaN

Ruben Van de Velde (Jun 10 2024 at 12:52):

There's no longer linear algebra or ring theory in the pole, and NumberTheory.Cyclotomic.Three has replaced NumberTheory.Cyclotomic.PID

Ruben Van de Velde (Jun 10 2024 at 12:53):

It would be nice if one of our topologists or analysts would take a look if anything seems implausible

Ruben Van de Velde (Jun 10 2024 at 12:55):

I looked briefly at the finiteness stuff under Filter, but that doesn't seem like an obvious dependency to get rid of

Yaël Dillies (Jun 10 2024 at 16:05):

Do we really need Analysis.Normed.Group.Basic sitting atop that much topology?

Yaël Dillies (Jun 10 2024 at 16:06):

I think there's a potential for a new Defs file here

Bolton Bailey (Jun 11 2024 at 02:39):

Yeah, file is almost 3k lines, should be split up somehow.

Ruben Van de Velde (Jun 11 2024 at 05:31):

#13713 does a bit, though it doesn't help with the pole

Ruben Van de Velde (Jun 11 2024 at 05:34):

Or does it - lemme bench

Ruben Van de Velde (Jun 11 2024 at 07:13):

It does help some - see the PR for details

Johan Commelin (Jun 11 2024 at 07:27):

What happened with that first bench? :open_mouth:

Johan Commelin (Jun 11 2024 at 07:28):

There's now also a bunch of files that get +16 extra transitive imports. It's not a lot. But I wonder if we can reasonably split the file in a way that none of the files get more imports (modulo importing newly created files)...

Ruben Van de Velde (Jun 11 2024 at 07:28):

You mean

- ~Mathlib.Analysis.Normed.Group.Lemmas   instructions   939.9%

? I added a lot of code to a file that only had two trivial results before

Johan Commelin (Jun 11 2024 at 07:28):

Aaah, fair enough (-;

Johan Commelin (Jun 11 2024 at 07:29):

I didn't realise it was that small before.

Ruben Van de Velde (Jun 11 2024 at 07:29):

We could create another file between Basic and Lemmas, but then I'd like suggestions for a name :)

Ruben Van de Velde (Jun 11 2024 at 07:31):

#13702 is also up for review

Johan Commelin (Jun 11 2024 at 07:33):

Can we have {Defs,Basic,Lemmas}?

Johan Commelin (Jun 11 2024 at 07:34):

Otoh, maybe these +16 imports aren't what we should be focussing on

Ruben Van de Velde (Jun 11 2024 at 09:04):

If you think it's useful, I can do that

Yaël Dillies (Jun 11 2024 at 09:40):

I would like to have a look for myself first

Ruben Van de Velde (Jun 11 2024 at 20:46):

#13738 also up for review

Ruben Van de Velde (Jun 12 2024 at 12:05):

If somebody wants to review a wholly implausible performance win: #13756

Johan Commelin (Jun 12 2024 at 13:30):

Very nice :merge:

Ruben Van de Velde (Jun 13 2024 at 07:37):

A review on #13738 would be appreciated

Yaël Dillies (Jun 13 2024 at 07:46):

Sorry, short on time today

Riccardo Brasca (Jun 13 2024 at 07:50):

Having a look

Riccardo Brasca (Jun 13 2024 at 07:55):

LGTM

Ruben Van de Velde (Jun 13 2024 at 08:31):

Riccardo Brasca said:

LGTM

Did you mean to put that on github? :)

Riccardo Brasca (Jun 13 2024 at 08:34):

Ahahah, yes sorry, I just had a look :P

Ruben Van de Velde (Jun 15 2024 at 17:57):

@Yaël Dillies are you planning to look at #13713?

Yaël Dillies (Jun 19 2024 at 23:37):

Johan Commelin said:

There's now also a bunch of files that get +16 extra transitive imports. It's not a lot. But I wonder if we can reasonably split the file in a way that none of the files get more imports (modulo importing newly created files)...

Update on that: We did mostly manage. Now only

Analysis.Normed.Group.Hom
Analysis.Normed.Order.Lattice
Analysis.Normed.Group.AddTorsor
Analysis.NormedSpace.LinearIsometry

get 17 new imports

Kim Morrison (Jun 20 2024 at 01:21):

Could you say why they get more imports?

Yaël Dillies (Jun 20 2024 at 07:53):

That's because we are moving some lemmas from Analysis.Normed.Group.Basic to Analysis.Normed.Group.Lemmas and those files need those lemmas, but also Analysis.Normed.Group.Lemmas has 17 more imports than Analysis.Normed.Group.Basic

Yaël Dillies (Jun 20 2024 at 07:53):

If you look at the PR, you will see that the balance of imports is a net positive

Ruben Van de Velde (Jun 20 2024 at 19:02):

Can I have a review on #13945?

Ruben Van de Velde (Jun 20 2024 at 23:23):

Yaël Dillies said:

If you look at the PR, you will see that the balance of imports is a net positive

Updated results for the pole in #13713

Ruben Van de Velde (Jun 22 2024 at 21:06):

A simpler change is up for review at #14035

Ruben Van de Velde (Jun 24 2024 at 19:57):

Anyone up for a review in #13684?

Anne Baanen (Oct 15 2024 at 11:36):

Here's a fresh lake exe pole output:

Analyzing Mathlib at 5d2ccbb3e5b5df402d3b88f4c9aa0cd2ac986130
| file                                                           | instructions | cumulative | parallelism |
| :------------------------------------------------------------- | -----------: | ---------: | :---------: |
| Mathlib                                                        |        10653 |    6304159 |    20.06    |
| Mathlib.NumberTheory.FLT.Three                                 |       131894 |    6293506 |    8.56     |
| Mathlib.NumberTheory.Cyclotomic.Three                          |        45005 |    6161612 |    8.68     |
| Mathlib.NumberTheory.Cyclotomic.Rat                            |       116140 |    6116607 |    8.69     |
| Mathlib.NumberTheory.Cyclotomic.Discriminant                   |        41496 |    6000466 |    8.83     |
| Mathlib.NumberTheory.NumberField.Discriminant                  |       195560 |    5958970 |    8.70     |
| Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody |       162278 |    5763409 |    8.94     |
| Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls           |        69465 |    5601130 |    7.35     |
| Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup           |        36321 |    5531664 |    7.41     |
| Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral    |        41059 |    5495343 |    7.45     |
| Mathlib.Analysis.SpecialFunctions.Gamma.Basic                  |        41404 |    5454283 |    7.49     |
| Mathlib.Analysis.MellinTransform                               |        36644 |    5412878 |    7.54     |
| Mathlib.Analysis.SpecialFunctions.ImproperIntegrals            |        15705 |    5376233 |    7.57     |
| Mathlib.Analysis.SpecialFunctions.JapaneseBracket              |        15588 |    5360528 |    7.35     |
| Mathlib.Analysis.SpecialFunctions.Integrals                    |        85209 |    5344939 |    7.33     |
| Mathlib.Analysis.SpecialFunctions.Pow.Deriv                    |       150728 |    5259730 |    6.24     |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv          |       138271 |    5109002 |    6.21     |
| Mathlib.Analysis.SpecialFunctions.ExpDeriv                     |        39944 |    4970730 |    6.31     |
| Mathlib.Analysis.Complex.RealDeriv                             |        39822 |    4930786 |    6.18     |
| Mathlib.Analysis.Calculus.ContDiff.Basic                       |       363213 |    4890964 |    5.09     |
| Mathlib.Analysis.Calculus.FDeriv.Mul                           |       429447 |    4527751 |    5.40     |
| Mathlib.Analysis.Calculus.FDeriv.Analytic                      |       248575 |    4098303 |    5.85     |
| Mathlib.Analysis.Analytic.CPolynomial                          |       132075 |    3849728 |    5.84     |
| Mathlib.Analysis.Analytic.Constructions                        |       116780 |    3717653 |    5.99     |
| Mathlib.Analysis.Analytic.Composition                          |       156874 |    3600873 |    6.10     |
| Mathlib.Analysis.Analytic.Basic                                |       238838 |    3443998 |    6.33     |
| Mathlib.Analysis.Calculus.FormalMultilinearSeries              |        75233 |    3205159 |    6.19     |
| Mathlib.Analysis.NormedSpace.Multilinear.Curry                 |       207707 |    3129926 |    6.32     |
| Mathlib.Analysis.NormedSpace.Multilinear.Basic                 |       277144 |    2922218 |    6.69     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace          |        57737 |    2645074 |    7.18     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear             |       164037 |    2587336 |    7.30     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.Basic                |        81703 |    2423298 |    7.73     |
| Mathlib.Topology.Algebra.Module.StrongTopology                 |        99415 |    2341595 |    7.60     |
| Mathlib.Topology.Algebra.Module.UniformConvergence             |        12545 |    2242180 |    7.89     |
| Mathlib.Analysis.LocallyConvex.Bounded                         |        40910 |    2229635 |    7.91     |
| Mathlib.Analysis.Seminorm                                      |       144829 |    2188724 |    8.03     |
| Mathlib.Analysis.LocallyConvex.Basic                           |        29324 |    2043895 |    8.48     |
| Mathlib.Analysis.Normed.Module.Basic                           |        43638 |    2014571 |    8.32     |
| Mathlib.Analysis.Normed.Field.Lemmas                           |        24235 |    1970932 |    8.47     |
| Mathlib.Analysis.Normed.Group.Uniform                          |        29796 |    1946697 |    7.87     |
| Mathlib.Topology.MetricSpace.Algebra                           |        12077 |    1916900 |    7.86     |
| Mathlib.Topology.Algebra.SeparationQuotient                    |        34064 |    1904823 |    6.97     |
| Mathlib.Topology.Algebra.Module.Basic                          |       229518 |    1870758 |    6.26     |
| Mathlib.Topology.Algebra.UniformGroup                          |        69007 |    1641240 |    5.80     |
| Mathlib.Topology.Algebra.Group.Basic                           |        93875 |    1572233 |    5.90     |
| Mathlib.Topology.Algebra.Monoid                                |        38398 |    1478357 |    4.90     |
| Mathlib.Topology.Algebra.MulAction                             |        10926 |    1439958 |    4.52     |
| Mathlib.Topology.Algebra.ConstMulAction                        |        31674 |    1429032 |    4.53     |
| Mathlib.Topology.Algebra.Constructions                         |         5547 |    1397357 |    4.18     |
| Mathlib.Topology.Homeomorph                                    |        26162 |    1391809 |    4.19     |
| Mathlib.Topology.Support                                       |        12092 |    1365647 |    4.24     |
| Mathlib.Topology.Separation                                    |        57223 |    1353554 |    3.96     |
| Mathlib.Topology.GDelta                                        |         6854 |    1296331 |    3.98     |
| Mathlib.Topology.UniformSpace.Basic                            |        48776 |    1289476 |    3.99     |
| Mathlib.Topology.Compactness.Compact                           |        30063 |    1240700 |    4.11     |
| Mathlib.Topology.Bases                                         |        33925 |    1210636 |    4.17     |
| Mathlib.Topology.ContinuousOn                                  |        32503 |    1176711 |    4.26     |
| Mathlib.Topology.Constructions                                 |        42381 |    1144207 |    4.31     |
| Mathlib.Topology.Maps.Basic                                    |        12699 |    1101826 |    4.42     |
| Mathlib.Topology.Order                                         |        19605 |    1089126 |    4.46     |
| Mathlib.Topology.Defs.Induced                                  |         3095 |    1069521 |    4.53     |
| Mathlib.Topology.Basic                                         |        36216 |    1066426 |    4.54     |
| Mathlib.Topology.Defs.Filter                                   |         8220 |    1030209 |    4.64     |
| Mathlib.Order.Filter.Ultrafilter                               |        13418 |    1021988 |    4.52     |
| Mathlib.Order.Filter.Cofinite                                  |         6512 |    1008569 |    4.27     |
| Mathlib.Order.Filter.AtTopBot                                  |        44663 |    1002057 |    4.28     |
| Mathlib.Order.Filter.Bases                                     |        24351 |     957394 |    4.34     |
| Mathlib.Order.Filter.Basic                                     |        62846 |     933042 |    4.29     |
| Mathlib.Data.Set.Finite                                        |        38689 |     870196 |    4.52     |
| Mathlib.Data.Finite.Basic                                      |         3150 |     831507 |    4.65     |
| Mathlib.Data.Fintype.Sigma                                     |        16601 |     828357 |    4.41     |
| Mathlib.Data.Finset.Sigma                                      |         8608 |     811755 |    4.40     |
| Mathlib.Data.Finset.Lattice                                    |        49195 |     803147 |    4.40     |
| Mathlib.Data.Finset.Prod                                       |        12306 |     753952 |    4.11     |
| Mathlib.Data.Finset.Card                                       |        21205 |     741646 |    4.16     |
| Mathlib.Data.Finset.Image                                      |        20377 |     720440 |    4.26     |
| Mathlib.Data.Finset.Union                                      |         8323 |     700063 |    4.30     |
| Mathlib.Data.Finset.Basic                                      |        66069 |     691739 |    4.10     |
| Mathlib.Data.Multiset.FinsetOps                                |         7816 |     625669 |    4.30     |
| Mathlib.Data.Multiset.Dedup                                    |         4448 |     617853 |    4.34     |
| Mathlib.Data.Multiset.Nodup                                    |         9101 |     613404 |    4.36     |
| Mathlib.Data.Multiset.Range                                    |         2596 |     604303 |    4.41     |
| Mathlib.Data.Multiset.Basic                                    |        68439 |     601706 |    4.42     |
| Mathlib.Data.List.Perm                                         |        16018 |     533266 |    4.03     |
| Mathlib.Data.List.Dedup                                        |         4275 |     517247 |    4.07     |
| Mathlib.Data.List.Nodup                                        |        10294 |     512972 |    4.08     |
| Mathlib.Data.Set.Pairwise.Basic                                |        11786 |     502678 |    3.98     |
| Mathlib.Data.Set.Function                                      |        38520 |     490891 |    3.54     |

Anne Baanen (Oct 15 2024 at 11:36):

| Mathlib.Data.Set.Prod                                          |        29331 |     452371 |    3.75     |
| Mathlib.Data.Set.Image                                         |        28142 |     423039 |    3.94     |
| Mathlib.Data.Set.Subsingleton                                  |         6620 |     394896 |    4.13     |
| Mathlib.Data.Set.Basic                                         |        55091 |     388276 |    4.18     |
| Mathlib.Order.SymmDiff                                         |        22311 |     333185 |    4.21     |
| Mathlib.Order.BooleanAlgebra                                   |        30818 |     310873 |    3.73     |
| Mathlib.Order.Heyting.Basic                                    |        35904 |     280055 |    4.03     |
| Mathlib.Order.PropInstances                                    |         2894 |     244150 |    4.48     |
| Mathlib.Order.Disjoint                                         |        14673 |     241255 |    4.52     |
| Mathlib.Order.BoundedOrder                                     |        11841 |     226582 |    2.83     |
| Mathlib.Order.Lattice                                          |        23180 |     214741 |    2.93     |
| Mathlib.Order.Monotone.Basic                                   |        18670 |     191561 |    3.15     |
| Mathlib.Order.RelClasses                                       |        12526 |     172890 |    2.46     |
| Mathlib.Order.Basic                                            |        22511 |     160363 |    1.96     |
| Mathlib.Tactic.Convert                                         |         5214 |     137852 |    1.91     |
| Mathlib.Tactic.CongrExclamation                                |        17858 |     132638 |    1.94     |
| Mathlib.Lean.Meta.CongrTheorems                                |        10616 |     114779 |    2.09     |
| Mathlib.Logic.IsEmpty                                          |         2886 |     104163 |    2.20     |
| Mathlib.Logic.Function.Basic                                   |        12937 |     101276 |    2.24     |
| Mathlib.Logic.Nonempty                                         |         2399 |      88338 |    1.68     |
| Mathlib.Algebra.Group.ZeroOne                                  |          996 |      85939 |    1.60     |
| Mathlib.Tactic.ToAdditive                                      |          935 |      84943 |    1.61     |
| Mathlib.Tactic.ToAdditive.Frontend                             |        33297 |      84008 |    1.62     |
| Mathlib.Tactic.Simps.Basic                                     |        32825 |      50710 |    1.34     |
| Mathlib.Lean.Expr.Basic                                        |         9002 |      17885 |    1.83     |
| Mathlib.Init                                                   |          643 |       8883 |    2.67     |
| Mathlib.Tactic.Linter.Lint                                     |         8239 |       8239 |    1.00     |
| Batteries.Tactic.Lint                                          |            0 |          0 |     NaN     |
| Batteries.Tactic.Lint.Misc                                     |            0 |          0 |     NaN     |
| Lean.Util.CollectLevelParams                                   |            0 |          0 |     NaN     |
| Lean.Expr                                                      |            0 |          0 |     NaN     |
| Init.Data.Hashable                                             |            0 |          0 |     NaN     |
| Init.Data.UInt.Basic                                           |            0 |          0 |     NaN     |
| Init.Data.Fin.Basic                                            |            0 |          0 |     NaN     |
| Init.Data.Nat.Bitwise.Basic                                    |            0 |          0 |     NaN     |
| Init.Data.Nat.Basic                                            |            0 |          0 |     NaN     |
| Init.SimpLemmas                                                |            0 |          0 |     NaN     |
| Init.Core                                                      |            0 |          0 |     NaN     |
| Init.Prelude                                                   |            0 |          0 |     NaN     |

Anne Baanen (Oct 15 2024 at 11:37):

It would be nice if we could have a bot post this output regularly (every week, together with the tech debt counters?). Does anyone want to take that task onto them?

Ruben Van de Velde (Oct 15 2024 at 15:35):

Unfortunately something seems to have broken since you posted that

Ruben Van de Velde (Oct 15 2024 at 15:36):

   "#############\n## General ##\n#############\nRunner name:      pheidippides\nHash:             e38935a1cc4b76330d195a46ef5fe7ff05656be6\nSystem:           Linux amd64 6.1.65\nCPU:              AMD Ryzen 9 7950X3D 16-Core Processor (32 threads)\nMemory:           127963 MiB total, 124918 MiB available\nJava version:     19.0.2 by N/A\nUser:             velcom-runner\nBench repo hash:  112ef83dfa774977d7b54143c391f8b859feca91\nExecuted command: [\"/var/lib/velcom-runner/mathlib4/bench_repo/bench\", \"/var/lib/velcom-runner/mathlib4/task_repo\"]\nStart time:       2024-10-15T11:23:05.071617639Z\nStop time:        2024-10-15T11:44:33.531999554Z\nExecution time:   PT21M28.460230593S\nExit code:        1\n\n############\n## Stdout ##\n############\n<empty>\n\n############\n## Stderr ##\n############\n+ temci exec --config ./scripts/bench/temci-config.yml\n[2024-10-15 11:44:24,253] Program block no. 0 failed: Unexpected return code 1, expected 0\n[2024-10-15 11:44:24,253] error\n\ninfo: downloading component 'lean'\ninfo: installing component 'lean'\ninfo: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'\ninfo: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'\ninfo: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'\ninfo: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'\ninfo: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'\ninfo: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'\ninfo: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'\n✔ [7/25] Built ProofWidgets.Compat\n✔ [8/25] Built ProofWidgets.Util\n✔ [9/25] Built ProofWidgets.Component.Basic\n✔ [10/25] Built ProofWidgets.Cancellable\n✔ [11/25] Built ProofWidgets.Component.MakeEditLink\n✔ [12/25] Built ProofWidgets.Component.Panel.Basic\n✔ [13/25] Built ProofWidgets.Component.Recharts\n✔ [14/25] Built ProofWidgets.Component.Panel.GoalTypePanel\n✔ [15/25] Built ProofWidgets.Data.Html\n✔ [16/25] Built ProofWidgets.Component.FilterDetails\n✔ [17/25] Built ProofWidgets.Component.HtmlDisplay\n✔ [18/25] Built ProofWidgets.Component.OfRpcMethod\n✔ [19/25] Built ProofWidgets.Presentation.Expr\n✔ [20/25] Built ProofWidgets.Component.PenroseDiagram\n✔ [21/25] Built ProofWidgets.Data.Svg\n✔ [22/25] Built ProofWidgets.Component.Panel.SelectionPanel\n✔ [23/25] Built ProofWidgets.Component.InteractiveSvg\n✔ [24/25] Built ProofWidgets\nBuild completed successfully.\nrm: cannot remove '.lake/packages/batteries/.lake/build/bin/runLinter': No such file or directory\n\n Performance counter stats for '/tmp/tmpvunhcdgb':\n\n         10,930.62 msec task-clock                #    0.806 CPUs utilized          \n    90,466,645,925      instructions:u                                              \n    20,736,879,885      branches                  #    1.897 G/sec                  \n       410,646,181      branch-misses             #    1.98% of all branches        \n\n      13.567094094 seconds time elapsed\n\n       8.516014000 seconds user\n       2.502838000 seconds sys\n\n\n\nCommand exited with non-zero status 1\n29163.95user 1303.43system 21:28.32elapsed 2364%CPU (0avgtext+0avgdata 10211060maxresident)k\n0inputs+12088992outputs (39102major+309256754minor)pagefaults 0swaps\n\n############\n## Reason ##\n############\nThe benchmark script terminated with a non-zero exit code (1)!\n"},

Ruben Van de Velde (Oct 15 2024 at 15:36):

rm: cannot remove '.lake/packages/batteries/.lake/build/bin/runLinter': No such file or directory

Kevin Buzzard (Oct 15 2024 at 16:40):

It would certainly be possible to remove Mathlib.NumberTheory.FLT.Three and Mathlib.NumberTheory.Cyclotomic.Three from the top of that pile, but I'm assuming that there would be little point in doing this; the general cyclotomic theory (the next couple of files down) will need inputs from analysis/topology etc. This is one reason why FLT is a good stress test for the system -- number theory has a habit of borrowing from many other areas and turning them into completely pointless facts like xn+ynznx^n+y^n\not=z^n which have no uses at all :-)

Kim Morrison (Oct 15 2024 at 23:46):

I think it's generally best not to trying cutting off the top end of the pole, but instead to attack the middle, where there is both plenty of low-hanging fruit, and the much wider impact.

Kim Morrison (Oct 16 2024 at 01:37):

Ruben Van de Velde said:

Unfortunately something seems to have broken since you posted that

Fixed.

Yaël Dillies (Oct 16 2024 at 08:16):

Actually, nothing in the middle seems out of place to me

Kim Morrison (Oct 16 2024 at 10:29):

I'm sure there is still lots that can be reduced here. e.g. in the Finset/Multiset/Fintype/Finite stuff.

Kim Morrison (Oct 16 2024 at 10:30):

Surely GDelta isn't needed for Topology.Algebra.Monoid?

Kim Morrison (Oct 16 2024 at 10:31):

Until there are no grey nodes in lake exe graph --from X --to Y for every pair X and Y on the longest pole, I'm skeptical there isn't more to do. :-)

Yaël Dillies (Oct 16 2024 at 10:31):

Kim Morrison said:

I'm sure there is still lots that can be reduced here. e.g. in the Finset/Multiset/Fintype/Finite stuff.

I've looked at that part extensively, and there is really not much more to be done unless we literally abandon the typeclass-based algebraic order lemmas in favor of a large duplication for the special cases of Nat, Int, Multiset α

Kim Morrison (Oct 16 2024 at 10:32):

Even just today I reduced imports in this section, see #17796

Yaël Dillies (Oct 16 2024 at 10:34):

Yes so pushing this approach would result in an exponential number of files in the number of concepts, as @Eric Wieser has been fearing for a while

Yaël Dillies (Oct 16 2024 at 10:34):

At some point, we do have to linearise part of the import tree a bit

Kim Morrison (Oct 16 2024 at 10:41):

e.g.
o.pdf

for GDelta / Algebra.Monoid, which I picked more or less at random.

Yaël Dillies (Oct 16 2024 at 10:42):

Topology.Homeomorph (and similar files, like Logic.Equiv.TransferInstance) do accumulate imports because they aim to transfer all properties ever across some kind of isomorphism

Kim Morrison (Oct 16 2024 at 10:47):

I agree that files like that shouldn't be atomised into files for every different property. But it would be reasonable to stratify those properties into layers and handle those layers in separate files if that helps reduce imports.

Eric Wieser (Oct 16 2024 at 10:48):

It's not clear to me that such stratification would appease your "no gray nodes" metric, which is a criticism of the metric not the stratification

Kim Morrison (Oct 23 2024 at 23:54):

Preview of a tool that identifies all the "grey nodes" for a given set of modules, run on the latest longest pole.

i.e. given a list of modules, it makes a table with rows and columns indexed by that list, and the (A, B) cell has an x in it if A transitively imports B but does not use any declarations from it.

Kim Morrison (Oct 23 2024 at 23:57):

It quickly reveals lots of interesting patterns, e.g. that Mathlib.NumberTheory.Cyclotomic.Rat and Mathlib.NumberTheory.Cyclotomic.Discriminant do not actually use anything from from rows 7 (Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody) through 36 (Mathlib.Analysis.LocallyConvex.Basic) of the longest pole!

Kim Morrison (Oct 23 2024 at 23:58):

Any suggestions for displaying this data more conveniently very much appreciated.

Kim Morrison (Oct 23 2024 at 23:58):

I feel like having a tool that reports maximal rectangles in this grid might be helpful.

Kim Morrison (Oct 24 2024 at 00:00):

e.g. rows 70,71,72 (Mathlib.Data.Finset/Finite/Fintype.Sigma) are not used by rows 29-68, excepting row 55

Kim Morrison (Oct 24 2024 at 05:16):

Nicely packaged up in #18156.

Kim Morrison (Oct 24 2024 at 05:16):

It now outputs, as well as the markdown table, a list of lake exe graph commands that exhibit the largest rectangles of xs appearing in the table.

Kim Morrison (Oct 24 2024 at 05:38):

#18157 is a modification to lake exe pole:

Enables lake exe pole --loc which uses lines of code as a quick proxy for the instruction count.

This allows running lake exe pole on commits that have not been through the speed center, or in cases where it's convenient to avoid the speed center.

Johan Commelin (Oct 24 2024 at 05:45):

Kim Morrison said:

It now outputs, as well as the markdown table, a list of lake exe graph commands that exhibit the largest rectangles of xs appearing in the table.

How well does this scale? Can we run this on all 5000ish files in mathlib?

Kim Morrison (Oct 24 2024 at 05:51):

This runs successfully on any linear sequence of imports, taking ~10s or so. (e.g. the long pole is about 100 files)

Kim Morrison (Oct 24 2024 at 05:52):

I haven't tried it on bigger graphs yet, but I would guess that it would run in about ~10 minutes?

Kim Morrison (Oct 24 2024 at 05:52):

However "rectangle" no longer means anything sensible!

Kim Morrison (Oct 24 2024 at 05:53):

I guess we could have it look for generalized rectangles (i.e. some subset times some other subset), but that's more expensive, and still less clear what it means.

Kim Morrison (Oct 24 2024 at 05:53):

But just producing the table itself seems viable. What one does with a 5000x5000 table is unclear. :-)

Johan Commelin (Oct 24 2024 at 05:55):

You mentioned looking at connected components in the complement of the graph, the other day...

Kim Morrison (Oct 24 2024 at 05:56):

But remember it is actually 5000 complements in 5000 different graphs.

Johan Commelin (Oct 24 2024 at 06:33):

Yup, true. So we need a bit more tooling for that maybe...

Yaël Dillies (Oct 24 2024 at 06:34):

FYI I am working on reducing the number of files importing LinearAlgebra.Span. Bhavik and I already spotted quite a few bogus imports around there

Michael Rothgang (Oct 24 2024 at 09:22):

Kim Morrison said:

#18157 is a modification to lake exe pole:

Enables lake exe pole --loc which uses lines of code as a quick proxy for the instruction count.

This allows running lake exe pole on commits that have not been through the speed center, or in cases where it's convenient to avoid the speed center.

Implementation looks good to me. I can also imagine this is useful (but will leave the final on that to others).

Kim Morrison (Oct 24 2024 at 13:13):

#18168 splits NumberField.Discriminant into the "doesn't need analysis / needs analysis" parts, and thereby knocks FLT.Three off the longest pole.

Kim Morrison (Oct 24 2024 at 13:15):

I actually made that PR "live", in a little video I made (mostly because I wanted to learn how to use Da Vinci :-) demoing the new lake exe unused tool. Youtube URL available shortly. :-)

Kim Morrison (Oct 24 2024 at 13:24):

https://youtu.be/PVj_FHGwhUI (still processing right now, but I'm off)

Riccardo Brasca (Oct 25 2024 at 07:53):

Oh nice, I was opening the PR watching the video and literally 5 seconds later in the video you said "let's do it" :D

Edward van de Meent (Oct 25 2024 at 08:33):

love the video, it gives a clear explanation on how to do this!

Johan Commelin (Oct 25 2024 at 08:36):

If you like this, and you speak meta, please review #18156

Ruben Van de Velde (Oct 25 2024 at 10:05):

Analyzing Mathlib at d85e7dbb201ed04d86c1f27e373dc6f5fc637092

file instructions cumulative parallelism
Mathlib 10868 6195855 21.23
Mathlib.Analysis.CStarAlgebra.Module.Constructions 75856 6184986 7.55
Mathlib.Analysis.CStarAlgebra.Module.Defs 60114 6109130 7.63
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 178878 6049015 7.69
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 317549 5870136 7.86
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique 209150 5552587 8.08
Mathlib.Analysis.Normed.Algebra.Spectrum 137305 5343436 8.19
Mathlib.Analysis.Complex.Polynomial.Basic 28687 5206131 8.30
Mathlib.Analysis.Complex.Liouville 16965 5177444 7.83
Mathlib.Analysis.Complex.CauchyIntegral 49866 5160478 7.85
Mathlib.MeasureTheory.Integral.CircleIntegral 69319 5110611 7.75
Mathlib.Analysis.SpecialFunctions.NonIntegrable 14840 5041292 7.84
Mathlib.Analysis.SpecialFunctions.Log.Deriv 46656 5026451 6.43
Mathlib.Analysis.SpecialFunctions.ExpDeriv 40472 4979795 6.46
Mathlib.Analysis.Complex.RealDeriv 40262 4939322 6.33
Mathlib.Analysis.Calculus.ContDiff.Basic 369105 4899060 5.10
Mathlib.Analysis.Calculus.FDeriv.Mul 392259 4529954 5.42
Mathlib.Analysis.Calculus.FDeriv.Analytic 251478 4137694 5.83
Mathlib.Analysis.Analytic.CPolynomial 132705 3886216 5.83
Mathlib.Analysis.Analytic.Constructions 118229 3753510 5.97
Mathlib.Analysis.Analytic.Composition 157948 3635280 6.08
Mathlib.Analysis.Analytic.Basic 238443 3477331 6.30
Mathlib.Analysis.Calculus.FormalMultilinearSeries 75987 3238888 6.30
Mathlib.Analysis.NormedSpace.Multilinear.Curry 210383 3162900 6.42
Mathlib.Analysis.NormedSpace.Multilinear.Basic 279151 2952517 6.81
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 57467 2673366 7.31
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 165293 2615898 7.43
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 82221 2450604 7.86
Mathlib.Topology.Algebra.Module.StrongTopology 100284 2368383 7.73
Mathlib.Topology.Algebra.Module.UniformConvergence 12566 2268099 8.02
Mathlib.Analysis.LocallyConvex.Bounded 41465 2255532 8.04
Mathlib.Analysis.Seminorm 146539 2214067 7.75
Mathlib.Analysis.LocallyConvex.Basic 31327 2067527 8.19
Mathlib.Analysis.Normed.Module.Basic 43647 2036200 7.89
Mathlib.Analysis.Normed.Field.Lemmas 26259 1992553 8.02
Mathlib.Analysis.Normed.Group.Uniform 30216 1966294 7.21
Mathlib.Topology.MetricSpace.Algebra 12020 1936077 7.18
Mathlib.Topology.Algebra.SeparationQuotient.Basic 28874 1924057 6.31
Mathlib.Topology.Algebra.Module.Basic 230735 1895182 6.40
Mathlib.Topology.Algebra.UniformGroup 69827 1664447 5.91
Mathlib.Topology.Algebra.Group.Quotient 8184 1594619 5.98
Mathlib.Topology.Algebra.Group.Basic 89540 1586435 5.78
Mathlib.Topology.Algebra.Monoid 38219 1496894 4.82
Mathlib.Topology.Algebra.MulAction 11173 1458674 4.58
Mathlib.Topology.Algebra.ConstMulAction 32321 1447500 4.59
Mathlib.Topology.Algebra.Constructions 5649 1415179 4.22
Mathlib.Topology.Homeomorph 27995 1409530 4.23
Mathlib.Topology.Support 12586 1381534 4.29
Mathlib.Topology.Separation.Basic 57827 1368948 4.02
Mathlib.Topology.Compactness.Lindelof 17303 1311120 4.06
Mathlib.Topology.Compactness.SigmaCompact 9690 1293816 4.09
Mathlib.Topology.Compactness.LocallyCompact 6240 1284126 4.11
Mathlib.Topology.Compactness.Compact 30420 1277886 4.13
Mathlib.Topology.Bases 35209 1247466 4.19
Mathlib.Topology.ContinuousOn 34296 1212256 4.28
Mathlib.Topology.Constructions 45451 1177960 4.33
Mathlib.Topology.Maps.Basic 13986 1132508 4.45
Mathlib.Topology.Order 20606 1118521 4.49
Mathlib.Topology.Defs.Induced 3231 1097914 4.56
Mathlib.Topology.Basic 38124 1094682 4.57
Mathlib.Topology.Defs.Filter 8044 1056558 4.68
Mathlib.Order.Filter.Ultrafilter 13413 1048513 4.57
Mathlib.Order.Filter.Cofinite 6608 1035100 4.31
Mathlib.Order.Filter.AtTopBot 43899 1028491 4.31
Mathlib.Order.Filter.Bases 25140 984592 4.34
Mathlib.Order.Filter.Basic 57853 959451 4.29
Mathlib.Data.Set.Finite 40827 901598 4.49
Mathlib.Data.Finite.Sigma 2253 860770 4.42
Mathlib.Data.Fintype.Sigma 16732 858517 4.37
Mathlib.Data.Finset.Sigma 8937 841784 4.35
Mathlib.Data.Finset.Lattice 50946 832847 4.36
Mathlib.Data.Finset.Prod 12860 781900 4.06
Mathlib.Data.Finset.Card 23402 769039 4.11
Mathlib.Data.Finset.Image 21312 745637 4.21
Mathlib.Data.Finset.Union 8646 724325 4.25
Mathlib.Data.Finset.Basic 72072 715678 4.00
Mathlib.Data.Multiset.FinsetOps 8101 643606 4.22
Mathlib.Data.Multiset.Dedup 4583 635504 4.25
Mathlib.Data.Multiset.Nodup 9363 630921 4.27
Mathlib.Data.Multiset.Range 2670 621557 4.31
Mathlib.Data.Multiset.Basic 73315 618887 4.33

Ruben Van de Velde (Oct 25 2024 at 10:05):

file instructions cumulative parallelism
Mathlib.Data.List.Perm.Lattice 3691 545572 3.95
Mathlib.Data.List.Nodup 10998 541880 3.96
Mathlib.Data.Set.Pairwise.Basic 13196 530882 3.86
Mathlib.Data.Set.Function 42527 517685 3.43
Mathlib.Data.Set.Prod 30921 475158 3.64
Mathlib.Data.Set.Image 30312 444237 3.83
Mathlib.Data.Set.Subsingleton 6930 413924 4.01
Mathlib.Data.Set.Basic 58243 406994 4.06
Mathlib.Order.SymmDiff 23612 348750 4.08
Mathlib.Order.BooleanAlgebra 32484 325137 3.61
Mathlib.Order.Heyting.Basic 37694 292653 3.90
Mathlib.Order.PropInstances 3009 254959 4.33
Mathlib.Order.Disjoint 15507 251949 4.37
Mathlib.Order.BoundedOrder 12789 236441 2.75
Mathlib.Order.Lattice 24778 223652 2.85
Mathlib.Order.Monotone.Basic 19867 198874 3.07
Mathlib.Order.RelClasses 13166 179006 2.38
Mathlib.Order.Basic 24632 165840 1.88
Mathlib.Tactic.Convert 5323 141207 1.81
Mathlib.Tactic.CongrExclamation 18186 135883 1.85
Mathlib.Lean.Meta.CongrTheorems 10776 117697 1.98
Mathlib.Logic.IsEmpty 3010 106920 2.08
Mathlib.Logic.Function.Basic 14217 103909 2.11
Mathlib.Logic.Nonempty 2458 89692 1.51
Mathlib.Algebra.Group.ZeroOne 1001 87234 1.42
Mathlib.Tactic.ToAdditive 938 86232 1.43
Mathlib.Tactic.ToAdditive.Frontend 34249 85293 1.43
Mathlib.Tactic.Simps.Basic 33407 51044 1.49
Mathlib.Lean.Expr.Basic 8893 17636 2.25
Mathlib.Init 653 8743 3.53
Mathlib.Tactic.Linter.Lint 7197 8089 1.00
Mathlib.Tactic.DeclarationNames 891 891 1.00
Lean.DeclarationRange 0 0 NaN
Lean.MonadEnv 0 0 NaN
Lean.Environment 0 0 NaN
Init.Control.StateRef 0 0 NaN
Init.System.IO 0 0 NaN
Init.Control.Reader 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Kim Morrison (Oct 25 2024 at 10:54):

Oh, nice, I'm pleased to see C* algebras as the longest pole again. I miss having an excuse to look at them. :-)

Kim Morrison (Oct 25 2024 at 10:56):

#18156 doesn't actually have much meta code. The actual analysis lives in import-graph, where I sneakily merged my own PR. #18156 is mostly just "scripting" to present the data, and a little algorithm for finding large rectangles in subsets of ℕ × ℕ.

Kim Morrison (Oct 25 2024 at 10:57):

I was really pleased that everything for this tool (metaprogramming, data analysis, markdown presentation) could be done in Lean. It's (getting closer to) a new world.

Michael Rothgang (Oct 25 2024 at 14:44):

As I said on the PR: feel free to split out the drive-by clean-ups; I'd approve them right away.

Kim Morrison (Oct 28 2024 at 06:11):

Thanks @Edward van de Meent and @Michael Rothgang for the reviews.

Hopefully we can get this in soon? I'd like to iterate on it a bit further (aiming to run something like it on all of Mathlib, rather than just a long pole to some target), but would prefer to ship this first bit so it's usable on master already.

Edward van de Meent (Oct 28 2024 at 12:18):

so i just ran lake exe pole --loc, and got this as output...
anyone have an idea what went wrong?

| file                                   | LoC | cumulative | parallelism |
| :------------------------------------- | --: | ---------: | :---------: |
| Mathlib                                |   0 |          0 |     NaN     |
| Batteries                              |   0 |          0 |     NaN     |
| Batteries.Classes.Cast                 |   0 |          0 |     NaN     |
| Batteries.Util.LibraryNote             |   0 |          0 |     NaN     |
| Lean.Elab.Command                      |   0 |          0 |     NaN     |
| Lean.Meta.Diagnostics                  |   0 |          0 |     NaN     |
| Lean.PrettyPrinter                     |   0 |          0 |     NaN     |
| Lean.PrettyPrinter.Delaborator         |   0 |          0 |     NaN     |
| Lean.PrettyPrinter.Delaborator.Options |   0 |          0 |     NaN     |
| Lean.Data.Options                      |   0 |          0 |     NaN     |
| Lean.ImportingFlag                     |   0 |          0 |     NaN     |
| Init.System.IO                         |   0 |          0 |     NaN     |
| Init.Control.Reader                    |   0 |          0 |     NaN     |
| Init.Control.Basic                     |   0 |          0 |     NaN     |
| Init.Core                              |   0 |          0 |     NaN     |
| Init.Prelude                           |   0 |          0 |     NaN     |

Edward van de Meent (Oct 28 2024 at 12:18):

unless there truly are 0 LoC in mathlib :upside_down:

Damiano Testa (Oct 28 2024 at 12:39):

I am not sure why you get that output, this is what I see:

Analyzing Mathlib at 4e6a34eff012d737c3445f3983af80d55ef94dac

file LoC cumulative parallelism
Mathlib 5043 104569 14.93
Mathlib.NumberTheory.LSeries.DirichletContinuation 301 99526 8.22
Mathlib.NumberTheory.LSeries.ZMod 527 99225 8.23
Mathlib.NumberTheory.LSeries.RiemannZeta 243 98698 7.70
Mathlib.NumberTheory.LSeries.HurwitzZeta 189 98455 7.71
Mathlib.NumberTheory.LSeries.HurwitzZetaEven 805 98266 7.72
Mathlib.NumberTheory.LSeries.MellinEqDirichlet 153 97461 7.56
Mathlib.Analysis.SpecialFunctions.Gamma.Deligne 203 97308 7.57
Mathlib.Analysis.SpecialFunctions.Gamma.Beta 589 97105 7.58
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup 442 96516 7.52
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral 353 96074 7.54
Mathlib.Analysis.SpecialFunctions.Gamma.Basic 533 95721 7.56
Mathlib.Analysis.SpecialFunctions.ImproperIntegrals 192 95188 7.59
Mathlib.MeasureTheory.Integral.IntegralEqImproper 1324 94996 7.58
Mathlib.MeasureTheory.Function.Jacobian 1288 93672 7.28
Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace 497 92384 7.29
Mathlib.MeasureTheory.Covering.Besicovitch 1108 91887 7.15
Mathlib.MeasureTheory.Covering.Differentiation 918 90779 7.23
Mathlib.MeasureTheory.Decomposition.Lebesgue 1052 89861 7.27
Mathlib.MeasureTheory.Function.AEEqOfIntegral 697 88809 7.32
Mathlib.MeasureTheory.Integral.SetIntegral 1644 88112 7.29
Mathlib.MeasureTheory.Integral.Bochner 1968 86468 7.27
Mathlib.MeasureTheory.Integral.SetToL1 1648 84500 7.41
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp 989 82852 7.54
Mathlib.MeasureTheory.Function.L1Space 1458 81863 7.62
Mathlib.MeasureTheory.Function.LpOrder 106 80405 6.90
Mathlib.MeasureTheory.Function.LpSpace 1932 80299 6.90
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp 360 78367 6.87
Mathlib.MeasureTheory.Function.LpSeminorm.Basic 1417 78007 6.71
Mathlib.MeasureTheory.Function.AEEqFun 907 76590 5.91
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic 1884 75683 5.87
Mathlib.MeasureTheory.Function.SimpleFuncDense 248 73799 5.89
Mathlib.MeasureTheory.Function.SimpleFunc 1202 73551 5.82
Mathlib.MeasureTheory.Constructions.BorelSpace.Order 1017 72349 5.90
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic 696 71332 5.94
Mathlib.MeasureTheory.Group.Arithmetic 873 70636 5.98
Mathlib.MeasureTheory.Measure.AEMeasurable 423 69763 6.04
Mathlib.MeasureTheory.Measure.Trim 124 69340 6.06
Mathlib.MeasureTheory.Measure.Typeclasses 1574 69216 6.07
Mathlib.MeasureTheory.Measure.Restrict 970 67642 6.19
Mathlib.MeasureTheory.Measure.MeasureSpace 1986 66672 6.26
Mathlib.MeasureTheory.Measure.NullMeasurable 424 64686 6.38
Mathlib.MeasureTheory.Measure.AEDisjoint 137 64262 6.42
Mathlib.MeasureTheory.Measure.MeasureSpaceDef 426 64125 6.43
Mathlib.MeasureTheory.OuterMeasure.Induced 463 63699 6.46
Mathlib.MeasureTheory.OuterMeasure.Caratheodory 240 63236 6.50
Mathlib.MeasureTheory.OuterMeasure.OfFunction 467 62996 6.50
Mathlib.Analysis.SpecificLimits.Basic 734 62529 6.53
Mathlib.Topology.Instances.EReal 447 61795 6.03
Mathlib.Topology.Instances.ENNReal 1435 61348 6.03
Mathlib.Topology.Instances.NNReal 295 59913 6.07
Mathlib.Topology.Instances.Real 233 59618 6.01
Mathlib.Topology.Algebra.UniformGroup.Basic 505 59385 5.01
Mathlib.Topology.UniformSpace.Compact 261 58880 3.79
Mathlib.Topology.UniformSpace.Equicontinuity 1002 58619 3.81
Mathlib.Topology.UniformSpace.UniformConvergenceTopology 1169 57617 3.86
Mathlib.Topology.UniformSpace.Equiv 380 56448 3.90
Mathlib.Topology.UniformSpace.Pi 138 56068 3.91
Mathlib.Topology.UniformSpace.UniformEmbedding 648 55930 3.92
Mathlib.Topology.UniformSpace.Cauchy 815 55282 3.95

removed lines

| Mathlib.Order.Heyting.Basic | 1112 | 14128 | 3.61 |
| Mathlib.Order.PropInstances | 109 | 13016 | 3.83 |
| Mathlib.Order.Disjoint | 698 | 12907 | 3.85 |
| Mathlib.Order.BoundedOrder | 814 | 12209 | 2.66 |
| Mathlib.Order.Lattice | 1311 | 11395 | 2.78 |
| Mathlib.Order.Monotone.Basic | 1087 | 10084 | 3.00 |
| Mathlib.Order.RelClasses | 820 | 8997 | 2.55 |
| Mathlib.Order.Basic | 1375 | 8177 | 2.20 |
| Mathlib.Tactic.Convert | 212 | 6802 | 2.18 |
| Mathlib.Tactic.CongrExclamation | 747 | 6590 | 2.21 |
| Mathlib.Lean.Meta.CongrTheorems | 357 | 5843 | 2.37 |
| Mathlib.Logic.IsEmpty | 206 | 5486 | 2.46 |
| Mathlib.Logic.Function.Basic | 989 | 5280 | 2.52 |
| Mathlib.Logic.Nonempty | 149 | 4291 | 2.07 |
| Mathlib.Algebra.Group.ZeroOne | 27 | 4142 | 1.98 |
| Mathlib.Tactic.ToAdditive | 15 | 4115 | 1.98 |
| Mathlib.Tactic.ToAdditive.Frontend | 1512 | 4100 | 1.99 |
| Mathlib.Tactic.Simps.Basic | 1201 | 2588 | 2.31 |
| Mathlib.Lean.Expr.Basic | 492 | 1387 | 3.22 |
| Mathlib.Init | 37 | 895 | 3.79 |
| Mathlib.Tactic.Linter.Lint | 430 | 858 | 1.93 |
| Batteries.Tactic.Lint | 4 | 428 | 2.76 |
| Batteries.Tactic.Lint.Frontend | 281 | 424 | 1.32 |
| Batteries.Tactic.OpenPrivate | 143 | 143 | 1.00 |
| Lean.Elab.Command | 0 | 0 | NaN |
| Lean.Meta.Diagnostics | 0 | 0 | NaN |
| Lean.PrettyPrinter | 0 | 0 | NaN |
| Lean.PrettyPrinter.Delaborator | 0 | 0 | NaN |
| Lean.PrettyPrinter.Delaborator.Options | 0 | 0 | NaN |
| Lean.Data.Options | 0 | 0 | NaN |
| Lean.ImportingFlag | 0 | 0 | NaN |
| Init.System.IO | 0 | 0 | NaN |
| Init.Control.Reader | 0 | 0 | NaN |
| Init.Control.Basic | 0 | 0 | NaN |
| Init.Core | 0 | 0 | NaN |
| Init.Prelude | 0 | 0 | NaN |

Edward van de Meent (Oct 28 2024 at 12:47):

the issue seems to have fixed itself for now...
(after i tried running it with a specific --to option)
let me see if i can get it to reproduce.

Edward van de Meent (Oct 28 2024 at 12:56):

actually, it seems the issue still exists, it just seemed to disappear because i forgot to add --loc...

Edward van de Meent (Oct 28 2024 at 13:08):

maybe this is a result of my device using windows?

Damiano Testa (Oct 28 2024 at 13:19):

Edward van de Meent said:

maybe this is a result of my device using windows?

Ah, maybe: I am using Linux.

Edward van de Meent (Oct 28 2024 at 13:31):

seems to be an issue with countLOC ... debugging in progress

Edward van de Meent (Oct 28 2024 at 13:41):

the issue seems to be with the line

    let fp := FilePath.mk (( findOLean m).toString.replace ".lake/build/lib/" "")

in windows, the slashes are backwards, so this doesn't get removed

Edward van de Meent (Oct 28 2024 at 13:41):

surely there is a better way to do this, other than string manipulation?

Edward van de Meent (Oct 28 2024 at 13:42):

a hotfix would be to add .replace ".lake\\build\\lib\\" "" to the pipeline

Kim Morrison (Oct 28 2024 at 13:43):

Definitely. Sorry, I copy-pasted that line from another project and forgot to robustify it.

Kim Morrison (Oct 28 2024 at 13:43):

PR very welcome!

Edward van de Meent (Oct 28 2024 at 13:44):

you mean a PR with the hotfix? because i don't think that would be the idiomatic way to do this, and i'm not familiar enough to know what is

Damiano Testa (Oct 28 2024 at 13:44):

Can you link to the line in the code?

Kim Morrison (Oct 28 2024 at 13:45):

Hmm, I was hoping for someone to use the FilePath API to do this.

Edward van de Meent (Oct 28 2024 at 13:45):

here

Damiano Testa (Oct 28 2024 at 13:45):

docs#Lean.SearchPath may be relevant.

Damiano Testa (Oct 28 2024 at 13:48):

Does

import Lean

run_cmd
  dbg_trace  Lean.searchPathRef.get

print the string that should be removed for you?

Edward van de Meent (Oct 28 2024 at 13:50):

it returns many things...

[.\.\.lake/packages\batteries\.lake\build\lib, .\.\.lake/packages\Qq\.lake\build\lib, .\.\.lake/packages\aesop\.lake\build\lib, .\.\.lake/packages\proofwidgets\.lake\build\lib, .\.\.lake/packages\Cli\.lake\build\lib, .\.\.lake/packages\importGraph\.lake\build\lib, .\.\.lake/packages\LeanSearchClient\.lake\build\lib, .\.\.lake\build\lib, .\.\.lake/packages\batteries\.lake\build\lib, .\.\.lake/packages\Qq\.lake\build\lib, .\.\.lake/packages\aesop\.lake\build\lib, .\.\.lake/packages\proofwidgets\.lake\build\lib, .\.\.lake/packages\Cli\.lake\build\lib, .\.\.lake/packages\importGraph\.lake\build\lib, .\.\.lake/packages\LeanSearchClient\.lake\build\lib, .\.\.lake\build\lib, c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\lib\lean, c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\lib\lean]

Damiano Testa (Oct 28 2024 at 13:52):

It looks like the last entry before c:... is the one that we are looking for, right?

Damiano Testa (Oct 28 2024 at 13:53):

(It returns many things for me too: it should be all the paths that lake uses to locate packages.)

Edward van de Meent (Oct 28 2024 at 13:54):

yes, that seems about right...

Damiano Testa (Oct 28 2024 at 13:57):

I also found docs#Lean.moduleNameOfFileName that might take care of doing some conversion for us.

Damiano Testa (Oct 28 2024 at 13:58):

Ah, sorry, this is module and file, not olean...

Edward van de Meent (Oct 28 2024 at 13:58):

i think Lean.SearchPath.findWithExt might be helpful?

Edward van de Meent (Oct 28 2024 at 13:59):

because iiuc, what's going on here is a hack to turn a way of finding the oLean of a module by module name into a way of finding the actual lean file of the module.

Damiano Testa (Oct 28 2024 at 14:00):

Yes, I think so: the olean contains the "actual" information, but the loc proxy requires going back to the source .lean file.

Damiano Testa (Oct 28 2024 at 14:01):

Btw, docs#Lean.SearchPath.findModuleWithExt seems to also do the pathExists check for you.

Edward van de Meent (Oct 28 2024 at 14:01):

right

Damiano Testa (Oct 28 2024 at 14:01):

I have to go now, but if you can get this to work for you on Windows, I can test it later tonight on a Linux computer.

Edward van de Meent (Oct 28 2024 at 14:36):

the more i read into how lean handles module layouts and file directories, the more i realise that things are held together with hopes and prayers... everything feels hacky :sad:

Edward van de Meent (Oct 28 2024 at 14:38):

i guess that's a consequence of the youth of lean, but i do hope this will get more solid sometime

Mario Carneiro (Oct 28 2024 at 15:00):

Could you be more specific? I don't think it's a particularly bad system (and I've seen several particularly bad systems)

Mario Carneiro (Oct 28 2024 at 15:01):

the one thing which I think really goes in the direction of hackish is the ../stage0 hack for getting oleans during bootstrap

Mario Carneiro (Oct 28 2024 at 15:01):

but that basically doesn't impact users outside lean core at all

Yaël Dillies (Oct 28 2024 at 15:05):

I think Edward was thinking of lake exe pole. But that's not part of Lean core

Edward van de Meent (Oct 28 2024 at 15:15):

for now, i hope this is a good fix:

if let .some fp  Lean.SearchPath.findModuleWithExt [s!".{FilePath.pathSeparator}"] "lean" m

Edward van de Meent (Oct 28 2024 at 15:16):

basically, i create a path for the directory this gets run from and hope the things you're interested in can be found from there...

Edward van de Meent (Oct 28 2024 at 15:17):

it still feels like a hack, but at least we're using the proper functions...

Edward van de Meent (Oct 28 2024 at 15:17):

or, well, some proper functions

Edward van de Meent (Oct 28 2024 at 15:36):

PR at #18341 .

Edward van de Meent (Oct 28 2024 at 15:37):

if someone could test this on linux, please do, and leave a comment here or on the PR.

Mario Carneiro (Oct 28 2024 at 15:37):

oh yeah, mathlib scripts are quite often held together with duct tape and glue

Edward van de Meent (Oct 28 2024 at 15:38):

the funny thing is that i also read the documentation for ImportGraph.getCurrentModule...

Damiano Testa (Oct 28 2024 at 19:51):

I just tried it and it seems to work on my computer (Linux):

$ lake exe pole --loc
Analyzing Mathlib at bbfb7d1f1cb294d9135ca93d5569ed28c3bcc9ec

file LoC cumulative parallelism
Mathlib 5042 104338 14.58
Mathlib.NumberTheory.LSeries.DirichletContinuation 301 99296 7.93
Mathlib.NumberTheory.LSeries.ZMod 527 98995 7.94
Mathlib.NumberTheory.LSeries.RiemannZeta 243 98468 7.40
Mathlib.NumberTheory.LSeries.HurwitzZeta 189 98225 7.42
Mathlib.NumberTheory.LSeries.HurwitzZetaEven 805 98036 7.43
Mathlib.NumberTheory.LSeries.MellinEqDirichlet 153 97231 7.26
Mathlib.Analysis.SpecialFunctions.Gamma.Deligne 203 97078 7.27
Mathlib.Analysis.SpecialFunctions.Gamma.Beta 589 96875 7.28
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup 442 96286 7.22
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral 353 95844 7.24
Mathlib.Analysis.SpecialFunctions.Gamma.Basic 533 95491 7.26
Mathlib.Analysis.SpecialFunctions.ImproperIntegrals 192 94958 7.29
Mathlib.MeasureTheory.Integral.IntegralEqImproper 1324 94766 7.27
Mathlib.MeasureTheory.Function.Jacobian 1288 93442 6.96
Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace 497 92154 6.98
Mathlib.MeasureTheory.Covering.Besicovitch 1108 91657 6.84
Mathlib.MeasureTheory.Covering.Differentiation 918 90549 6.90
Mathlib.MeasureTheory.Decomposition.Lebesgue 1052 89631 6.94
Mathlib.MeasureTheory.Function.AEEqOfIntegral 697 88579 6.99
Mathlib.MeasureTheory.Integral.SetIntegral 1644 87882 6.96
Mathlib.MeasureTheory.Integral.Bochner 1968 86238 6.93
Mathlib.MeasureTheory.Integral.SetToL1 1648 84270 7.07
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp 989 82622 7.19
Mathlib.MeasureTheory.Function.L1Space 1458 81633 7.27
Mathlib.MeasureTheory.Function.LpOrder 106 80175 6.53
Mathlib.MeasureTheory.Function.LpSpace 1932 80069 6.54
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp 360 78137 6.50
Mathlib.MeasureTheory.Function.LpSeminorm.Basic 1417 77777 6.34
Mathlib.MeasureTheory.Function.AEEqFun 907 76360 5.53
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic 1887 75453 5.48
Mathlib.MeasureTheory.Function.SimpleFuncDense 248 73566 5.49
Mathlib.MeasureTheory.Function.SimpleFunc 1196 73318 5.41
Mathlib.MeasureTheory.Constructions.BorelSpace.Order 1017 72122 5.49
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic 699 71105 5.53
Mathlib.MeasureTheory.Group.Arithmetic 873 70406 5.56
Mathlib.MeasureTheory.Measure.AEMeasurable 423 69533 5.62
Mathlib.MeasureTheory.Measure.Trim 124 69110 5.64
Mathlib.MeasureTheory.Measure.Typeclasses 1574 68986 5.64
Mathlib.MeasureTheory.Measure.Restrict 970 67412 5.75
Mathlib.MeasureTheory.Measure.MeasureSpace 1986 66442 5.82
Mathlib.MeasureTheory.Measure.NullMeasurable 424 64456 5.93
Mathlib.MeasureTheory.Measure.AEDisjoint 137 64032 5.96
Mathlib.MeasureTheory.Measure.MeasureSpaceDef 426 63895 5.97
Mathlib.MeasureTheory.OuterMeasure.Induced 463 63469 6.00
Mathlib.MeasureTheory.OuterMeasure.Caratheodory 240 63006 6.03
Mathlib.MeasureTheory.OuterMeasure.OfFunction 467 62766 6.03
Mathlib.Analysis.SpecificLimits.Basic 734 62299 6.06
Mathlib.Topology.Instances.EReal 453 61565 5.56
Mathlib.Topology.Instances.ENNReal 1438 61112 5.55
Mathlib.Topology.Instances.NNReal 295 59674 5.58
Mathlib.Topology.Instances.Real 233 59379 5.51
Mathlib.Topology.Algebra.UniformGroup.Basic 505 59146 4.51
Mathlib.Topology.UniformSpace.Compact 261 58641 3.29
Mathlib.Topology.UniformSpace.Equicontinuity 1002 58380 3.30
Mathlib.Topology.UniformSpace.UniformConvergenceTopology 1169 57378 3.34
Mathlib.Topology.UniformSpace.Equiv 380 56209 3.37
Mathlib.Topology.UniformSpace.Pi 138 55829 3.39
Mathlib.Topology.UniformSpace.UniformEmbedding 655 55691 3.39
Mathlib.Topology.UniformSpace.Cauchy 815 55036 3.41
Mathlib.Topology.Algebra.Constructions 155 54221 3.41
Mathlib.Topology.Homeomorph 994 54066 3.42
Mathlib.Topology.Support 431 53072 3.45
Mathlib.Topology.Separation.Basic 2608 52641 3.25
Mathlib.Topology.Compactness.Lindelof 753 50033 3.28
Mathlib.Topology.Compactness.SigmaCompact 426 49280 3.31
Mathlib.Topology.Compactness.LocallyCompact 225 48854 3.33
Mathlib.Topology.Compactness.Compact 1142 48629 3.35
Mathlib.Topology.Bases 989 47487 3.39
Mathlib.Topology.ContinuousOn 1329 46498 3.43
Mathlib.Topology.Constructions 1770 45169 3.48
... ... ... ...
... ... ... ...
... ... ... ...
Mathlib.Order.Basic 1375 7794 1.81
Mathlib.Tactic.Convert 212 6419 1.78
Mathlib.Tactic.CongrExclamation 747 6207 1.81
Mathlib.Lean.Meta.CongrTheorems 357 5460 1.92
Mathlib.Logic.IsEmpty 206 5103 1.98
Mathlib.Logic.Function.Basic 989 4897 2.03
Mathlib.Logic.Nonempty 149 3908 1.56
Mathlib.Algebra.Group.ZeroOne 27 3759 1.47
Mathlib.Tactic.ToAdditive 15 3732 1.47
Mathlib.Tactic.ToAdditive.Frontend 1512 3717 1.47
Mathlib.Tactic.Simps.Basic 1201 2205 1.60
Mathlib.Lean.Expr.Basic 492 1004 2.20
Mathlib.Init 36 512 3.35
Mathlib.Tactic.Linter.Lint 430 476 1.00
Mathlib.Tactic.DeclarationNames 46 46 1.00
Lean.DeclarationRange 0 0 NaN
Lean.MonadEnv 0 0 NaN
Lean.Environment 0 0 NaN
Init.Control.StateRef 0 0 NaN
Init.System.IO 0 0 NaN
Init.Control.Reader 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Kim Morrison (Oct 29 2024 at 00:42):

#18341 works for me on mac as well, so I've :merge:'d.

Kim Morrison (Oct 29 2024 at 03:40):

https://github.com/leanprover-community/import-graph/pull/39

should both make the existing lake exe unused much faster, and enable a newer version of lake exe unused which can be run on all of Mathlib (rather than just a linear sequence of modules).

Pinging @Jon Eugster as import-graph maintainer.

Kim Morrison (Oct 29 2024 at 04:26):

and https://github.com/leanprover-community/import-graph/pull/40 allows multiple (comma-separated) --to and --from arguments.

Kim Morrison (Oct 29 2024 at 04:27):

What I'd really like is some visual indication of the modules appearing in --to and --from, but our rendering code is already quite complicated to handle the markedModule machinery (which, I think is not really being used ...)

Kim Morrison (Oct 29 2024 at 04:34):

Ahha! Node shapes work nicely enough:
o.png

Kim Morrison (Oct 29 2024 at 04:34):

This is included in import-graph#40 now.

Jon Eugster (Oct 29 2024 at 08:32):

Kim Morrison said:

... our rendering code is already quite complicated to handle the markedModule machinery (which, I think is not really being used ...)

I use it sometimes! I find the graph of --include-lean (or --include-deps) and other's quite useless without the highlighting. But you're right that it isn't used in the mathlib CI or thelike.

And some code cleanup would indeed be due, some stuff grew convoluted. Might do that in the next few weeks.

Kim Morrison (Oct 29 2024 at 10:22):

No, you're right, I remember finding markedModule quite useful when trying to understand where we're using Batteries in Mathlib.

Kim Morrison (Oct 30 2024 at 00:10):

I've updated import-graph#40 and it is hopefully ready to go now.

Andrew Yang (Nov 11 2024 at 07:29):

I want to try out lake exe pole but it gives a 'main' has already been declared error for me, which clashes with main function of ImportGraph. What am I missing?

Johan Commelin (Nov 11 2024 at 07:30):

Yeah, I stumbled on this last week as well. I'll try to fix it today.

Johan Commelin (Nov 11 2024 at 07:31):

Atm it's broken. Unfortunately CI hasn't caught this

Edward van de Meent (Nov 11 2024 at 08:21):

From the looks of it, this is because ImportGraph.UnusedTransitiveImports main gets imported

Edward van de Meent (Nov 11 2024 at 08:23):

(transitively)

Johan Commelin (Nov 11 2024 at 08:24):

Part 1: https://github.com/leanprover-community/import-graph/pull/43

Johan Commelin (Nov 11 2024 at 08:28):

Part 2: #18846

Johan Commelin (Nov 11 2024 at 08:28):

These two are independent, and both should fix the issue.

Yaël Dillies (Dec 01 2024 at 08:29):

@Ruben Van de Velde, did #19638 reduce the longest pole? If so, that was completely accidental! (but good :smile:)

Yaël Dillies (Dec 01 2024 at 09:34):

#19651 renames Topology.Support to Topology.Algebra.Support. This will motivate the import reduction to Topology.Homeomorph

Ruben Van de Velde (Dec 01 2024 at 09:41):

I thought so for a moment, but maybe not. I can't verify until the bench server is back up

Kim Morrison (Dec 10 2024 at 08:53):

Oops, this is also broken:

% lake exe pole
uncaught exception: parser 'subscript' was not found

Kim Morrison (Dec 10 2024 at 08:54):

(My understanding is that this, and lean4checker, are waiting on discussion between @Mario Carneiro and @Sebastian Ullrich at lean#6325.)

Eric Wieser (Dec 10 2024 at 13:15):

We can work around it today by telling the script to run initializers, which is much less scary than it was for leanchecker

Kim Morrison (Dec 10 2024 at 23:08):

Fixed in #19878. I also needed to update some URLs, which presumably will explain (and fix) the recent failures of the benchmark summary bot.

Kim Morrison (Dec 10 2024 at 23:08):

| file                                                                 | instructions | cumulative | parallelism |
| :------------------------------------------------------------------- | -----------: | ---------: | :---------: |
| Mathlib                                                              |        11861 |    6018901 |    23.78    |
| Mathlib.Analysis.CStarAlgebra.ApproximateUnit                        |       155439 |    6007039 |    7.99     |
| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order     |       234990 |    5851600 |    8.12     |
| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances |       313168 |    5616609 |    8.38     |
| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic     |        49989 |    5303441 |    8.69     |
| Mathlib.Analysis.CStarAlgebra.GelfandDuality                         |        81200 |    5253451 |    8.76     |
| Mathlib.Analysis.CStarAlgebra.Spectrum                               |        49279 |    5172251 |    8.73     |
| Mathlib.Analysis.Normed.Algebra.Spectrum                             |       125365 |    5122971 |    8.77     |
| Mathlib.Analysis.Complex.Polynomial.Basic                            |        25984 |    4997605 |    8.88     |
| Mathlib.Analysis.Complex.Liouville                                   |        15667 |    4971621 |    8.26     |
| Mathlib.Analysis.Complex.CauchyIntegral                              |        42234 |    4955953 |    8.29     |
| Mathlib.MeasureTheory.Integral.CircleIntegral                        |        63186 |    4913718 |    8.17     |
| Mathlib.Analysis.SpecialFunctions.NonIntegrable                      |        14026 |    4850532 |    8.27     |
| Mathlib.Analysis.SpecialFunctions.Log.Deriv                          |        39161 |    4836505 |    6.72     |
| Mathlib.Analysis.SpecialFunctions.ExpDeriv                           |        31631 |    4797344 |    6.73     |
| Mathlib.Analysis.Complex.RealDeriv                                   |        25947 |    4765712 |    5.82     |
| Mathlib.Analysis.Calculus.ContDiff.Basic                             |       420941 |    4739765 |    5.52     |
| Mathlib.Analysis.Calculus.FDeriv.Mul                                 |       371457 |    4318824 |    5.86     |
| Mathlib.Analysis.Calculus.FDeriv.Analytic                            |       250379 |    3947366 |    6.32     |
| Mathlib.Analysis.Analytic.CPolynomial                                |       133438 |    3696987 |    6.37     |
| Mathlib.Analysis.Analytic.Constructions                              |       117552 |    3563548 |    6.55     |
| Mathlib.Analysis.Analytic.Composition                                |       141559 |    3445996 |    6.67     |
| Mathlib.Analysis.Analytic.Basic                                      |       231851 |    3304436 |    6.90     |
| Mathlib.Analysis.Calculus.FormalMultilinearSeries                    |        67915 |    3072585 |    6.87     |
| Mathlib.Analysis.NormedSpace.Multilinear.Curry                       |       207820 |    3004670 |    7.01     |
| Mathlib.Analysis.NormedSpace.Multilinear.Basic                       |       274792 |    2796849 |    7.45     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace                |        58146 |    2522056 |    8.04     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear                   |       181397 |    2463910 |    8.19     |
| Mathlib.Analysis.NormedSpace.OperatorNorm.Basic                      |        79124 |    2282512 |    8.76     |
| Mathlib.Topology.Algebra.Module.StrongTopology                       |        93949 |    2203388 |    8.63     |
| Mathlib.Topology.Algebra.Module.UniformConvergence                   |        12237 |    2109438 |    8.95     |
| Mathlib.Analysis.LocallyConvex.Bounded                               |        36845 |    2097201 |    8.98     |
| Mathlib.Analysis.Seminorm                                            |       133376 |    2060355 |    8.72     |
| Mathlib.Analysis.LocallyConvex.Basic                                 |        27852 |    1926979 |    9.21     |
| Mathlib.Analysis.Normed.Module.Basic                                 |        44488 |    1899127 |    8.85     |
| Mathlib.Analysis.Normed.Field.Lemmas                                 |        26232 |    1854638 |    9.01     |
| Mathlib.Analysis.Normed.Group.Uniform                                |        29879 |    1828406 |    8.18     |
| Mathlib.Topology.MetricSpace.Algebra                                 |        12091 |    1798527 |    8.10     |
| Mathlib.Topology.Algebra.SeparationQuotient.Basic                    |        28186 |    1786435 |    7.05     |
| Mathlib.Topology.Algebra.Module.Basic                                |       239872 |    1758248 |    7.15     |
| Mathlib.Topology.Algebra.UniformGroup.Defs                           |        48082 |    1518376 |    6.53     |
| Mathlib.Topology.Algebra.Group.Basic                                 |        88018 |    1470293 |    6.68     |
| Mathlib.Topology.Algebra.Monoid                                      |        42235 |    1382275 |    5.49     |
| Mathlib.Topology.Algebra.MulAction                                   |        11045 |    1340039 |    5.28     |
| Mathlib.Topology.Algebra.ConstMulAction                              |        30268 |    1328994 |    5.29     |
| Mathlib.Topology.Algebra.Constructions                               |         5964 |    1298725 |    4.99     |
| Mathlib.Topology.Homeomorph                                          |        32622 |    1292761 |    5.01     |
| Mathlib.Topology.Algebra.Support                                     |        12821 |    1260138 |    5.08     |
| Mathlib.Topology.Separation.Basic                                    |        59883 |    1247317 |    4.73     |
| Mathlib.Topology.Compactness.Lindelof                                |        17778 |    1187433 |    4.80     |
| Mathlib.Topology.Compactness.SigmaCompact                            |         9841 |    1169654 |    4.85     |
| Mathlib.Topology.Compactness.LocallyCompact                          |         6503 |    1159813 |    4.88     |
| Mathlib.Topology.Compactness.Compact                                 |        32008 |    1153310 |    4.90     |
| Mathlib.Topology.Bases                                               |        34781 |    1121301 |    4.69     |
| Mathlib.Topology.ContinuousOn                                        |        37171 |    1086520 |    4.80     |
| Mathlib.Topology.Constructions                                       |        47108 |    1049348 |    4.93     |
| Mathlib.Topology.Maps.Basic                                          |        15033 |    1002240 |    4.88     |
| Mathlib.Topology.Order                                               |        21228 |     987206 |    4.94     |
| Mathlib.Topology.Defs.Induced                                        |         3430 |     965977 |    5.02     |
| Mathlib.Topology.Basic                                               |        36725 |     962546 |    5.04     |
| Mathlib.Order.Filter.AtTopBot                                        |        36056 |     925821 |    5.00     |
| Mathlib.Order.Filter.Bases                                           |        21339 |     889765 |    4.98     |
| Mathlib.Order.Filter.Finite                                          |        11026 |     868425 |    5.07     |

Kim Morrison (Dec 10 2024 at 23:09):

| Mathlib.Data.Set.Finite.Lattice                                      |        12050 |     857399 |    5.05     |
| Mathlib.Data.Finite.Sigma                                            |         2417 |     845348 |    5.01     |
| Mathlib.Data.Fintype.Sigma                                           |        16484 |     842931 |    4.96     |
| Mathlib.Data.Finset.Sigma                                            |         9260 |     826446 |    4.94     |
| Mathlib.Data.Finset.Lattice.Fold                                     |        52821 |     817185 |    4.95     |
| Mathlib.Data.Finset.Prod                                             |        12782 |     764363 |    4.66     |
| Mathlib.Data.Finset.Card                                             |        23351 |     751580 |    4.72     |
| Mathlib.Data.Finset.Image                                            |        21820 |     728229 |    4.84     |
| Mathlib.Data.Finset.Union                                            |         8843 |     706409 |    4.89     |
| Mathlib.Data.Finset.Basic                                            |        18172 |     697565 |    4.42     |
| Mathlib.Data.Finset.SDiff                                            |         7228 |     679392 |    4.44     |
| Mathlib.Data.Finset.Lattice.Lemmas                                   |         5195 |     672164 |    4.48     |
| Mathlib.Data.Finset.Insert                                           |        14431 |     666968 |    4.49     |
| Mathlib.Data.Finset.Empty                                            |         5145 |     652536 |    4.51     |
| Mathlib.Data.Finset.Defs                                             |         9325 |     647390 |    4.54     |
| Mathlib.Data.Multiset.Nodup                                          |         9343 |     638064 |    4.59     |
| Mathlib.Data.Multiset.Range                                          |         2842 |     628721 |    4.64     |
| Mathlib.Data.Multiset.Basic                                          |        72729 |     625879 |    4.66     |
| Mathlib.Data.List.Perm.Lattice                                       |         3834 |     553149 |    4.57     |
| Mathlib.Data.List.Nodup                                              |        11083 |     549314 |    4.59     |
| Mathlib.Data.Set.Pairwise.Basic                                      |        28015 |     538231 |    4.49     |
| Mathlib.Data.Set.Function                                            |        46707 |     510215 |    4.02     |
| Mathlib.Data.Set.Prod                                                |        32061 |     463508 |    4.32     |
| Mathlib.Data.Set.Image                                               |        31303 |     431447 |    4.57     |
| Mathlib.Data.Set.Subsingleton                                        |         7109 |     400143 |    4.04     |
| Mathlib.Data.Set.Basic                                               |        59989 |     393033 |    4.10     |
| Mathlib.Order.BooleanAlgebra                                         |        32922 |     333044 |    4.11     |
| Mathlib.Order.Heyting.Basic                                          |        39352 |     300121 |    4.46     |
| Mathlib.Order.PropInstances                                          |         3177 |     260768 |    4.98     |
| Mathlib.Order.Disjoint                                               |        15940 |     257591 |    5.03     |
| Mathlib.Order.BoundedOrder.Lattice                                   |         3955 |     241651 |    5.29     |
| Mathlib.Order.Lattice                                                |        25650 |     237695 |    3.17     |
| Mathlib.Order.Monotone.Basic                                         |        20794 |     212045 |    3.42     |
| Mathlib.Order.RelClasses                                             |        13315 |     191251 |    2.39     |
| Mathlib.Order.Basic                                                  |        28168 |     177935 |    2.35     |
| Mathlib.Tactic.Convert                                               |         5448 |     149767 |    2.18     |
| Mathlib.Tactic.CongrExclamation                                      |        19182 |     144319 |    2.22     |
| Mathlib.Lean.Meta.CongrTheorems                                      |        10941 |     125137 |    2.41     |
| Mathlib.Logic.IsEmpty                                                |         3326 |     114196 |    2.55     |
| Mathlib.Logic.Function.Basic                                         |        14403 |     110869 |    2.57     |
| Mathlib.Logic.Nonempty                                               |         2314 |      96465 |    2.09     |
| Mathlib.Algebra.Group.ZeroOne                                        |         1106 |      94151 |    2.01     |
| Mathlib.Tactic.ToAdditive                                            |         1055 |      93044 |    2.03     |
| Mathlib.Tactic.ToAdditive.Frontend                                   |        34467 |      91988 |    2.04     |
| Mathlib.Tactic.Simps.Basic                                           |        32764 |      57521 |    2.17     |
| Mathlib.Lean.Expr.Basic                                              |         9171 |      24756 |    3.56     |
| Mathlib.Init                                                         |          757 |      15585 |    4.11     |
| Mathlib.Tactic.Linter.Lint                                           |         2097 |      14828 |    2.69     |
| Batteries.Tactic.Lint                                                |          605 |      12731 |    2.39     |
| Batteries.Tactic.Lint.Frontend                                       |         8850 |      12125 |    1.22     |
| Batteries.Tactic.OpenPrivate                                         |         3275 |       3275 |    1.00     |
| Lean.Elab.Command                                                    |            0 |          0 |     NaN     |
| Lean.Meta.Diagnostics                                                |            0 |          0 |     NaN     |
| Lean.PrettyPrinter                                                   |            0 |          0 |     NaN     |
| Lean.PrettyPrinter.Delaborator                                       |            0 |          0 |     NaN     |
| Lean.PrettyPrinter.Delaborator.Options                               |            0 |          0 |     NaN     |
| Lean.Data.Options                                                    |            0 |          0 |     NaN     |
| Lean.ImportingFlag                                                   |            0 |          0 |     NaN     |
| Init.System.IO                                                       |            0 |          0 |     NaN     |
| Init.System.IOError                                                  |            0 |          0 |     NaN     |
| Init.Data.ToString.Basic                                             |            0 |          0 |     NaN     |
| Init.Data.Repr                                                       |            0 |          0 |     NaN     |
| Init.Data.Format.Basic                                               |            0 |          0 |     NaN     |
| Init.Control.State                                                   |            0 |          0 |     NaN     |
| Init.Control.Basic                                                   |            0 |          0 |     NaN     |
| Init.Core                                                            |            0 |          0 |     NaN     |
| Init.Prelude                                                         |            0 |          0 |     NaN     |

Kim Morrison (Dec 10 2024 at 23:50):

Some interesting output from scripts/unused_in_pole.sh:

  • unused3.pdf
    Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds imports Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable but then doesn't need anything from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation which has substantial imports.

  • unused4.pdf
    Mathlib.Topology.Homeomorph has many imports which are not needed by many downstream users of Homeomorph.

  • unused5.pdf
    The chain from Mathlib.Topology.ContinuousOn to Mathlib.Analysis.SpecificLimits.Basic has a lot of intermediate steps which aren't used.

Kim Morrison (Dec 10 2024 at 23:51):

(Note this is reporting on a different long pole than the table above, because unused_in_pole uses LoC instead of speed center instruction counts to determine the longest pole.)

Anne Baanen (Jan 13 2025 at 10:58):

It's been a while since we've looked at the pole. So have a fresh report:

Analyzing Mathlib at 6ee88ac3b2eceab3b4fbd2a91a9a87011c06a271

file instructions cumulative parallelism
Mathlib 12287 6088063 24.97
Mathlib.Analysis.CStarAlgebra.ApproximateUnit 152028 6075776 8.24
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 226638 5923747 8.37
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 307794 5697108 8.63
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 48744 5389314 8.94
Mathlib.Analysis.CStarAlgebra.GelfandDuality 83077 5340570 9.01
Mathlib.Analysis.CStarAlgebra.Spectrum 49868 5257492 9.00
Mathlib.Analysis.Normed.Algebra.Spectrum 128893 5207624 9.04
Mathlib.Analysis.Complex.Polynomial.Basic 26460 5078731 9.19
Mathlib.Analysis.Complex.Liouville 17501 5052270 8.56
Mathlib.Analysis.Complex.CauchyIntegral 46470 5034768 8.59
Mathlib.MeasureTheory.Integral.CircleIntegral 65966 4988298 8.48
Mathlib.Analysis.SpecialFunctions.NonIntegrable 16717 4922332 8.58
Mathlib.Analysis.SpecialFunctions.Log.Deriv 42053 4905614 7.01
Mathlib.Analysis.SpecialFunctions.ExpDeriv 33512 4863561 7.02
Mathlib.Analysis.Complex.RealDeriv 27882 4830048 6.07
Mathlib.Analysis.Calculus.ContDiff.Basic 441766 4802166 5.74
Mathlib.Analysis.Calculus.FDeriv.Mul 426217 4360399 6.11
Mathlib.Analysis.Calculus.FDeriv.Analytic 260994 3934182 6.65
Mathlib.Analysis.Analytic.CPolynomial 136232 3673187 6.69
Mathlib.Analysis.Analytic.Constructions 143060 3536955 6.89
Mathlib.Analysis.Analytic.Composition 143935 3393895 7.06
Mathlib.Analysis.Analytic.Basic 248860 3249959 7.32
Mathlib.Analysis.Calculus.FormalMultilinearSeries 76885 3001099 7.33
Mathlib.Analysis.NormedSpace.Multilinear.Curry 212899 2924213 7.49
Mathlib.Analysis.NormedSpace.Multilinear.Basic 275020 2711314 8.00
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 59368 2436294 8.66
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 183461 2376925 8.83
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 80061 2193463 9.49
Mathlib.Topology.Algebra.Module.StrongTopology 86938 2113402 9.38
Mathlib.Topology.Algebra.Module.UniformConvergence 12724 2026463 9.65
Mathlib.Analysis.LocallyConvex.Bounded 37961 2013739 9.68
Mathlib.Analysis.Seminorm 133219 1975778 9.41
Mathlib.Analysis.LocallyConvex.Basic 27989 1842559 9.97
Mathlib.Analysis.Normed.Module.Basic 44881 1814569 9.57
Mathlib.Analysis.Normed.Field.Lemmas 25465 1769688 9.76
Mathlib.Analysis.Normed.Field.Basic 117443 1744223 8.15
Mathlib.Analysis.Normed.Group.Constructions 17856 1626779 7.04
Mathlib.Analysis.Normed.Group.Basic 84409 1608922 7.10
Mathlib.Topology.Metrizable.Uniformity 15131 1524513 7.24
Mathlib.Topology.Metrizable.Basic 5304 1509381 7.28
Mathlib.Topology.MetricSpace.Basic 8603 1504077 7.30
Mathlib.Topology.MetricSpace.Pseudo.Lemmas 7222 1495473 7.21
Mathlib.Topology.MetricSpace.Pseudo.Constructions 16215 1488250 7.04
Mathlib.Topology.MetricSpace.Pseudo.Defs 43264 1472035 6.82
Mathlib.Topology.EMetricSpace.Defs 31623 1428771 6.76
Mathlib.Data.ENNReal.Inv 84456 1397147 6.34
Mathlib.Data.ENNReal.Operations 42073 1312690 6.68
Mathlib.Data.ENNReal.Basic 27043 1270616 5.40
Mathlib.Data.NNReal.Defs 49667 1243573 5.47
Mathlib.Data.Real.Archimedean 20519 1193905 5.36
Mathlib.Algebra.Order.Archimedean.Basic 56614 1173385 5.07
Mathlib.Data.Rat.Floor 17472 1116771 5.27
Mathlib.Algebra.Order.Floor 143902 1099299 5.29
Mathlib.Tactic.Linarith 2680 955396 5.55
Mathlib.Tactic.Linarith.Frontend 11831 952715 5.11
Mathlib.Tactic.Ring.Basic 138318 940883 4.69
Mathlib.Tactic.NormNum.Inv 19507 802565 5.29
Mathlib.Data.Rat.Cast.CharZero 7825 783058 5.29
Mathlib.Data.Rat.Cast.Defs 16595 775232 5.33
Mathlib.Algebra.Field.Rat 5128 758636 5.09
Mathlib.Data.NNRat.Defs 15738 753508 5.11
Mathlib.Algebra.Order.Ring.Unbundled.Nonneg 14135 737770 5.02
Mathlib.Order.CompleteLatticeIntervals 15556 723634 4.29
Mathlib.Order.ConditionallyCompleteLattice.Basic 28065 708078 4.23
Mathlib.Data.Set.Lattice 82209 680012 4.36
Mathlib.Order.CompleteBooleanAlgebra 44212 597802 4.17
Mathlib.Order.CompleteLattice 51864 553590 4.42
Mathlib.Order.Hom.Set 8633 501725 4.48
Mathlib.Logic.Equiv.Set 18657 493092 4.28
Mathlib.Data.Set.Function 47413 474434 4.40
Mathlib.Data.Set.Prod 32703 427021 4.78
Mathlib.Data.Set.Image 31306 394317 5.10
Mathlib.Data.Set.Subsingleton 7827 363010 4.55
Mathlib.Data.Set.Basic 59953 355183 4.62
Mathlib.Order.BooleanAlgebra 33465 295230 4.78
Mathlib.Order.Heyting.Basic 40111 261764 5.26
Mathlib.Order.PropInstances 3311 221652 6.03
Mathlib.Order.Disjoint 16338 218341 6.11
Mathlib.Order.BoundedOrder.Lattice 4643 202003 6.52
Mathlib.Order.Lattice 25825 197360 3.99
Mathlib.Order.Monotone.Basic 21458 171534 4.41
Mathlib.Order.RelClasses 14012 150076 3.19

Anne Baanen (Jan 13 2025 at 10:58):

file instructions cumulative parallelism
Mathlib.Order.Basic 28226 136063 3.21
Mathlib.Tactic.Convert 5545 107837 2.36
Mathlib.Tactic.CongrExclamation 19615 102291 2.43
Mathlib.Lean.Meta.CongrTheorems 11011 82676 2.77
Mathlib.Logic.IsEmpty 3621 71665 3.05
Mathlib.Logic.Function.Basic 14748 68043 3.11
Mathlib.Order.Defs.Unbundled 4279 53294 2.52
Mathlib.Tactic.SplitIfs 17477 49014 2.36
Mathlib.Tactic.Core 5681 31537 3.12
Mathlib.Lean.Expr.Basic 9805 25856 3.58
Mathlib.Init 875 16050 4.22
Mathlib.Tactic.Linter.Lint 2312 15174 2.68
Batteries.Tactic.Lint 640 12861 2.39
Batteries.Tactic.Lint.Frontend 8907 12221 1.22
Batteries.Tactic.OpenPrivate 3314 3314 1.00
Lean.Elab.Command 0 0 NaN
Lean.Meta.Diagnostics 0 0 NaN
Lean.PrettyPrinter 0 0 NaN
Lean.PrettyPrinter.Delaborator 0 0 NaN
Lean.PrettyPrinter.Delaborator.Options 0 0 NaN
Lean.Data.Options 0 0 NaN
Lean.ImportingFlag 0 0 NaN
Init.System.IO 0 0 NaN
Init.System.IOError 0 0 NaN
Init.Data.ToString.Basic 0 0 NaN
Init.Data.Repr 0 0 NaN
Init.Data.Format.Basic 0 0 NaN
Init.Control.State 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Kim Morrison (Jan 13 2025 at 11:13):

A longest pole that doesn't go through the development of finiteness! Wow.

Kim Morrison (Jan 13 2025 at 11:14):

Seems crazy to me that Mathlib.Order.CompleteLatticeIntervals is a dependency of the ring tactic... :-(

Kim Morrison (Jan 13 2025 at 11:15):

Mathlib.Topology.EMetricSpace.Defs depending on Mathlib.Data.ENNReal.Inv seems suspicious. Surely for the definitions inverses are not needed!

Anne Baanen (Jan 13 2025 at 11:22):

Interesting unused imports:

  • unused1.pdf Basically the same as unused3.pdf from last month: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds imports Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable but then doesn't need anything from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation which has substantial imports.
  • unused2.pdf Mathlib.Topology.Homeomorph imports compactness, which topological monoids/groups don't need, and it also looks like we might also be able to cut off some MulAction dependencies.
  • unused5.pdf: Mathlib.Topology.Semicontinuous depends on Mathlib.Topology.Instances.ENNReal and Mathlib.Topology.Instances.NNReal which in turn import a lot that Semicontinous doesn't need.

Kim Morrison (Jan 13 2025 at 11:24):

@Anne Baanen, note that these unusedi.pdf files you're generating are actually for a different longest pole.

Kim Morrison (Jan 13 2025 at 11:25):

We need to remove the --loc flag in scripts/unused_in_pole.sh.

Kim Morrison (Jan 13 2025 at 11:25):

(I think that was there because at the time I wrote the script the speedcenter was down, so instruction counts weren't available.)

Anne Baanen (Jan 13 2025 at 11:25):

I was confused about that for a moment! It turns out pole --loc does go through finiteness:

file LoC cumulative parallelism
Mathlib 5563 98959 16.36
Mathlib.NumberTheory.LSeries.PrimesInAP 492 93396 9.51
Mathlib.NumberTheory.LSeries.Nonvanishing 421 92904 8.73
Mathlib.NumberTheory.LSeries.DirichletContinuation 394 92483 8.74
Mathlib.NumberTheory.EulerProduct.DirichletLSeries 211 92089 8.28
Mathlib.NumberTheory.LSeries.Dirichlet 418 91878 8.29
Mathlib.NumberTheory.LSeries.RiemannZeta 243 91460 8.12
Mathlib.NumberTheory.LSeries.HurwitzZeta 189 91217 8.13
Mathlib.NumberTheory.LSeries.HurwitzZetaEven 808 91028 8.14
Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds 279 90220 8.15
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable 534 89941 8.17
Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation 132 89407 8.20
Mathlib.Analysis.Fourier.PoissonSummation 221 89275 8.21
Mathlib.Analysis.Distribution.FourierSchwartz 111 89054 8.22
Mathlib.Analysis.Fourier.Inversion 190 88943 7.98
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform 366 88753 7.99
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral 375 88387 7.92
Mathlib.Analysis.SpecialFunctions.Gamma.Basic 533 88012 7.94
Mathlib.Analysis.SpecialFunctions.ImproperIntegrals 192 87479 7.98
Mathlib.MeasureTheory.Integral.IntegralEqImproper 1320 87287 7.97
Mathlib.MeasureTheory.Function.Jacobian 1291 85967 7.63
Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace 499 84676 7.65
Mathlib.MeasureTheory.Covering.Besicovitch 1112 84177 7.42
Mathlib.MeasureTheory.Covering.Differentiation 916 83065 7.50
Mathlib.MeasureTheory.Integral.Average 785 82149 7.54
Mathlib.MeasureTheory.Integral.SetIntegral 1659 81364 7.60
Mathlib.MeasureTheory.Integral.Bochner 1972 79705 7.58
Mathlib.MeasureTheory.Integral.SetToL1 1639 77733 7.74
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp 983 76094 7.89
Mathlib.MeasureTheory.Function.L1Space 1538 75111 7.98
Mathlib.MeasureTheory.Function.LpOrder 106 73573 7.34
Mathlib.MeasureTheory.Function.LpSpace 1929 73467 7.35
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp 395 71538 7.32
Mathlib.MeasureTheory.Function.LpSeminorm.Basic 1475 71143 7.15
Mathlib.MeasureTheory.Function.AEEqFun 907 69668 6.13
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic 1890 68761 6.10
Mathlib.MeasureTheory.Function.SimpleFuncDense 248 66871 6.10
Mathlib.MeasureTheory.Function.SimpleFunc 1265 66623 6.02
Mathlib.MeasureTheory.Constructions.BorelSpace.Order 1022 65358 6.11
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic 699 64336 6.18
Mathlib.MeasureTheory.Group.Arithmetic 873 63637 6.23
Mathlib.MeasureTheory.Measure.AEMeasurable 423 62764 6.30
Mathlib.MeasureTheory.Measure.Trim 124 62341 6.32
Mathlib.MeasureTheory.Measure.Typeclasses 1573 62217 6.34
Mathlib.MeasureTheory.Measure.Restrict 970 60644 6.47
Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving 229 59674 6.56
Mathlib.MeasureTheory.Measure.AbsolutelyContinuous 193 59445 6.58
Mathlib.MeasureTheory.Measure.Map 322 59252 6.60
Mathlib.MeasureTheory.Measure.MeasureSpace 1386 58930 6.62
Mathlib.MeasureTheory.Measure.NullMeasurable 455 57544 6.75
Mathlib.MeasureTheory.Measure.AEDisjoint 137 57089 6.76
Mathlib.MeasureTheory.Measure.MeasureSpaceDef 421 56952 6.77
Mathlib.MeasureTheory.OuterMeasure.Induced 463 56531 6.81
Mathlib.MeasureTheory.OuterMeasure.Caratheodory 240 56068 6.86
Mathlib.MeasureTheory.OuterMeasure.OfFunction 467 55828 6.86
Mathlib.Analysis.SpecificLimits.Basic 702 55361 6.89
Mathlib.Topology.Instances.EReal 453 54659 6.34
Mathlib.Topology.Semicontinuous 1113 54206 6.34
Mathlib.Topology.Instances.ENNReal 1473 53093 6.45
Mathlib.Topology.Instances.NNReal 306 51620 6.51
Mathlib.Topology.Algebra.InfiniteSum.Order 307 51314 5.67
Mathlib.Topology.Algebra.InfiniteSum.NatInt 529 51007 5.31
Mathlib.Topology.Algebra.InfiniteSum.Group 391 50478 5.35
Mathlib.Topology.Algebra.UniformGroup.Defs 540 50087 5.08
Mathlib.Topology.Algebra.Group.Basic 1876 49547 5.09
Mathlib.Topology.Algebra.Monoid 997 47671 4.47
Mathlib.Topology.Algebra.MulAction 298 46674 4.30
Mathlib.Topology.Algebra.ConstMulAction 543 46376 4.30
Mathlib.Topology.Algebra.Constructions 156 45833 4.06
Mathlib.Topology.Homeomorph 1111 45677 4.07
Mathlib.Topology.DenseEmbedding 358 44566 3.83
Mathlib.Topology.Separation.Regular 662 44208 3.86
Mathlib.Topology.Separation.Hausdorff 663 43546 3.88
Mathlib.Topology.Separation.Basic 1116 42883 3.91
Mathlib.Topology.Compactness.LocallyCompact 228 41767 3.87
Mathlib.Topology.Compactness.Compact 1156 41539 3.89
Mathlib.Topology.Bases 997 40383 3.71
Mathlib.Topology.ContinuousOn 1524 39386 3.77
Mathlib.Topology.Constructions 1871 37862 3.88
Mathlib.Topology.Maps.Basic 781 35991 3.79
Mathlib.Topology.Order 894 35210 3.85
Mathlib.Topology.Defs.Induced 147 34316 3.93
Mathlib.Topology.Basic 1768 34169 3.94
Mathlib.Order.Filter.AtTopBot 1335 32401 3.93
Mathlib.Order.Filter.Bases 855 31066 3.92
Mathlib.Order.Filter.Finite 342 30211 4.00
Mathlib.Data.Set.Finite.Lattice 425 29869 3.95
Mathlib.Data.Set.Finite.Powerset 55 29444 3.96
Mathlib.Data.Set.Finite.Basic 986 29389 3.40
Mathlib.Data.Fintype.Card 1167 28403 3.48
Mathlib.Data.Fintype.Basic 1222 27236 3.49
Mathlib.Data.Finset.Image 772 26014 3.51
Mathlib.Data.Finset.Union 236 25242 3.52
Mathlib.Data.Finset.Basic 673 25006 2.87
Mathlib.Data.Finset.SDiff 246 24333 2.85
Mathlib.Data.Finset.Lattice.Lemmas 174 24087 2.86
Mathlib.Data.Finset.Insert 694 23913 2.86
Mathlib.Data.Finset.Empty 229 23219 2.87
Mathlib.Data.Finset.Defs 429 22990 2.89

Anne Baanen (Jan 13 2025 at 11:25):

file LoC cumulative parallelism
Mathlib.Data.Multiset.Nodup 212 22561 2.93
Mathlib.Data.Multiset.Range 65 22349 2.94
Mathlib.Data.Multiset.Basic 2688 22284 2.95
Mathlib.Data.List.Perm.Lattice 107 19596 2.96
Mathlib.Data.List.Nodup 395 19489 2.96
Mathlib.Data.Set.Pairwise.Basic 422 19094 2.80
Mathlib.Data.Set.Function 1725 18672 2.47
Mathlib.Data.Set.Prod 923 16947 2.62
Mathlib.Data.Set.Image 1395 16024 2.71
Mathlib.Data.Set.Subsingleton 318 14629 2.33
Mathlib.Data.Set.Basic 2163 14311 2.36
Mathlib.Order.BooleanAlgebra 805 12148 2.47
Mathlib.Order.Heyting.Basic 1111 11343 2.58
Mathlib.Order.PropInstances 109 10232 2.75
Mathlib.Order.Disjoint 704 10123 2.77
Mathlib.Order.BoundedOrder.Lattice 165 9419 2.90
Mathlib.Order.Lattice 1311 9254 2.87
Mathlib.Order.Monotone.Basic 1142 7943 3.16
Mathlib.Order.RelClasses 817 6801 2.28
Mathlib.Order.Basic 1415 5984 2.36
Mathlib.Tactic.Convert 213 4569 1.78
Mathlib.Tactic.CongrExclamation 747 4356 1.82
Mathlib.Lean.Meta.CongrTheorems 357 3609 1.99
Mathlib.Logic.IsEmpty 222 3252 2.10
Mathlib.Logic.Function.Basic 987 3030 2.12
Mathlib.Logic.Basic 997 2043 1.59
Mathlib.Tactic.Basic 161 1046 2.05
Mathlib.Tactic.PPWithUniv 52 885 2.13
Mathlib.Init 39 833 2.20
Mathlib.Tactic.Linter.Style 431 794 1.00
Mathlib.Tactic.Linter.Header 363 363 1.00
Lean.Elab.Command 0 0 NaN
Lean.Meta.Diagnostics 0 0 NaN
Lean.PrettyPrinter 0 0 NaN
Lean.PrettyPrinter.Delaborator 0 0 NaN
Lean.PrettyPrinter.Delaborator.Options 0 0 NaN
Lean.Data.Options 0 0 NaN
Lean.ImportingFlag 0 0 NaN
Init.System.IO 0 0 NaN
Init.System.IOError 0 0 NaN
Init.Data.ToString.Basic 0 0 NaN
Init.Data.Repr 0 0 NaN
Init.Data.Format.Basic 0 0 NaN
Init.Control.State 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Kim Morrison (Jan 13 2025 at 11:26):

I think splitting each of the Mathlib.Topology.Instances.X files into a Defs and Lemmas would give a big improvement.

Kim Morrison (Jan 13 2025 at 11:28):

lake exe graph --from Mathlib.Data.Set.Basic --to Mathlib.Data.NNRat.Defs
unused0.pdf

is pretty crazy. We really need to get Mathlib.Order.CompleteLatticeIntervals out of Mathlib.Algebra.Order.Ring.Unbundled.Nonneg, it pulls in so much!

Anne Baanen (Jan 13 2025 at 11:29):

Shall I take a look at the importers of Mathlib.Order.CompleteLatticeIntervals then?

Yaël Dillies (Jan 13 2025 at 11:29):

Kim Morrison said:

A longest pole that doesn't go through the development of finiteness! Wow.

It was some hard work :sweat:

Kim Morrison (Jan 13 2025 at 11:30):

Thanks! I think that one actually had contributions from a few people. :-)

Anne Baanen (Jan 13 2025 at 11:33):

Yaël Dillies said:

It was some hard work :sweat:

The work is definitely appreciated, for everyone who contributed!

Yaël Dillies (Jan 13 2025 at 11:37):

Here are a few comments:

  1. Analysis.Seminorm shouldn't be importing normed groups
  2. Topology.Homeomorph is still bonkers. It should be imported in other topology files, rather than importing them
  3. I don't see why MeasureTheory.OuterMeasure.OfFunction needs to import Analysis.SpecificLimits.Basic
  4. MeasureTheory.Measure.QuasiMeasurePreserving seems to be imported to prove results about MeasurableEquiv, which seems a bit overkill

Kim Morrison (Jan 13 2025 at 11:38):

Kim Morrison said:

lake exe graph --from Mathlib.Data.Set.Basic --to Mathlib.Data.NNRat.Defs
unused0.pdf

is pretty crazy. We really need to get Mathlib.Order.CompleteLatticeIntervals out of Mathlib.Algebra.Order.Ring.Unbundled.Nonneg, it pulls in so much!

I'm taking a look at this now. Seems easy, hardest part is naming the split files.

Edward van de Meent (Jan 13 2025 at 11:39):

it's kind of surprising to me that in as long as this topic has existed, it has never been moved to #mathlib4 ...

Kim Morrison (Jan 13 2025 at 11:42):

Edward van de Meent said:

it's kind of surprising to me that in as long as this topic has existed, it has never been moved to #mathlib4 ...

The difficulty is scrolling back to the top!

Notification Bot (Jan 13 2025 at 11:42):

This topic was moved here from #general > The long pole in mathlib by Johan Commelin.

Rémy Degenne (Jan 13 2025 at 11:52):

Yaël Dillies said:

  1. MeasureTheory.Measure.QuasiMeasurePreserving seems to be imported to prove results about MeasurableEquiv, which seems a bit overkill

I split QuasiMeasurePreserving last week from MeasureSpace (and two other new files as well: Map and AbsolutelyContinuous), but I did not try to reduce imports anywhere. So looking at those files might be worth it.

Kim Morrison (Jan 13 2025 at 12:12):

Kim Morrison said:

Kim Morrison said:

lake exe graph --from Mathlib.Data.Set.Basic --to Mathlib.Data.NNRat.Defs
unused0.pdf

is pretty crazy. We really need to get Mathlib.Order.CompleteLatticeIntervals out of Mathlib.Algebra.Order.Ring.Unbundled.Nonneg, it pulls in so much!

I'm taking a look at this now. Seems easy, hardest part is naming the split files.

#20703

It's not amazing, about 40 files with >10 fewer imports. There's probably more to be gained from tweaking the split, but I'd prefer to move on.

Kim Morrison (Jan 13 2025 at 12:15):

unused0.pdf above gets replaced with
after.pdf. Still a lot of grey, but only half as much!

Kim Morrison (Jan 13 2025 at 12:27):

Kim Morrison said:

I think splitting each of the Mathlib.Topology.Instances.X files into a Defs and Lemmas would give a big improvement.

#20707 does the split just for X=Real/EReal/NNReal/ENNReal, and gets pretty massive import reductions. I just kept all the instances (and any theorems needed for the instances) in the Defs file, and everything else in the Lemmas file.

David Loeffler (Jan 13 2025 at 14:27):

Anne Baanen said:

Interesting unused imports:

  • unused1.pdf Basically the same as unused3.pdf from last month: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds imports Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable but then doesn't need anything from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation which has substantial imports.

This could be solved by splitting up JacobiTheta.TwoVariable appropriately; but it probably wouldn't make much of a difference, since the Poisson summation stuff is needed for (indeed, was written specifically to be used by) the next file along the long pole after JacobiTheta.Bounds, namely LSeries.HurwitzZetaEven.

Ruben Van de Velde (Jan 13 2025 at 14:32):

Yeah, I think we had the same conclusion upthread

Anne Baanen (Feb 06 2025 at 15:07):

It's been a while since we've looked at the pole! So have a fresh report:

Analyzing Mathlib at 4a69dc8b998d4bedb9541bc4dd45685be03f5fd5

file instructions cumulative parallelism
Mathlib 12778 6253820 23.85
Mathlib.Analysis.CStarAlgebra.CStarMatrix 117462 6241041 7.78
Mathlib.Analysis.CStarAlgebra.Module.Constructions 75694 6123579 7.90
Mathlib.Analysis.CStarAlgebra.Module.Defs 55114 6047885 7.98
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 188911 5992770 8.04
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 193492 5803858 8.24
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric 164553 5610366 8.42
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 191548 5445812 8.64
Mathlib.Analysis.Normed.Algebra.Spectrum 129121 5254264 8.68
Mathlib.Analysis.Complex.Polynomial.Basic 26134 5125142 8.82
Mathlib.Analysis.Complex.Liouville 17940 5099008 8.21
Mathlib.Analysis.Complex.CauchyIntegral 45818 5081067 8.23
Mathlib.MeasureTheory.Integral.CircleIntegral 66660 5035249 8.12
Mathlib.Analysis.SpecialFunctions.NonIntegrable 16457 4968589 8.22
Mathlib.Analysis.SpecialFunctions.Log.Deriv 43210 4952132 6.69
Mathlib.Analysis.SpecialFunctions.ExpDeriv 34019 4908921 6.70
Mathlib.Analysis.Complex.RealDeriv 27725 4874902 5.86
Mathlib.Analysis.Calculus.ContDiff.Basic 432945 4847177 5.53
Mathlib.Analysis.Calculus.FDeriv.Mul 416961 4414231 5.86
Mathlib.Analysis.Calculus.FDeriv.Analytic 253316 3997270 6.36
Mathlib.Analysis.Analytic.CPolynomial 132059 3743953 6.37
Mathlib.Analysis.Analytic.Constructions 145156 3611893 6.54
Mathlib.Analysis.Analytic.Composition 141210 3466737 6.70
Mathlib.Analysis.Analytic.Basic 251494 3325527 6.93
Mathlib.Analysis.Calculus.FormalMultilinearSeries 74192 3074032 6.94
Mathlib.Analysis.NormedSpace.Multilinear.Curry 208364 2999839 7.09
Mathlib.Analysis.NormedSpace.Multilinear.Basic 275262 2791475 7.54
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 57627 2516212 8.13
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 177214 2458584 8.28
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 77613 2281370 8.85
Mathlib.Topology.Algebra.Module.StrongTopology 87290 2203757 8.64
Mathlib.Topology.Algebra.Module.UniformConvergence 12099 2116466 8.87
Mathlib.Analysis.LocallyConvex.Bounded 36632 2104367 8.89
Mathlib.Analysis.Seminorm 130174 2067734 8.63
Mathlib.Analysis.LocallyConvex.Basic 27256 1937560 9.10
Mathlib.Analysis.Normed.Module.Basic 48158 1910304 8.73
Mathlib.Analysis.Normed.Field.Lemmas 25267 1862145 8.90
Mathlib.Analysis.Normed.Field.Basic 113061 1836877 8.01
Mathlib.Analysis.Normed.Group.Constructions 17894 1723816 7.52
Mathlib.Analysis.Normed.Group.Basic 88099 1705921 7.59
Mathlib.Topology.Instances.ENNReal.Defs 5629 1617821 7.87
Mathlib.Topology.Instances.NNReal.Defs 6425 1612192 7.87
Mathlib.Topology.Instances.Real.Defs 5923 1605766 7.84
Mathlib.Topology.Algebra.Order.Field 29701 1599843 6.87
Mathlib.Topology.Algebra.Field 26696 1570142 6.84
Mathlib.Topology.Algebra.Ring.Basic 18002 1543446 6.72
Mathlib.Topology.Algebra.Group.Basic 90420 1525443 6.59
Mathlib.Topology.Algebra.Monoid 51919 1435022 5.34
Mathlib.Topology.Algebra.MulAction 11250 1383103 5.15
Mathlib.Topology.Algebra.ConstMulAction 30387 1371853 5.16
Mathlib.Topology.Algebra.Constructions 6129 1341466 4.88
Mathlib.Topology.Homeomorph 33862 1335336 4.90
Mathlib.Topology.DenseEmbedding 10521 1301474 4.63
Mathlib.Topology.Separation.Regular 14888 1290953 4.66
Mathlib.Topology.Separation.Hausdorff 15936 1276064 4.68
Mathlib.Topology.Separation.Basic 26575 1260128 4.72
Mathlib.Topology.Compactness.LocallyCompact 6699 1233552 4.67
Mathlib.Topology.Compactness.Compact 32045 1226853 4.69
Mathlib.Topology.Bases 35107 1194807 4.47
Mathlib.Topology.ContinuousOn 38319 1159699 4.57
Mathlib.Topology.Constructions 49130 1121379 4.69
Mathlib.Topology.Maps.Basic 15154 1072249 4.61
Mathlib.Topology.Order 21113 1057095 4.66
Mathlib.Topology.Defs.Induced 3572 1035981 4.74
Mathlib.Topology.Basic 37149 1032408 4.75
Mathlib.Order.Filter.AtTopBot 35579 995259 4.70
Mathlib.Order.Filter.Bases 21488 959679 4.67
Mathlib.Order.Filter.Finite 11102 938191 4.72
Mathlib.Data.Set.Finite.Lattice 15616 927089 4.73
Mathlib.Data.Finite.Sigma 2555 911473 4.69
Mathlib.Data.Fintype.Sigma 16568 908917 4.64
Mathlib.Data.Finset.Sigma 9290 892348 4.60
Mathlib.Data.Finset.Lattice.Fold 54212 883058 4.61
Mathlib.Data.Finset.Prod 12928 828845 4.32
Mathlib.Data.Finset.Card 24281 815917 4.37
Mathlib.Data.Finset.Image 23716 791636 4.48
Mathlib.Data.Finset.Union 10089 767919 4.53
Mathlib.Data.Finset.Basic 17476 757830 3.89
Mathlib.Data.Finset.SDiff 7280 740353 3.89
Mathlib.Data.Finset.Lattice.Lemmas 5270 733073 3.92
Mathlib.Data.Finset.Insert 14564 727802 3.93
Mathlib.Data.Finset.Empty 5090 713237 3.94
Mathlib.Data.Finset.Defs 9166 708147 3.96

Anne Baanen (Feb 06 2025 at 15:07):

file instructions cumulative parallelism
Mathlib.Data.Multiset.Nodup 9346 698980 4.00
Mathlib.Data.Multiset.Range 2938 689634 4.04
Mathlib.Data.Multiset.Basic 66536 686695 4.05
Mathlib.Data.List.Perm.Lattice 4016 620159 4.34
Mathlib.Data.List.Nodup 12131 616142 4.35
Mathlib.Data.Set.Pairwise.Basic 27407 604010 3.71
Mathlib.Data.Set.Function 47569 576603 3.82
Mathlib.Data.Set.Prod 32112 529034 4.07
Mathlib.Data.Set.Image 30740 496922 4.27
Mathlib.Data.Set.Subsingleton 7271 466181 4.42
Mathlib.Data.Set.Basic 62101 458909 4.48
Mathlib.Order.BooleanAlgebra 32941 396808 4.49
Mathlib.Order.Heyting.Basic 39294 363867 4.80
Mathlib.Order.GaloisConnection.Defs 8337 324572 5.25
Mathlib.Order.Hom.Basic 31447 316235 5.37
Mathlib.Order.RelIso.Basic 15240 284787 5.11
Mathlib.Logic.Embedding.Basic 9639 269547 5.05
Mathlib.Logic.Equiv.Basic 39902 259908 5.16
Mathlib.Tactic.CC 5418 220005 1.98
Mathlib.Tactic.CC.Addition 96969 214587 2.00
Mathlib.Tactic.CC.MkProof 23961 117618 2.82
Mathlib.Tactic.CC.Datatypes 12218 93656 2.77
Mathlib.Lean.Meta.CongrTheorems 11054 81438 2.75
Mathlib.Logic.IsEmpty 3487 70384 3.03
Mathlib.Logic.Function.Basic 14194 66896 3.09
Mathlib.Order.Defs.Unbundled 3845 52701 2.50
Mathlib.Tactic.SplitIfs 17907 48856 2.34
Mathlib.Tactic.Core 5516 30948 3.13
Mathlib.Lean.Expr.Basic 9290 25431 3.59
Mathlib.Init 820 16141 4.12
Mathlib.Tactic.Linter.Lint 2185 15320 2.69
Batteries.Tactic.Lint 647 13135 2.39
Batteries.Tactic.Lint.Frontend 9081 12488 1.22
Batteries.Tactic.OpenPrivate 3406 3406 1.00
Lean.Elab.Command 0 0 NaN
Lean.Meta.Diagnostics 0 0 NaN
Lean.PrettyPrinter 0 0 NaN
Lean.PrettyPrinter.Delaborator 0 0 NaN
Lean.PrettyPrinter.Delaborator.Options 0 0 NaN
Lean.Data.Options 0 0 NaN
Lean.ImportingFlag 0 0 NaN
Init.System.IO 0 0 NaN
Init.System.IOError 0 0 NaN
Init.Data.ToString.Basic 0 0 NaN
Init.Data.Repr 0 0 NaN
Init.Data.Format.Basic 0 0 NaN
Init.Control.State 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Anne Baanen (Feb 06 2025 at 15:08):

It looks like the previous work has been undone and we're passing through finiteness again.

Anne Baanen (Feb 06 2025 at 15:13):

Here's an interesting bit of the import graph that I would like to shake: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances depends on Mathlib.Analysis.Normed.Algebra.Spectrum which has a huge amount of grey imports:
unused2.pdf

Anne Baanen (Feb 06 2025 at 17:02):

I managed to shake InnerProductSpace.Basic a bit: #21516. Staring at Mathlib.Analysis.Normed.Algebra.Spectrum did not give me any useful places to split. Maybe someone who knows this corner of mathlib will be more useful.

Kim Morrison (Feb 07 2025 at 09:17):

Anne Baanen said:

It looks like the previous work has been undone and we're passing through finiteness again.

This isn't necessarily a sign of regression. As we shorten the longest pole, we should expect to reach the point where there are multiple poles of similar length, and the report bounces back and forth between them due to small changes.

Kim Morrison (Feb 07 2025 at 09:30):

Anne Baanen said:

Here's an interesting bit of the import graph that I would like to shake: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances depends on Mathlib.Analysis.Normed.Algebra.Spectrum which has a huge amount of grey imports:
unused2.pdf

I had a look a bit too, but am out of time. It does look interesting to refactor this.

Kim Morrison (Feb 07 2025 at 09:31):

@Anne Baanen, could you take a look at set_option linter.upstreamableDecl in Normed.Algebra.Spectrum? It seems to be buggy there.

Anne Baanen (Feb 07 2025 at 09:50):

Kim Morrison said:

Anne Baanen, could you take a look at set_option linter.upstreamableDecl in Normed.Algebra.Spectrum? It seems to be buggy there.

Ok, will take a look right now!

Anne Baanen (Feb 07 2025 at 09:59):

I see the errors like linter Mathlib.Linter.DoubleImports.upstreamableDeclLinter failed: unknown constant 'isClosed'. Or is there also something else I should look for (e.g. missing lints on a declaration that is upstreamable)?

Anne Baanen (Feb 07 2025 at 10:15):

Looks like the error messages are gone in #21505 at least.

Kim Morrison (Feb 07 2025 at 10:58):

Just isClosed etc

Anne Baanen (Mar 03 2025 at 12:41):

Beep! One fresh new semi-automated long pole report:

Analyzing Mathlib at 4c2da682350ad568c6d32d2f9055e42a8c98ffb0

file instructions cumulative parallelism
Mathlib 13410 6210402 25.03
Mathlib.Analysis.CStarAlgebra.CStarMatrix 121103 6196991 8.02
Mathlib.Analysis.CStarAlgebra.Module.Constructions 75119 6075887 8.15
Mathlib.Analysis.CStarAlgebra.Module.Defs 55480 6000768 8.24
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 189726 5945287 8.31
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 173832 5755560 8.53
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric 165594 5581728 8.65
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 193269 5416133 8.89
Mathlib.Analysis.Normed.Algebra.Spectrum 129864 5222864 8.94
Mathlib.Analysis.Complex.Polynomial.Basic 25838 5092999 9.08
Mathlib.Analysis.Complex.Liouville 18112 5067160 8.47
Mathlib.Analysis.Complex.CauchyIntegral 45690 5049048 8.50
Mathlib.MeasureTheory.Integral.CircleIntegral 64640 5003357 8.39
Mathlib.Analysis.SpecialFunctions.NonIntegrable 16706 4938716 8.49
Mathlib.Analysis.SpecialFunctions.Log.Deriv 46443 4922009 6.29
Mathlib.Analysis.SpecialFunctions.ExpDeriv 34392 4875566 6.29
Mathlib.Analysis.Complex.RealDeriv 28144 4841174 6.08
Mathlib.Analysis.Calculus.ContDiff.Operations 189677 4813029 5.79
Mathlib.Analysis.Calculus.ContDiff.Basic 285118 4623351 5.97
Mathlib.Analysis.Calculus.FDeriv.Mul 417669 4338233 6.19
Mathlib.Analysis.Calculus.FDeriv.Analytic 271309 3920563 6.74
Mathlib.Analysis.Analytic.CPolynomial 56070 3649254 6.78
Mathlib.Analysis.Analytic.Constructions 164543 3593184 6.82
Mathlib.Analysis.Analytic.Composition 145784 3428641 7.02
Mathlib.Analysis.Analytic.Basic 289397 3282856 7.28
Mathlib.Analysis.Calculus.FormalMultilinearSeries 68181 2993459 7.39
Mathlib.Analysis.NormedSpace.Multilinear.Curry 208597 2925277 7.54
Mathlib.Analysis.NormedSpace.Multilinear.Basic 277244 2716679 8.03
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 57418 2439435 8.70
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 177453 2382017 8.87
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 77861 2204564 9.50
Mathlib.Topology.Algebra.Module.StrongTopology 81135 2126702 9.27
Mathlib.Topology.Algebra.Module.UniformConvergence 12062 2045566 9.51
Mathlib.Analysis.LocallyConvex.Bounded 36334 2033504 9.54
Mathlib.Analysis.Seminorm 131851 1997169 9.24
Mathlib.Analysis.LocallyConvex.Basic 26909 1865318 9.77
Mathlib.Analysis.Normed.Module.Basic 48794 1838409 9.40
Mathlib.Analysis.Normed.Field.Lemmas 25223 1789614 9.60
Mathlib.Analysis.Normed.Group.Uniform 30001 1764390 8.89
Mathlib.Topology.MetricSpace.Algebra 12111 1734389 8.54
Mathlib.Topology.Algebra.SeparationQuotient.Basic 30197 1722277 7.67
Mathlib.Topology.Algebra.Module.LinearMap 128633 1692079 7.78
Mathlib.Topology.Algebra.UniformGroup.Defs 47591 1563445 6.73
Mathlib.Topology.Algebra.Group.Basic 94177 1515854 6.88
Mathlib.Topology.Algebra.Monoid 52711 1421677 5.68
Mathlib.Topology.Algebra.MulAction 11478 1368965 5.48
Mathlib.Topology.Algebra.ConstMulAction 30768 1357487 5.49
Mathlib.Topology.Algebra.Constructions 6292 1326719 5.21
Mathlib.Topology.Homeomorph 35153 1320427 5.23
Mathlib.Topology.DenseEmbedding 10826 1285273 4.97
Mathlib.Topology.Separation.Regular 15206 1274447 5.00
Mathlib.Topology.Separation.Hausdorff 16326 1259240 5.02
Mathlib.Topology.Separation.Basic 27243 1242914 5.07
Mathlib.Topology.Compactness.LocallyCompact 6878 1215670 5.03
Mathlib.Topology.Compactness.Compact 32575 1208792 5.05
Mathlib.Topology.Bases 36427 1176216 4.81
Mathlib.Topology.ContinuousOn 39450 1139789 4.92
Mathlib.Topology.Constructions 52652 1100338 5.06
Mathlib.Topology.Maps.Basic 15804 1047686 4.99
Mathlib.Topology.Order 21543 1031881 5.05
Mathlib.Topology.Defs.Induced 3698 1010338 5.14
Mathlib.Topology.Basic 38067 1006639 5.16
Mathlib.Order.Filter.AtTopBot.Basic 23087 968572 5.08
Mathlib.Order.Filter.Bases 21974 945484 5.07
Mathlib.Order.Filter.Finite 11333 923510 5.13
Mathlib.Data.Set.Finite.Lattice 17440 912176 5.14
Mathlib.Data.Finite.Sigma 2638 894736 5.11
Mathlib.Data.Fintype.Sigma 15909 892097 4.97
Mathlib.Data.Finset.Sigma 9470 876188 5.02
Mathlib.Data.Finset.Lattice.Fold 43905 866717 4.41
Mathlib.Data.Set.Lattice 83721 822812 3.51
Mathlib.Order.CompleteBooleanAlgebra 41444 739090 3.78
Mathlib.Order.GaloisConnection.Basic 15080 697646 3.95
Mathlib.Order.CompleteLattice 55908 682566 3.99
Mathlib.Order.Hom.Set 8329 626658 4.03
Mathlib.Logic.Equiv.Set 18643 618328 4.04
Mathlib.Data.Set.Function 48599 599685 4.13
Mathlib.Data.Set.Prod 35389 551086 4.40
Mathlib.Data.Set.Image 35805 515697 4.64
Mathlib.Data.Set.Subsingleton 7500 479891 3.94
Mathlib.Data.Set.Insert 18637 472391 3.99
Mathlib.Data.Set.Basic 46878 453753 4.01
Mathlib.Order.BooleanAlgebra 33496 406875 3.91

Anne Baanen (Mar 03 2025 at 12:41):

file instructions cumulative parallelism
Mathlib.Order.Heyting.Basic 39891 373378 4.18
Mathlib.Order.PropInstances 3360 333487 4.53
Mathlib.Order.Disjoint 16338 330126 4.57
Mathlib.Order.BoundedOrder.Lattice 4162 313787 4.75
Mathlib.Order.BoundedOrder.Basic 10149 309624 4.36
Mathlib.Tactic.Finiteness.Attr 1599 299475 2.75
Aesop 1324 297875 2.54
Aesop.Main 7205 296551 2.35
Aesop.Search.Main 106551 289345 2.20
Aesop.Search.ExpandSafePrefix 5909 182793 2.36
Aesop.Search.Expansion 25780 176884 2.39
Aesop.Search.Expansion.Norm 17383 151103 2.55
Aesop.Search.RuleSelection 3557 133720 2.48
Aesop.Search.SearchM 3759 130163 2.50
Aesop.Tree.TreeM 3164 126404 2.53
Aesop.Forward.State.Initial 3140 123239 2.48
Aesop.RuleSet 25247 120099 2.32
Aesop.Index 7756 94851 2.57
Aesop.Forward.Match 8158 87094 2.58
Aesop.Rule 2119 78935 2.27
Aesop.Rule.Basic 1433 76816 2.30
Aesop.RuleTac.Descr 1493 75382 2.33
Aesop.RuleTac.Basic 2531 73888 2.35
Aesop.Forward.Match.Types 2178 71357 1.44
Aesop.Rule.Forward 1580 69178 1.46
Aesop.Forward.RuleInfo 7370 67598 1.45
Aesop.Index.Basic 1824 60227 1.40
Aesop.RulePattern 7845 58403 1.42
Aesop.RPINF 4963 50557 1.48
Aesop.BaseM 1828 45594 1.53
Aesop.Stats.Basic 3475 43766 1.17
Aesop.Tracing 4360 40290 1.15
Aesop.Util.Basic 12357 35930 1.11
Aesop.Util.UnorderedArraySet 1859 23572 1.00
Batteries.Data.Array.Merge 6194 21713 1.00
Batteries.Tactic.Alias 7098 15519 1.00
Batteries.CodeAction.Deprecated 3195 8420 1.00
Batteries.CodeAction.Basic 2802 5224 1.00
Batteries.CodeAction.Attr 2422 2422 1.00
Lean.Server.CodeActions.Basic 0 0 NaN
Lean.Server.FileWorker.RequestHandling 0 0 NaN
Lean.DeclarationRange 0 0 NaN
Lean.Data.DeclarationRange 0 0 NaN
Lean.Data.Position 0 0 NaN
Lean.Data.Format 0 0 NaN
Lean.Data.Options 0 0 NaN
Lean.ImportingFlag 0 0 NaN
Init.System.IO 0 0 NaN
Init.System.IOError 0 0 NaN
Init.Data.ToString.Basic 0 0 NaN
Init.Data.Repr 0 0 NaN
Init.Data.Format.Basic 0 0 NaN
Init.Control.State 0 0 NaN
Init.Control.Basic 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Anne Baanen (Mar 03 2025 at 12:45):

Anne Baanen said:

Here's an interesting bit of the import graph that I would like to shake: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances depends on Mathlib.Analysis.Normed.Algebra.Spectrum which has a huge amount of grey imports:
unused2.pdf

This is still relevant:
unused8.pdf

Anne Baanen (Mar 03 2025 at 12:46):

Another interesting lead: Data.Finite.Sigma has a huge grey clump in its dependency graph:
unused7.pdf

Anne Baanen (Mar 03 2025 at 12:51):

The import graph of Mathlib.Topology.Compactness.LocallyCompact looks somewhat suspicious, perhaps Compactness.Compact can be profitably split:
unused6.pdf
(note: the definition of compactness already lives in Mathlib.Topology.Defs.Filter, unlike what the module docs suggest; see #22501.)

Anne Baanen (Mar 03 2025 at 12:53):

Apart from that, the unused_in_pole report seems mostly to be complaints about meta code not being visibly used in non-meta code.

Anne Baanen (Mar 03 2025 at 12:55):

(Oops, uploaded files from the previous run. Now they should be accurate.)

Anne Baanen (Mar 10 2025 at 09:50):

Beep! One fresh new semi-automated long pole report:

Analyzing Mathlib at 0b9779515e12f6c25d12131a542a45e47a219fe3

file instructions cumulative parallelism
Mathlib 13671 6525800 24.45
Mathlib.Analysis.CStarAlgebra.CStarMatrix 146731 6512129 7.91
Mathlib.Analysis.CStarAlgebra.Module.Constructions 73551 6365398 8.06
Mathlib.Analysis.CStarAlgebra.Module.Defs 65432 6291846 8.14
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 186578 6226414 8.22
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 168885 6039835 8.41
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric 187112 5870950 8.52
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 217550 5683837 8.77
Mathlib.Analysis.Normed.Algebra.Spectrum 137555 5466286 8.82
Mathlib.Analysis.Complex.Polynomial.Basic 25877 5328731 8.96
Mathlib.Analysis.Complex.Liouville 18414 5302854 8.36
Mathlib.Analysis.Complex.CauchyIntegral 48474 5284439 8.38
Mathlib.MeasureTheory.Integral.CircleIntegral 71817 5235964 8.29
Mathlib.Analysis.SpecialFunctions.NonIntegrable 16878 5164146 8.37
Mathlib.Analysis.SpecialFunctions.Log.Deriv 45989 5147267 6.18
Mathlib.Analysis.SpecialFunctions.ExpDeriv 32772 5101278 6.17
Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas 28889 5068505 5.70
Mathlib.Analysis.Calculus.ContDiff.Operations 199791 5039616 5.68
Mathlib.Analysis.Calculus.ContDiff.Basic 296689 4839825 5.85
Mathlib.Analysis.Calculus.FDeriv.Mul 422061 4543135 6.07
Mathlib.Analysis.Calculus.FDeriv.Analytic 279320 4121074 6.58
Mathlib.Analysis.Analytic.CPolynomial 54056 3841754 6.62
Mathlib.Analysis.Analytic.Constructions 177279 3787697 6.65
Mathlib.Analysis.Analytic.Composition 159205 3610417 6.85
Mathlib.Analysis.Analytic.Basic 286592 3451212 7.11
Mathlib.Analysis.Calculus.FormalMultilinearSeries 86417 3164619 7.22
Mathlib.Analysis.NormedSpace.Multilinear.Curry 216079 3078202 7.39
Mathlib.Analysis.NormedSpace.Multilinear.Basic 300703 2862122 7.86
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 56905 2561419 8.54
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 192101 2504514 8.69
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 89872 2312413 9.33
Mathlib.Topology.Algebra.Module.StrongTopology 103559 2222540 9.13
Mathlib.Topology.Algebra.Module.UniformConvergence 14546 2118981 9.43
Mathlib.Analysis.LocallyConvex.Bounded 47748 2104435 9.47
Mathlib.Analysis.Seminorm 171959 2056686 9.20
Mathlib.Analysis.LocallyConvex.Basic 36731 1884726 9.89
Mathlib.Analysis.Normed.Module.Basic 55056 1847995 9.55
Mathlib.Analysis.Normed.Field.Lemmas 16727 1792939 9.77
Mathlib.Analysis.Normed.Ring.Lemmas 13068 1776211 9.55
Mathlib.Analysis.Normed.Group.Uniform 30652 1763143 9.04
Mathlib.Topology.MetricSpace.Algebra 12292 1732491 8.62
Mathlib.Topology.Algebra.SeparationQuotient.Basic 30977 1720198 7.79
Mathlib.Topology.Algebra.Module.LinearMap 143515 1689220 7.91
Mathlib.Topology.Algebra.UniformGroup.Defs 47850 1545704 6.90
Mathlib.Topology.Algebra.Group.Basic 95161 1497854 7.05
Mathlib.Topology.Algebra.Monoid 53238 1402692 5.85
Mathlib.Topology.Algebra.MulAction 11801 1349453 5.64
Mathlib.Topology.Algebra.ConstMulAction 31122 1337652 5.66
Mathlib.Topology.Algebra.Support 13815 1306529 5.37
Mathlib.Topology.Homeomorph 35189 1292714 5.05
Mathlib.Topology.DenseEmbedding 10989 1257524 5.14
Mathlib.Topology.Separation.Regular 15398 1246534 5.18
Mathlib.Topology.Separation.Hausdorff 16533 1231136 5.21
Mathlib.Topology.Separation.Basic 27535 1214602 5.26
Mathlib.Topology.Compactness.LocallyCompact 7013 1187067 5.22
Mathlib.Topology.Compactness.Compact 32838 1180054 5.25
Mathlib.Topology.Bases 36696 1147216 4.99
Mathlib.Topology.ContinuousOn 39862 1110520 5.10
Mathlib.Topology.Constructions 53154 1070657 5.25
Mathlib.Topology.Maps.Basic 16025 1017503 5.13
Mathlib.Topology.Order 21776 1001478 5.20
Mathlib.Topology.Defs.Induced 3821 979702 5.29
Mathlib.Topology.Basic 38415 975881 5.31
Mathlib.Order.Filter.Lift 13880 937465 5.24
Mathlib.Order.Filter.Finite 11480 923585 5.19
Mathlib.Data.Set.Finite.Lattice 17665 912104 5.19
Mathlib.Data.Finite.Sigma 2748 894439 5.16
Mathlib.Data.Fintype.Sigma 16119 891690 5.02
Mathlib.Data.Finset.Sigma 9622 875571 5.07
Mathlib.Data.Finset.Lattice.Fold 44329 865948 4.47
Mathlib.Data.Set.Lattice 84227 821618 3.57
Mathlib.Order.CompleteBooleanAlgebra 41649 737390 3.85
Mathlib.Order.GaloisConnection.Basic 15264 695740 4.02
Mathlib.Order.CompleteLattice 56357 680476 4.06
Mathlib.Order.Hom.Set 9205 624118 4.10
Mathlib.Logic.Equiv.Set 18834 614912 3.90
Mathlib.Data.Set.Function 48886 596077 3.98
Mathlib.Data.Set.Prod 35770 547191 4.24
Mathlib.Data.Set.Image 35361 511420 4.47
Mathlib.Data.Set.Subsingleton 7666 476059 4.03
Mathlib.Data.Set.Insert 18885 468392 4.08
Mathlib.Data.Set.Disjoint 5468 449507 4.10
Mathlib.Data.Set.Basic 34075 444039 4.13

Anne Baanen (Mar 10 2025 at 09:50):

file instructions cumulative parallelism
Mathlib.Order.BooleanAlgebra 33809 409963 3.96
Mathlib.Order.Heyting.Basic 40332 376154 4.23
Mathlib.Order.PropInstances 3483 335821 4.59
Mathlib.Order.Disjoint 16610 332338 4.62
Mathlib.Order.BoundedOrder.Lattice 4297 315728 4.81
Mathlib.Order.BoundedOrder.Basic 10371 311430 4.43
Mathlib.Tactic.Finiteness.Attr 1696 301059 2.81
Aesop 1412 299363 2.59
Aesop.Main 7243 297950 2.40
Aesop.Search.Main 105320 290706 2.26
Aesop.Search.ExpandSafePrefix 5966 185386 2.42
Aesop.Search.Expansion 25751 179420 2.46
Aesop.Search.Expansion.Norm 17393 153669 2.62
Aesop.Search.RuleSelection 3638 136275 2.56
Aesop.Search.SearchM 3837 132636 2.58
Aesop.Tree.TreeM 3249 128798 2.61
Aesop.Forward.State.Initial 3216 125549 2.57
Aesop.RuleSet 25278 122332 2.41
Aesop.Index 7827 97053 2.68
Aesop.Forward.Match 8210 89226 2.70
Aesop.Rule 2209 81015 2.40
Aesop.Rule.Basic 1520 78806 2.44
Aesop.RuleTac.Descr 1580 77285 2.47
Aesop.RuleTac.Basic 2609 75704 2.50
Aesop.Forward.Match.Types 2263 73094 1.61
Aesop.Rule.Forward 1667 70830 1.62
Aesop.Forward.RuleInfo 7413 69163 1.62
Aesop.Index.Basic 1911 61749 1.59
Aesop.RulePattern 7823 59838 1.61
Aesop.RPINF 4931 52015 1.71
Aesop.BaseM 1914 47083 1.78
Aesop.Stats.Basic 3561 45169 1.17
Aesop.Tracing 4416 41607 1.15
Aesop.Util.Basic 12489 37191 1.11
Aesop.Util.UnorderedArraySet 1887 24702 1.00
Batteries.Data.Array.Merge 7296 22815 1.00
Batteries.Tactic.Alias 7085 15518 1.00
Batteries.CodeAction.Deprecated 3175 8433 1.00
Batteries.CodeAction.Basic 2812 5257 1.00
Batteries.CodeAction.Attr 2445 2445 1.00
Lean.Server.CodeActions.Basic 0 0 NaN
Lean.Server.FileWorker.RequestHandling 0 0 NaN
Lean.Server.FileWorker.InlayHints 0 0 NaN
Lean.Server.GoTo 0 0 NaN
Lean.Data.Json.FromToJson 0 0 NaN
Lean.Data.Json.Basic 0 0 NaN
Init.Data.Range 0 0 NaN
Init.Data.Range.Basic 0 0 NaN
Init.Meta 0 0 NaN
Init.MetaTypes 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Anne Baanen (Mar 10 2025 at 09:53):

Anne Baanen said:

Anne Baanen said:

Here's an interesting bit of the import graph that I would like to shake: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances depends on Mathlib.Analysis.Normed.Algebra.Spectrum which has a huge amount of grey imports:
unused2.pdf

This is still relevant:
unused8.pdf

Still there ready for the taking! :)
unused9.pdf

Anne Baanen (Mar 10 2025 at 09:55):

Anne Baanen said:

Another interesting lead: Data.Finite.Sigma has a huge grey clump in its dependency graph:
unused7.pdf

This has improved a bit but only slightly. I've been stumbling across Finset.Image quite a few times in looking at other import graphs, so probably time to do something about that:
unused7.pdf

Anne Baanen (Mar 10 2025 at 09:57):

Anne Baanen said:

The import graph of Mathlib.Topology.Compactness.LocallyCompact looks somewhat suspicious, perhaps Compactness.Compact can be profitably split:
unused6.pdf
(note: the definition of compactness already lives in Mathlib.Topology.Defs.Filter, unlike what the module docs suggest; see #22501.)

No real change either: unused6.pdf

Anne Baanen (Mar 10 2025 at 09:59):

Apart from that, the unused-in-pole script seems to focus on meta code, which import-graph is not too useful in analyzing dependencies of. Should we copy some sort of --exclude-meta logic like we have for lake exe graph?

Anne Baanen (Mar 10 2025 at 10:05):

Anne Baanen said:

Anne Baanen said:

Another interesting lead: Data.Finite.Sigma has a huge grey clump in its dependency graph:
unused7.pdf

This has improved a bit but only slightly. I've been stumbling across Finset.Image quite a few times in looking at other import graphs, so probably time to do something about that:
unused7.pdf

One improvement should be ready in a week: we have a deprecated lemma

@[deprecated filter_mem_eq_inter (since := "2024-09-15")]
theorem filter_mem_image_eq_image (f : α  β) (s : Finset α) (t : Finset β) (h :  x  s, f x  t) :
    (t.filter fun y => y  s.image f) = s.image f := by
  rwa [filter_mem_eq_inter, inter_eq_right, image_subset_iff]

where filter_mem_eq_inter seems to be the only reason to import Data.Finset.Basic. (Of course, we still get a whole bunch of transitive imports since Data.Finset.Image contains lemmas on map and image interacting with basically every other Finset definition...)

Anne Baanen (Mar 18 2025 at 15:10):

docs#Finset.filter_mem_image_eq_image can now be removed, saving 2 whole dependencies across 8 whole files! :) #23054

Anne Baanen (Mar 18 2025 at 17:26):

split Order/CompleteLattice.lean: #23064

Anne Baanen (Mar 28 2025 at 09:20):

Beep! One semi-regular semi-automated semi-accurate analysis of the longest pole.

file instructions cumulative parallelism
Mathlib 13958 6607330 24.69
Mathlib.Analysis.CStarAlgebra.CStarMatrix 148206 6593371 7.95
Mathlib.Analysis.CStarAlgebra.Module.Constructions 71622 6445165 8.10
Mathlib.Analysis.CStarAlgebra.Module.Defs 66116 6373543 8.18
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 183001 6307426 8.25
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 170097 6124424 8.45
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric 188346 5954326 8.56
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 219767 5765980 8.80
Mathlib.Analysis.Normed.Algebra.Spectrum 139412 5546213 8.86
Mathlib.Analysis.Complex.Polynomial.Basic 26167 5406801 9.01
Mathlib.Analysis.Complex.Liouville 19315 5380634 8.41
Mathlib.Analysis.Complex.CauchyIntegral 48895 5361318 8.43
Mathlib.MeasureTheory.Integral.CircleIntegral 69557 5312422 8.34
Mathlib.Analysis.SpecialFunctions.NonIntegrable 17083 5242865 8.41
Mathlib.Analysis.SpecialFunctions.Log.Deriv 46489 5225782 6.18
Mathlib.Analysis.SpecialFunctions.ExpDeriv 33131 5179292 6.17
Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas 29161 5146160 5.69
Mathlib.Analysis.Calculus.ContDiff.Operations 202609 5116999 5.66
Mathlib.Analysis.Calculus.ContDiff.Basic 301021 4914390 5.83
Mathlib.Analysis.Calculus.FDeriv.Mul 424529 4613368 6.05
Mathlib.Analysis.Calculus.FDeriv.Analytic 280630 4188839 6.55
Mathlib.Analysis.Analytic.CPolynomial 54850 3908209 6.59
Mathlib.Analysis.Analytic.Constructions 193910 3853358 6.67
Mathlib.Analysis.Analytic.Linear 51750 3659448 6.86
Mathlib.Analysis.Analytic.CPolynomialDef 106604 3607697 6.94
Mathlib.Analysis.Analytic.ChangeOrigin 105908 3501092 7.12
Mathlib.Analysis.Analytic.Basic 288787 3395184 7.32
Mathlib.Analysis.Calculus.FormalMultilinearSeries 86010 3106396 7.38
Mathlib.Analysis.NormedSpace.Multilinear.Curry 215851 3020386 7.56
Mathlib.Analysis.NormedSpace.Multilinear.Basic 286805 2804534 8.05
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 55343 2517729 8.76
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 190919 2462385 8.91
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 87727 2271466 9.58
Mathlib.Topology.Algebra.Module.StrongTopology 102385 2183738 9.33
Mathlib.Topology.Algebra.Module.UniformConvergence 14453 2081353 9.23
Mathlib.Analysis.LocallyConvex.Bounded 47169 2066899 9.27
Mathlib.Analysis.Seminorm 166697 2019730 9.34
Mathlib.Analysis.LocallyConvex.Basic 35857 1853032 10.04
Mathlib.Analysis.Normed.Module.Basic 55756 1817175 9.61
Mathlib.Analysis.Normed.Field.Lemmas 16560 1761419 9.83
Mathlib.Analysis.Normed.Ring.Lemmas 13371 1744859 9.57
Mathlib.Analysis.Normed.Group.Uniform 31149 1731487 9.34
Mathlib.Topology.MetricSpace.Algebra 12453 1700338 8.93
Mathlib.Topology.Algebra.SeparationQuotient.Basic 31274 1687885 8.05
Mathlib.Topology.Algebra.Module.LinearMap 144954 1656610 8.19
Mathlib.Topology.Algebra.Module.Basic 20299 1511656 8.41
Mathlib.Topology.Algebra.Group.Quotient 8608 1491356 7.42
Mathlib.Topology.Algebra.Group.Pointwise 28820 1482748 7.25
Mathlib.Topology.Algebra.Group.Basic 60927 1453927 7.37
Mathlib.Topology.Algebra.Monoid 50348 1393000 6.00
Mathlib.Topology.Algebra.MulAction 11921 1342651 5.79
Mathlib.Topology.Algebra.ConstMulAction 31458 1330729 5.81
Mathlib.Topology.Algebra.Constructions 6381 1299271 5.14
Mathlib.Topology.Homeomorph.Lemmas 17086 1292889 5.16
Mathlib.Topology.DenseEmbedding 11126 1275803 5.21
Mathlib.Topology.Separation.Regular 15565 1264676 5.24
Mathlib.Topology.Separation.Hausdorff 17361 1249111 5.27
Mathlib.Topology.Separation.Basic 27866 1231750 5.32
Mathlib.Topology.Compactness.LocallyCompact 7106 1203884 5.28
Mathlib.Topology.Compactness.Compact 34680 1196777 5.30
Mathlib.Topology.Bases 37091 1162096 5.05
Mathlib.Topology.ContinuousOn 36492 1125004 5.16
Mathlib.Topology.Constructions 32475 1088512 5.30
Mathlib.Topology.Constructions.SumProd 33841 1056036 5.10
Mathlib.Topology.Homeomorph.Defs 11882 1022195 5.24
Mathlib.Topology.Maps.Basic 16227 1010312 5.29
Mathlib.Topology.Order 22007 994085 5.36
Mathlib.Topology.Defs.Induced 3863 972077 5.45
Mathlib.Topology.Basic 39589 968214 5.47
Mathlib.Order.Filter.Lift 14019 928625 5.41
Mathlib.Order.Filter.Finite 11588 914605 5.36
Mathlib.Data.Set.Finite.Lattice 17865 903017 5.37
Mathlib.Data.Finite.Sigma 2777 885151 5.34
Mathlib.Data.Fintype.Sigma 16322 882374 5.19
Mathlib.Data.Finset.Sigma 9714 866052 5.25
Mathlib.Data.Finset.Lattice.Fold 46645 856337 4.77
Mathlib.Data.Finset.Sum 12184 809691 4.39
Mathlib.Data.Finset.Card 25156 797507 4.20
Mathlib.Data.Finset.Image 21698 772351 4.27
Mathlib.Data.Finset.SymmDiff 3015 750653 4.25
Mathlib.Data.Finset.SDiff 7771 747637 4.26
Mathlib.Data.Finset.Lattice.Lemmas 5610 739866 4.29
Mathlib.Data.Finset.Insert 15397 734256 4.31
Mathlib.Data.Multiset.FinsetOps 8653 718858 4.34

...

Anne Baanen (Mar 28 2025 at 09:20):

file instructions cumulative parallelism
Mathlib.Data.Multiset.Dedup 4747 710204 4.36
Mathlib.Data.Multiset.UnionInter 16310 705457 4.37
Mathlib.Data.Multiset.Filter 12552 689146 4.42
Mathlib.Data.Multiset.MapFold 14134 676594 4.39
Mathlib.Data.Multiset.Replicate 5214 662459 4.44
Mathlib.Data.Multiset.AddSub 13406 657245 4.46
Mathlib.Data.Multiset.Count 7738 643839 4.53
Mathlib.Data.List.Nodup 12657 636100 4.54
Mathlib.Data.Set.Pairwise.Basic 28704 623443 3.87
Mathlib.Data.Set.Function 32692 594738 4.00
Mathlib.Data.Set.Prod 42709 562046 4.17
Mathlib.Data.Set.Image 37289 519337 4.43
Mathlib.Data.Set.Subsingleton 7757 482047 4.02
Mathlib.Data.Set.Insert 21553 474289 4.07
Mathlib.Data.Set.Disjoint 5654 452736 4.10
Mathlib.Data.Set.Basic 35263 447081 4.14
Mathlib.Order.BooleanAlgebra 34275 411818 3.97
Mathlib.Order.Heyting.Basic 41063 377543 4.24
Mathlib.Order.PropInstances 3514 336479 4.61
Mathlib.Order.Disjoint 16857 332964 4.64
Mathlib.Order.BoundedOrder.Lattice 4348 316107 4.84
Mathlib.Order.BoundedOrder.Basic 10702 311758 4.45
Mathlib.Tactic.Finiteness.Attr 1705 301056 2.82
Aesop 1412 299350 2.59
Aesop.Main 7244 297937 2.40
Aesop.Search.Main 105318 290693 2.26
Aesop.Search.ExpandSafePrefix 5966 185374 2.42
Aesop.Search.Expansion 25748 179408 2.46
Aesop.Search.Expansion.Norm 17385 153659 2.62
Aesop.Search.RuleSelection 3640 136274 2.54
Aesop.Search.SearchM 3837 132633 2.57
Aesop.Tree.TreeM 3248 128796 2.60
Aesop.Forward.State.Initial 3216 125547 2.55
Aesop.RuleSet 25279 122330 2.40
Aesop.Index 7827 97051 2.66
Aesop.Forward.Match 8210 89223 2.67
Aesop.Rule 2209 81012 2.38
Aesop.Rule.Basic 1520 78803 2.41
Aesop.RuleTac.Descr 1580 77282 2.44
Aesop.RuleTac.Basic 2609 75702 2.47
Aesop.Forward.Match.Types 2263 73092 1.58
Aesop.Rule.Forward 1666 70828 1.60
Aesop.Forward.RuleInfo 7412 69161 1.59
Aesop.Index.Basic 1911 61749 1.59
Aesop.RulePattern 7820 59838 1.61
Aesop.RPINF 4932 52017 1.71
Aesop.BaseM 1914 47084 1.78
Aesop.Stats.Basic 3561 45169 1.17
Aesop.Tracing 4416 41608 1.15
Aesop.Util.Basic 12490 37192 1.11
Aesop.Util.UnorderedArraySet 1887 24702 1.00
Batteries.Data.Array.Merge 7296 22814 1.00
Batteries.Tactic.Alias 7084 15518 1.00
Batteries.CodeAction.Deprecated 3174 8433 1.00
Batteries.CodeAction.Basic 2812 5258 1.00
Batteries.CodeAction.Attr 2445 2445 1.00
Lean.Server.CodeActions.Basic 0 0 NaN
Lean.Server.FileWorker.RequestHandling 0 0 NaN
Lean.Server.FileWorker.InlayHints 0 0 NaN
Lean.Server.GoTo 0 0 NaN
Lean.Data.Json.FromToJson 0 0 NaN
Lean.Data.Json.Basic 0 0 NaN
Init.Data.Range 0 0 NaN
Init.Data.Range.Basic 0 0 NaN
Init.Meta 0 0 NaN
Init.MetaTypes 0 0 NaN
Init.Core 0 0 NaN
Init.Prelude 0 0 NaN

Anne Baanen (Mar 28 2025 at 09:28):

Anne Baanen said:

Anne Baanen said:

The import graph of Mathlib.Topology.Compactness.LocallyCompact looks somewhat suspicious, perhaps Compactness.Compact can be profitably split:
unused6.pdf
(note: the definition of compactness already lives in Mathlib.Topology.Defs.Filter, unlike what the module docs suggest; see #22501.)

No real change either: unused6.pdf

This looks a bit different now, I think we can still make some profit here: unused4.pdf

Anne Baanen (Mar 28 2025 at 09:30):

We have Mathlib.Topology.Homeomorph.Defs and Mathlib.Topology.Maps.Basic both importing finiteness via Mathlib.Order.Filter.Lift -> Mathlib.Topology.Basic which they do not need at all: unused6.pdf
unused9.pdf

Anne Baanen (Mar 28 2025 at 09:31):

Mathlib.Data.Multiset.Count imports Mathlib.Data.List.Nodup which has basically entirely gray dependencies. unused7.pdf

Patrick Massot (Mar 28 2025 at 09:39):

I’ll take a look at the filter question.

Anne Baanen (Mar 28 2025 at 09:40):

I also noticed that no file on the pole depends on Mathlib.Data.Finset.SymmDiff except for the file that imports it, Mathlib.Data.Finset.Image. We can probably profitably reverse the order of that dependency.

Anne Baanen (Mar 28 2025 at 09:41):

I'll take a look at the Mathlib.Data.List.Nodup -> Mathlib.Data.Multiset.Count import too.

Patrick Massot (Mar 28 2025 at 09:46):

However I’m not sure what those graphs say.

Patrick Massot (Mar 28 2025 at 09:47):

The unused6 graphs suggests finiteness isn’t really needed. But the next node after Filter.Lift is Topology.Basic which definitely uses finiteness a lot.

Patrick Massot (Mar 28 2025 at 09:47):

grep says Finite appears 19 times in that file.

Patrick Massot (Mar 28 2025 at 09:47):

So what do we gain if I kick finiteness out of Filter.Lift?

Patrick Massot (Mar 28 2025 at 09:48):

Do we simply gain one import in one file?

Ruben Van de Velde (Mar 28 2025 at 09:50):

No, the graph shows that Mathlib.Topology.Compactness.LocallyCompact imports Mathlib.Topology.Basic imports Mathlib.Order.Filter.Lift, but Mathlib.Topology.Compactness.LocallyCompact doesn't actually use anything from Mathlib.Order.Filter.Lift

Patrick Massot (Mar 28 2025 at 09:52):

I don’t see LocallyCompact anywhere

Patrick Massot (Mar 28 2025 at 09:52):

Which graph are you looking at?

Ruben Van de Velde (Mar 28 2025 at 10:09):

unused4.pdf

Anne Baanen (Mar 28 2025 at 11:02):

Anne Baanen said:

I also noticed that no file on the pole depends on Mathlib.Data.Finset.SymmDiff except for the file that imports it, Mathlib.Data.Finset.Image. We can probably profitably reverse the order of that dependency.

#23398. Not a huge difference if we go further downstream, but it does clean up 62 files.

Eric Wieser (Mar 28 2025 at 11:57):

This is only a file with 5 theorems; if this is important to get off the longest pole, perhaps we should be focusing on minimizing the per-file import overhead?

Anne Baanen (Mar 28 2025 at 12:06):

To be honest, I don't think the pole is an overwhelming argument here. I have been annoyed for a while at Finset.Image being a big node in the import graph that everything to do with finiteness seems to need to pass through.

Anne Baanen (Mar 28 2025 at 16:56):

Anne Baanen said:

I also noticed that no file on the pole depends on Mathlib.Data.Finset.SymmDiff except for the file that imports it, Mathlib.Data.Finset.Image. We can probably profitably reverse the order of that dependency.

Reversing the dependency order didn't work, so let's just split: #23407.

Patrick Massot (Mar 28 2025 at 21:56):

@Anne Baanen I opened #23411 about the finiteness in filters stuff. With major help by Anatole, I was able to remove some finiteness at the cost of having more complicated proofs. I don’t know if it’s worth the trouble. Feel free to discard or redo.

Johan Commelin (Apr 08 2025 at 10:04):

I just noticed:

$ lake exe pole
⚠ [72/76] Built LongestPole.Main
warning: ././././LongestPole/Main.lean:137:20: `compile_time_search_path%` is deprecated; use `initSearchPath (← findSysroot)` instead.

Trying to simply perform that fix didn't work.

Johan Commelin (Apr 08 2025 at 11:40):

I've fixed other deprecations in

chore(LongestPole): fix some deprecations and a shebang line #23824

Johan Commelin (Apr 08 2025 at 11:41):

If someone knows how to fix the remaining one, please push to this branch

Ruben Van de Velde (Apr 09 2025 at 19:46):

Number of files in the pole isn't the most relevant statistic, but still: #23861 drops it by ten

Johan Commelin (Apr 26 2025 at 09:59):

Update of the long pole:

file instructions cumulative parallelism
Mathlib 13337 6235246 25.50
Mathlib.Analysis.CStarAlgebra.CStarMatrix 139498 6221909 8.16
Mathlib.Analysis.CStarAlgebra.Module.Constructions 62101 6082411 8.31
Mathlib.Analysis.CStarAlgebra.Module.Defs 63206 6020310 8.39
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 170094 5957103 8.46
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic 172217 5787009 8.65
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric 178360 5614791 8.78
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 215452 5436431 9.03
Mathlib.Analysis.Normed.Algebra.Spectrum 126471 5220978 9.12
Mathlib.Analysis.Complex.Polynomial.Basic 26234 5094506 9.27
Mathlib.Analysis.Complex.Liouville 18066 5068272 8.66
Mathlib.Analysis.Complex.CauchyIntegral 53123 5050205 8.69
Mathlib.MeasureTheory.Integral.CircleIntegral 67489 4997082 8.60
Mathlib.Analysis.SpecialFunctions.NonIntegrable 16761 4929593 8.68
Mathlib.Analysis.SpecialFunctions.Log.Deriv 46034 4912831 6.37
Mathlib.Analysis.SpecialFunctions.ExpDeriv 33536 4866797 6.37
Mathlib.Analysis.Complex.RealDeriv 29129 4833260 6.18
Mathlib.Analysis.Calculus.ContDiff.Operations 191050 4804130 5.88
Mathlib.Analysis.Calculus.ContDiff.Basic 294922 4613080 6.06
Mathlib.Analysis.Calculus.FDeriv.Mul 425206 4318158 6.30
Mathlib.Analysis.Calculus.FDeriv.Analytic 283467 3892951 6.87
Mathlib.Analysis.Analytic.CPolynomial 52612 3609484 6.93
Mathlib.Analysis.Analytic.Constructions 187541 3556871 7.02
Mathlib.Analysis.Analytic.Linear 51126 3369330 7.24
Mathlib.Analysis.Analytic.CPolynomialDef 105287 3318203 7.34
Mathlib.Analysis.Analytic.ChangeOrigin 108299 3212915 7.54
Mathlib.Analysis.Analytic.Basic 272134 3104615 7.77
Mathlib.Analysis.Calculus.FormalMultilinearSeries 79434 2832480 7.87
Mathlib.Analysis.NormedSpace.Multilinear.Curry 220088 2753046 8.07
Mathlib.Analysis.NormedSpace.Multilinear.Basic 272799 2532957 8.67
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace 51383 2260158 9.49
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear 172928 2208774 9.67
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic 73313 2035845 10.41
Mathlib.Topology.Algebra.Module.StrongTopology 85599 1962532 10.13
Mathlib.Topology.Algebra.Module.UniformConvergence 13549 1876932 10.02
Mathlib.Analysis.LocallyConvex.Bounded 41977 1863382 10.06
Mathlib.Analysis.Seminorm 142067 1821404 10.15
Mathlib.Analysis.LocallyConvex.Basic 32629 1679336 10.87
Mathlib.Analysis.Normed.Module.Basic 50632 1646707 10.39
Mathlib.Analysis.Normed.Field.Lemmas 14565 1596074 10.63
Mathlib.Analysis.Normed.Ring.Lemmas 20950 1581508 10.65
Mathlib.Analysis.Normed.Group.Uniform 29353 1560558 10.14
Mathlib.Topology.MetricSpace.Algebra 12094 1531205 9.78
Mathlib.Topology.Algebra.SeparationQuotient.Basic 27106 1519110 8.90
Mathlib.Topology.Algebra.Module.LinearMap 112798 1492003 9.04
Mathlib.Topology.Algebra.Module.Basic 17272 1379205 9.23
Mathlib.Topology.Algebra.Group.Quotient 7803 1361933 8.13
Mathlib.Topology.Algebra.Group.Pointwise 25536 1354129 7.95
Mathlib.Topology.Algebra.Group.Basic 55936 1328592 8.08
Mathlib.Topology.Algebra.Monoid 45150 1272656 6.57
Mathlib.Topology.Algebra.MulAction 11939 1227506 6.34
Mathlib.Topology.Algebra.ConstMulAction 31746 1215567 6.34
Mathlib.Topology.Algebra.Support 13641 1183820 6.03
Mathlib.Topology.Separation.Hausdorff 16887 1170179 5.66
Mathlib.Topology.Separation.Basic 26350 1153291 5.70
Mathlib.Topology.Compactness.LocallyCompact 7103 1126940 5.60
Mathlib.Topology.Compactness.Compact 31087 1119837 5.63
Mathlib.Topology.ContinuousOn 34501 1088750 5.45
Mathlib.Topology.Constructions 30851 1054248 5.60
Mathlib.Topology.Constructions.SumProd 32623 1023397 5.38
Mathlib.Topology.Homeomorph.Defs 11952 990773 5.53
Mathlib.Topology.Maps.Basic 14494 978821 5.58
Mathlib.Topology.Order 20737 964327 5.65
Mathlib.Topology.Continuous 7663 943589 5.74
Mathlib.Topology.ClusterPt 10200 935926 5.78
Mathlib.Topology.Neighborhoods 10733 925725 5.84
Mathlib.Topology.Closure 13374 914992 5.75

Johan Commelin (Apr 26 2025 at 09:59):

continued:

file instructions cumulative parallelism
Mathlib.Order.Filter.Lift 14099 901618 5.59
Mathlib.Order.Filter.Finite 12197 887518 5.55
Mathlib.Data.Set.Finite.Lattice 17628 875320 5.56
Mathlib.Data.Finite.Sigma 3049 857692 5.54
Mathlib.Data.Fintype.Sigma 17341 854643 5.34
Mathlib.Data.Finset.Sigma 10159 837302 5.40
Mathlib.Order.CompleteLattice.Finset 8947 827142 5.27
Mathlib.Data.Set.Lattice.Image 42259 818194 3.61
Mathlib.Data.Set.Lattice 37633 775935 3.75
Mathlib.Data.Set.BooleanAlgebra 3690 738301 3.89
Mathlib.Order.CompleteBooleanAlgebra 42216 734610 3.90
Mathlib.Order.GaloisConnection.Basic 16418 692393 4.06
Mathlib.Order.CompleteLattice.Basic 38338 675975 4.01
Mathlib.Order.Hom.Set 9649 637637 4.01
Mathlib.Logic.Equiv.Set 19393 627987 3.94
Mathlib.Data.Set.Function 30604 608594 4.03
Mathlib.Data.Set.Prod 41473 577989 4.17
Mathlib.Data.Set.Image 35132 536516 4.42
Mathlib.Data.Set.Subsingleton 8026 501383 4.10
Mathlib.Data.Set.Insert 20921 493356 4.15
Mathlib.Data.Set.Disjoint 6145 472434 4.17
Mathlib.Data.Set.Basic 32488 466289 4.21
Mathlib.Order.BooleanAlgebra 35850 433801 4.26
Mathlib.Order.Heyting.Basic 41640 397951 4.55
Mathlib.Order.PropInstances 3640 356310 4.94
Mathlib.Order.Disjoint 15980 352670 4.98
Mathlib.Order.BoundedOrder.Lattice 4604 336690 5.17
Mathlib.Order.BoundedOrder.Basic 9748 332085 4.81
Mathlib.Tactic.Finiteness.Attr 2041 322337 2.88

Johan Commelin (Apr 26 2025 at 10:04):

The two most interesting graphs produced by ./scripts/unused_in_pole.sh are:

Yaël Dillies (Apr 26 2025 at 10:10):

I disagree that they are interesting. There's really not much left to be gained from splitting finiteness files further

Kevin Buzzard (Apr 26 2025 at 10:12):

Number theory off the hook! Clearly we need to try harder!

Johan Commelin (Apr 26 2025 at 13:59):

Yaël Dillies said:

I disagree that they are interesting. There's really not much left to be gained from splitting finiteness files further

I'll not share the other 8 PDFs... They are even less interesting :grinning:


Last updated: May 02 2025 at 03:31 UTC