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 banningimport 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
andalias
- 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
inMathlib.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 be prime and an integer such that "... :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
importingMathlib.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):
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.IntegralClosure
→ Mathlib.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.Operations
→ LinearAlgebra.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 suspiciousYeah, 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 suspiciousYeah, I'm looking into this one.
theorem factors_count_eq {n p : ℕ} : n.factors.count p = n.factorization p
goes through UFDshttps://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:
- Merge this PR into the one you want to measure.
- Run
!bench
in GitHub so speed.lean-fro.org benchmarks it. - 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.Operations
→LinearAlgebra.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 importAlgebra.Module.Submodule.Basic
. Is that the case after #12105 ?
There's still other paths too;
Mathlib.Algebra.Group.UniqueProds
→Mathlib.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
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 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 x
s 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 ofx
s 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):
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 '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.UnusedTransitiveImport
s 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
importsMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
but then doesn't need anything fromMathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
which has substantial imports. -
unused4.pdf
Mathlib.Topology.Homeomorph
has many imports which are not needed by many downstream users ofHomeomorph
. -
unused5.pdf
The chain fromMathlib.Topology.ContinuousOn
toMathlib.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
importsMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
but then doesn't need anything fromMathlib.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 someMulAction
dependencies. - unused5.pdf:
Mathlib.Topology.Semicontinuous
depends onMathlib.Topology.Instances.ENNReal
andMathlib.Topology.Instances.NNReal
which in turn import a lot thatSemicontinous
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:
Analysis.Seminorm
shouldn't be importing normed groupsTopology.Homeomorph
is still bonkers. It should be imported in other topology files, rather than importing them- I don't see why
MeasureTheory.OuterMeasure.OfFunction
needs to importAnalysis.SpecificLimits.Basic
MeasureTheory.Measure.QuasiMeasurePreserving
seems to be imported to prove results aboutMeasurableEquiv
, 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.pdfis pretty crazy. We really need to get
Mathlib.Order.CompleteLatticeIntervals
out ofMathlib.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:
MeasureTheory.Measure.QuasiMeasurePreserving
seems to be imported to prove results aboutMeasurableEquiv
, 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.pdfis pretty crazy. We really need to get
Mathlib.Order.CompleteLatticeIntervals
out ofMathlib.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.
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 aDefs
andLemmas
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
importsMathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
but then doesn't need anything fromMathlib.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 onMathlib.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 onMathlib.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 onMathlib.Analysis.Normed.Algebra.Spectrum
which has a huge amount of grey imports:
unused2.pdfThis 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, perhapsCompactness.Compact
can be profitably split:
unused6.pdf
(note: the definition of compactness already lives inMathlib.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.pdfThis 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, perhapsCompactness.Compact
can be profitably split:
unused6.pdf
(note: the definition of compactness already lives inMathlib.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):
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