Zulip Chat Archive
Stream: mathlib4
Topic: long files
Johan Commelin (Jan 29 2025 at 10:44):
Algebra
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:set_option linter.style.longFile 1800
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean:set_option linter.style.longFile 2000
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Algebra/MonoidAlgebra/Defs.lean:set_option linter.style.longFile 1700
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean:set_option linter.style.longFile 2000
AlgebraicGeometry
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean:set_option linter.style.longFile 1700
Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean:set_option linter.style.longFile 2100
Analysis
Mathlib/Analysis/Calculus/ContDiff/Basic.lean:set_option linter.style.longFile 2200
Mathlib/Analysis/Normed/Group/Basic.lean:set_option linter.style.longFile 1700
CategoryTheory
Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:set_option linter.style.longFile 2100
Computability
Mathlib/Computability/TMToPartrec.lean:set_option linter.style.longFile 2100
Mathlib/Computability/TuringMachine.lean:set_option linter.style.longFile 2100
Data
Mathlib/Data/Finsupp/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Data/List/Basic.lean:set_option linter.style.longFile 2200
Mathlib/Data/Multiset/Basic.lean:set_option linter.style.longFile 2800
Mathlib/Data/Num/Lemmas.lean:set_option linter.style.longFile 1700
Mathlib/Data/Ordmap/Ordset.lean:set_option linter.style.longFile 1700
Mathlib/Data/Real/EReal.lean:set_option linter.style.longFile 2200
Mathlib/Data/Seq/WSeq.lean:set_option linter.style.longFile 1800
Mathlib/Data/Set/Basic.lean:set_option linter.style.longFile 2300
Mathlib/Data/Set/Function.lean:set_option linter.style.longFile 1800
Mathlib/Data/Set/Lattice.lean:set_option linter.style.longFile 2100
Mathlib/Data/ZMod/Basic.lean:set_option linter.style.longFile 1700
Geometry
Mathlib/Geometry/Manifold/IsManifold.lean:set_option linter.style.longFile 1900
LinearAlgebra
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean:set_option linter.style.longFile 1800
Mathlib/LinearAlgebra/Dual.lean:set_option linter.style.longFile 2100
Mathlib/LinearAlgebra/LinearIndependent.lean:set_option linter.style.longFile 1700
Mathlib/LinearAlgebra/Multilinear/Basic.lean:set_option linter.style.longFile 1900
Mathlib/LinearAlgebra/TensorProduct/Basic.lean:set_option linter.style.longFile 1700
Logic
Mathlib/Logic/Equiv/Basic.lean:set_option linter.style.longFile 2000
MeasureTheory
Mathlib/MeasureTheory/Function/L1Space.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Function/LpSpace.lean:set_option linter.style.longFile 1900
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean:set_option linter.style.longFile 2000
Mathlib/MeasureTheory/Integral/Bochner.lean:set_option linter.style.longFile 2100
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/Lebesgue.lean:set_option linter.style.longFile 2200
Mathlib/MeasureTheory/Integral/SetIntegral.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/SetToL1.lean:set_option linter.style.longFile 1800
Mathlib/MeasureTheory/Measure/Typeclasses.lean:set_option linter.style.longFile 1700
Order
Mathlib/Order/CompleteLattice.lean:set_option linter.style.longFile 1900
Mathlib/Order/Filter/Basic.lean:set_option linter.style.longFile 2200
Mathlib/Order/Hom/Lattice.lean:set_option linter.style.longFile 1800
Mathlib/Order/Interval/Set/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Order/LiminfLimsup.lean:set_option linter.style.longFile 1900
Mathlib/Order/UpperLower/Basic.lean:set_option linter.style.longFile 1900
SetTheory
Mathlib/SetTheory/Cardinal/Basic.lean:set_option linter.style.longFile 2300
Mathlib/SetTheory/Game/PGame.lean:set_option linter.style.longFile 2300
Mathlib/SetTheory/Ordinal/Arithmetic.lean:set_option linter.style.longFile 2600
Mathlib/SetTheory/ZFC/Basic.lean:set_option linter.style.longFile 1700
Topology
Mathlib/Topology/Algebra/Group/Basic.lean:set_option linter.style.longFile 1900
Mathlib/Topology/Basic.lean:set_option linter.style.longFile 1900
Mathlib/Topology/Category/Profinite/Nobeling.lean:set_option linter.style.longFile 2000
Mathlib/Topology/Constructions.lean:set_option linter.style.longFile 1900
Mathlib/Topology/ContinuousOn.lean:set_option linter.style.longFile 1700
Mathlib/Topology/UniformSpace/Basic.lean:set_option linter.style.longFile 1900
Johan Commelin (Jan 29 2025 at 10:44):
If you have some mathlib expertise in one of these areas, please help splitting these files!
Johan Commelin (Jan 29 2025 at 11:13):
#21215 takes care of LinearAlgebra/Multilinear/Basic
Michael Rothgang (Jan 29 2025 at 12:00):
I can take care of Geometry/Manifold/IsManifold.lean
Johan Commelin (Jan 29 2025 at 15:13):
#21224 takes care of LinearAlgebra/TensorProduct/Basic
Michael Rothgang (Jan 29 2025 at 15:37):
#21219 splits IsManifold/Basic.lean in two smaller files
Bolton Bailey (Jan 29 2025 at 17:09):
#21230 splits Data/Finsupp/Basic.lean
Etienne Marion (Jan 29 2025 at 17:40):
#21231 for MeasureTheory/Function/L1Space
Bolton Bailey (Jan 29 2025 at 17:58):
#21232 for Data/List/Basic
Violeta Hernández (Jan 29 2025 at 20:51):
All the set theory ones are pretty complicated to split as they're embroiled in current refactors... Except for the ZFC file. I'm not sure what's the division that makes the most sense though. I could put classes in their own file, or put PSet and ZFSet in separate files, or both.
Etienne Marion (Jan 30 2025 at 19:38):
#21273 for MeasureTheory/Function/StronglyMeasurable/Basic
Kim Morrison (Jan 30 2025 at 21:17):
Violeta Hernández said:
All the set theory ones are pretty complicated to split as they're embroiled in current refactors... Except for the ZFC file. I'm not sure what's the division that makes the most sense though. I could put classes in their own file, or put
PSetandZFSetin separate files, or both.
Could you list the open PRs that need review? I'd like to get this unblocked. Files shouldn't be "embroiled".
Yaël Dillies (Jan 31 2025 at 20:18):
#21308 for Data.ZMod.Basic
Etienne Marion (Feb 08 2025 at 18:54):
#21580 for MeasureTheory/Integral/Bochner
Bolton Bailey (Feb 08 2025 at 20:08):
#21567 for Data.Set.Basic
Kim Morrison (Feb 09 2025 at 05:56):
Thanks both, much appreciated!
Ben Eltschig (Feb 09 2025 at 06:58):
#21591 splits Topology.Connected.PathConnected; it's not on this list, but is also already somewhat lengthy and would reach >1500 lines with another PR I'm working on.
Xavier Roblot (Feb 09 2025 at 13:43):
#21554 splits Analysis.Normed.Group.Basic and is a first step toward removing Complex.abs
Bjørn Kjos-Hanssen (Feb 09 2025 at 21:17):
#21623 splits Computability/TuringMachine
Kim Morrison (Feb 10 2025 at 00:53):
Bjørn Kjos-Hanssen ☀️ said:
#21623 splits
Computability/TuringMachine
@Bjørn Kjos-Hanssen ☀️, what is going on with the file names here? I haven't seen a filename ending with 0 elsewhere.
Bjørn Kjos-Hanssen (Feb 10 2025 at 00:59):
@Kim Morrison The file has different variants of Turing machines, TM0, TM1, TM2... so the 0 was meant to indicate that TM0 is in that file. Should I try to make it more descriptive?
Kim Morrison (Feb 10 2025 at 01:11):
In that case, the name would be okay, as long as this is explained in the module docs of both files (preferably towards the beginning).
Bjørn Kjos-Hanssen (Feb 10 2025 at 01:41):
Makes sense, I've added an explanation.
Kim Morrison (Feb 10 2025 at 04:08):
Hmm, I guess it's still a bit of a weird name, as TuringMachine0 covers TM0 and TM1, while TuringMachine covers TM2.
Do others have ideas?
If not I can merge as is.
Bjørn Kjos-Hanssen (Feb 10 2025 at 04:25):
Maybe PostTuringMachine.lean instead of TuringMachine0.lean? To quote the file, "A TM0 Turing machine is essentially a Post-Turing machine, adapted for type theory." And "The TM1 model is a simplification and extension of TM0 (Post-Turing model) in the direction of
Wang B-machines."
Edit: I have now submitted a new version with that change.
Kim Morrison (Feb 10 2025 at 04:36):
Great.
Violeta Hernández (Feb 10 2025 at 04:38):
Kim Morrison said:
Could you list the open PRs that need review? I'd like to get this unblocked. Files shouldn't be "embroiled".
Being honest, the current blocker is me. I've had a bunch of refactors planned out in #17033 for months, but I haven't quite found the necessary time to execute them. Hopefully I can get back on track these following weeks.
As for the refactors which are already done, #19802 is a pretty large one which would be nice to get merged soon.
Anne Baanen (Feb 10 2025 at 15:24):
#21664 splits UniformSpace/Basic.lean into a Defs.lean and Basic.lean
Michael Rothgang (Feb 12 2025 at 12:34):
#21783 splits material on (bounded) continuous functions out of MeasureTheory/Function/LpSpace.lean
David Ang (Feb 12 2025 at 16:41):
#21356 splits the elliptic curve files but it's not 100% ready yet
Bjørn Kjos-Hanssen (Feb 19 2025 at 00:34):
#22068 splits Computability/TMToPartrec.lean
Bolton Bailey (Feb 20 2025 at 18:23):
Looking at Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean, it seems a bit off that so many of the lemmas are about Monoids and so few are about Groups per se. Could we perhaps move the entire ...BigOperators/Group/* directory into a new ...BigOperators/Monoid/ and then recreate nearly the same file structure in ...BigOperators/Group/* with just the Group lemmas?
Kim Morrison (Feb 25 2025 at 02:21):
I'm taking a look at our current long files. I'll post bullet points separately in case people want to use emojis to claim them. :-)
Kim Morrison (Feb 25 2025 at 02:21):
- #22258 (still needs a
shake) splits CategoryTheory.Limits.Shapes.Biproducts into the finitary and binary parts. Besides this file there are no long files in CategoryTheory!
Kim Morrison (Feb 25 2025 at 02:21):
- file#Data/Ordmap/Ordset is an untouched corner of Mathlib since 2017. I think it would be better to move it out (separate repo? Batteries?) than invest time in it here, but we should do one or the other! @Mario Carneiro?
Kim Morrison (Feb 25 2025 at 02:21):
- file#AlgebraicGeometry/EllipticCurve/Jacobian and file#AlgebraicGeometry/EllipticCurve/Projective are both slightly too long. @David Ang, do you think these could be split usefully into smaller pieces? (Edit: already WIP at #21356)
Kim Morrison (Feb 25 2025 at 02:21):
- file#Data/Num/Lemmas, perhaps @Mario Carneiro could take a look at revising this?
Kim Morrison (Feb 25 2025 at 02:22):
- I'm looking at Mathlib.Algebra.BigOperators.Group.Finset.Basic now: now #22261
Kim Morrison (Feb 25 2025 at 02:22):
- Mathlib.Analysis.Calculus.ContDiff.Basic: perhaps @Sébastien Gouëzel or @Floris van Doorn could suggest a split, or suggest someone who might like to do the split? It seems we could easily move the "operations" (+, *, -, smul) to a second file, or move all the material about inverses to a separate file. Or the 1d specializations? Besides this file there are no long files in Analysis! :tada:
Kim Morrison (Feb 25 2025 at 02:22):
Kim Morrison (Feb 25 2025 at 02:22):
- Ideas for file#Mathlib/Data/Real/EReal?
Kim Morrison (Feb 25 2025 at 02:22):
- There's a cluster of LinearAlgebra files: file#LinearAlgebra/Dual, file#LinearAlgebra/LinearIndependent, file#LinearAlgbra/AffineSpace/AffineSubspace, file#LinearAlgebra/Multilinear/Basic, file#LinearAlgebra/TensorProduct/Basic
Kim Morrison (Feb 25 2025 at 02:22):
- Quite a few other files, please post if you have ideas about how to split them!
Anne Baanen (Feb 25 2025 at 08:54):
Kim Morrison said:
- There's a cluster of LinearAlgebra files: file#LinearAlgebra/Dual, file#LinearAlgebra/LinearIndependent, file#LinearAlgbra/AffineSpace/AffineSubspace, file#LinearAlgebra/Multilinear/Basic, file#LinearAlgebra/TensorProduct/Basic
#22065 splits file#LinearAlgebra/LinearIndependent.
Michael Rothgang (Feb 25 2025 at 15:35):
I believe @David Ang has a draft PR splitting both EllioticCurve files. That had a diff if +-6000 lines, though - so should presumably be split :drum:
Sébastien Gouëzel (Feb 25 2025 at 16:49):
#22293 splits the file Calculus.ContDiff.
David Ang (Feb 25 2025 at 17:04):
Michael Rothgang said:
I believe David Ang has a draft PR splitting both EllioticCurve files. That had a diff if +-6000 lines, though - so should presumably be split :drum:
Yeah, I saw the comment on my PR two weeks ago, but haven't had the time to touch Lean yet... give me a week!
Kim Morrison (Feb 27 2025 at 04:01):
split long file Mahtlib.LinearAlgebra.TensorProduct.Basic #22351
Kim Morrison (Feb 27 2025 at 04:01):
split Mathlib.LinearAlgebra.Multilinear.Basic #22350
Kim Morrison (Feb 27 2025 at 04:38):
This isn't actually a long file, but I think this split will make file#LinearAlgbra/AffineSpace/AffineSubspace easier:
split Mathlib.Algebra.AddTorsor into Defs/Basic #22310
David Ang (Feb 27 2025 at 20:15):
#22374 is my attempt at isolating the first main changes in the 6000+- line diff
Kim Morrison (Feb 27 2025 at 23:13):
split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace #22384
Kim Morrison (Mar 03 2025 at 00:59):
split long file Mathlib.Data.Set.Basic #22484
Kim Morrison (Mar 03 2025 at 00:59):
split long file Algebra.BigOperators.Group.Finset.Basic #22476
Kim Morrison (Mar 03 2025 at 01:00):
remove some bad simp attributes #22482 (this only incidentally fixes a long file!)
Bolton Bailey (Mar 03 2025 at 02:39):
Bolton Bailey said:
Looking at
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean, ...
This PR turned out to go stale very quickly, but I think Fintype could perhaps be split out of this file
Bolton Bailey (Mar 03 2025 at 02:40):
(actually seems Kim's message immediately above addresses this file)
David Ang (Mar 04 2025 at 13:18):
David Ang said:
Michael Rothgang said:
I believe David Ang has a draft PR splitting both EllioticCurve files. That had a diff if +-6000 lines, though - so should presumably be split :drum:
Yeah, I saw the comment on my PR two weeks ago, but haven't had the time to touch Lean yet... give me a week!
As promised exactly one week ago, #22545 splits Jacobian files and #22549 splits projective files, but these depend on two small chores #22479 and #22524
Anne Baanen (Mar 07 2025 at 16:19):
#22697 splits LinearAlgebra.Dual.
Michael Rothgang (Mar 11 2025 at 12:34):
#22827 splits Topology/Constructions.lean
Bolton Bailey (Mar 16 2025 at 19:10):
An update to the OP (now further updated as of March 17)
Algebra
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean:set_option linter.style.longFile 1800
:check: Mathlib/Algebra/Group/Pointwise/Set/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean:set_option linter.style.longFile 2000
Data
Mathlib/Data/Num/Lemmas.lean:set_option linter.style.longFile 1700
Mathlib/Data/Ordmap/Ordset.lean:set_option linter.style.longFile 1700
Mathlib/Data/Real/EReal.lean:set_option linter.style.longFile 2200
Mathlib/Data/Seq/WSeq.lean:set_option linter.style.longFile 1800
:check: Mathlib/Data/Set/Function.lean:set_option linter.style.longFile 1800
:check: Mathlib/Data/Set/Lattice.lean:set_option linter.style.longFile 2100
Geometry
:check: Mathlib/Geometry/Manifold/VectorField.lean:set_option linter.style.longFile 1700
Logic
Mathlib/Logic/Equiv/Basic.lean:set_option linter.style.longFile 2000
Measure Theory
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/Lebesgue.lean:set_option linter.style.longFile 2200
Mathlib/MeasureTheory/Integral/SetToL1.lean:set_option linter.style.longFile 1800
Mathlib/MeasureTheory/Measure/Typeclasses.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean:set_option linter.style.longFile 1700
Order
:check: Mathlib/Order/CompleteLattice.lean:set_option linter.style.longFile 1900
Mathlib/Order/Hom/Lattice.lean:set_option linter.style.longFile 1800
Mathlib/Order/Interval/Set/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Order/LiminfLimsup.lean:set_option linter.style.longFile 1900
Mathlib/Order/UpperLower/Basic.lean:set_option linter.style.longFile 1900
Set Theory
:check: Mathlib/SetTheory/Cardinal/Basic.lean:set_option linter.style.longFile 2400
Mathlib/SetTheory/Game/PGame.lean:set_option linter.style.longFile 2300
:check: Mathlib/SetTheory/Ordinal/Arithmetic.lean:set_option linter.style.longFile 2600
Mathlib/SetTheory/ZFC/Basic.lean:set_option linter.style.longFile 1700
Topology
:check: Mathlib/Topology/Algebra/Group/Basic.lean:set_option linter.style.longFile 2100
Mathlib/Topology/Basic.lean:set_option linter.style.longFile 1900
Mathlib/Topology/Category/Profinite/Nobeling.lean:set_option linter.style.longFile 2000
:check: Mathlib/Topology/ContinuousOn.lean:set_option linter.style.longFile 1700
Kevin Buzzard (Mar 16 2025 at 19:14):
We're number-theory-free :-)
Bolton Bailey (Mar 16 2025 at 20:09):
#22987 splits Logic/Equiv/Basic.lean
Michael Rothgang (Mar 16 2025 at 21:03):
Thanks for posting the update! It appears that you counted an older copy of mathlib, though: as one example, Topology/Constructions.lean has since been split
Kim Morrison (Mar 17 2025 at 05:27):
chore: split long file Mathlib.Geometry.Manifold.VectorField #23000
Kim Morrison (Mar 17 2025 at 05:33):
chore: split long file Topology.ContinuousOn #23001
This one will still need a shake, but could be delegated already. :-)
Kim Morrison (Mar 17 2025 at 05:51):
split long file Topology.Algebra.Group.Basic #23002
Kim Morrison (Mar 17 2025 at 06:40):
split long file Order.CompleteLattice #23003
Anne Baanen (Mar 17 2025 at 15:51):
split SetTheory/Cardinal/Basic.lean: #23014
Anne Baanen (Mar 17 2025 at 15:53):
I am going to stare at Mathlib/SetTheory/Ordinal/Arithmetic.lean now, see if there is a good place to start carving. But I'll only have 40 or so minutes tonight, so if you don't hear anything from me before , feel free to claim it instead :)
Anne Baanen (Mar 17 2025 at 16:27):
(WIP, feel free to take over while I'm away!): split Ordinal/Arithmetic.lean: #23017
Kim Morrison (Mar 18 2025 at 04:07):
chore: split long file MeasureTheory/Function/LpSeminorm #23036
Anne Baanen (Mar 18 2025 at 09:27):
split Ordinal/Arithmetic.lean: #23017 should now be ready for review.
Anne Baanen (Mar 19 2025 at 15:08):
partial split of Data/Set/Lattice.lean: #23098
Anne Baanen (Mar 19 2025 at 15:09):
partial split of Equiv/Basic.lean: #23099 (needs a shake)
Jeremy Tan (Mar 20 2025 at 08:55):
SetTheory.Game.PGame: #23133
Anne Baanen (Mar 20 2025 at 14:44):
Split Data.Set.Function: #23149
Anne Baanen (Mar 20 2025 at 14:53):
split iUnion/iInter from Algebra.Pointwise.Set.Basic: #23152
Anne Baanen (Mar 20 2025 at 16:43):
A tiny bit of progress on Algebra.Pointwise.Finset.Basic: #23156
Jeremy Tan (Mar 24 2025 at 02:48):
Order.UpperLower.Basic: #23248
Jeremy Tan (Mar 24 2025 at 04:32):
Order.Hom.Lattice: #23249
Jeremy Tan (Mar 24 2025 at 07:25):
Order.LiminfLimsup: #23250
Jeremy Tan (Mar 25 2025 at 07:29):
Data.Seq.WSeq: #23294 (still trying to see if there are any more good splits at time of posting)
Jeremy Tan (Mar 25 2025 at 14:05):
OK #23294 is ready
Jeremy Tan (Mar 26 2025 at 00:33):
This is all that's left:
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean:set_option linter.style.longFile 1800
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean:set_option linter.style.longFile 2000
Mathlib/Data/Num/Lemmas.lean:set_option linter.style.longFile 1700
Mathlib/Data/Ordmap/Ordset.lean:set_option linter.style.longFile 1700
Mathlib/Data/Real/EReal.lean:set_option linter.style.longFile 2200
Mathlib/Data/WSeq/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/Lebesgue.lean:set_option linter.style.longFile 2200
Mathlib/MeasureTheory/Integral/SetToL1.lean:set_option linter.style.longFile 1800
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Measure/Typeclasses.lean:set_option linter.style.longFile 1700
Mathlib/Order/Interval/Set/Basic.lean:set_option linter.style.longFile 1700
Mathlib/SetTheory/ZFC/Basic.lean:set_option linter.style.longFile 1700
Mathlib/Topology/Basic.lean:set_option linter.style.longFile 1900
Mathlib/Topology/Category/Profinite/Nobeling.lean:set_option linter.style.longFile 2000
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean:set_option linter.style.longFile 1700
Jeremy Tan (Mar 26 2025 at 00:33):
#23294 (Data.WSeq.Basic) is still awaiting review
Johan Commelin (Mar 26 2025 at 02:19):
I am working on Nobeling
Johan Commelin (Mar 26 2025 at 05:57):
Some tiny prerequisites:
- chore(Data/FunLike): add
dite_applyandite_applytheorems #23306
Johan Commelin (Mar 26 2025 at 05:57):
- chore(Algebra/BigOperators/Finsupp): add Finsupp.sum_apply'' #23305
Jeremy Tan (Mar 27 2025 at 02:37):
SetTheory.ZFC.Basic: #23354
Jeremy Tan (Mar 28 2025 at 05:45):
In #23390 I move Data.Real.EReal to Data.EReal.Basic, anticipating the split of this file
Jeremy Tan (Mar 30 2025 at 13:50):
Data.EReal.Basic: #23428
Bolton Bailey (Mar 30 2025 at 14:48):
#23429 Algebra.Group.Pointwise.Finset.Basic
Jeremy Tan (Mar 31 2025 at 19:14):
MeasureTheory.Function.LpSpace.Basic: #23508
Jeremy Tan (Apr 01 2025 at 06:48):
MeasureTheory.MeasurableSpace.Basic: #23523
Jeremy Tan (Apr 01 2025 at 09:41):
Data.Ordmap.Ordset: #23529
Jeremy Tan (Apr 01 2025 at 15:50):
Order.Interval.Set.Basic: #23556
Jeremy Tan (Apr 02 2025 at 02:21):
Topology.ContinuousMap.Bounded.Basic: #23574
Jeremy Tan (Apr 02 2025 at 02:21):
I now have four open PRs splitting long files. Would anyone like to review and merge them?
Jeremy Tan (Apr 03 2025 at 05:53):
Algebra.Order.GroupWithZero.Unbundled: #23620
Jeremy Tan (Apr 03 2025 at 05:54):
(really, the branch name for the above PR should have been gwalior)
Jeremy Tan (Apr 03 2025 at 08:03):
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:set_option linter.style.longFile 1600
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean:set_option linter.style.longFile 2000
Mathlib/Data/Num/Lemmas.lean:set_option linter.style.longFile 1700
Mathlib/Data/Ordmap/Ordset.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/Lebesgue.lean:set_option linter.style.longFile 2200
Mathlib/MeasureTheory/Integral/SetIntegral.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/SetToL1.lean:set_option linter.style.longFile 1800
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Measure/Typeclasses.lean:set_option linter.style.longFile 1700
Mathlib/Topology/Basic.lean:set_option linter.style.longFile 1900
Mathlib/Topology/Category/Profinite/Nobeling.lean:set_option linter.style.longFile 2000
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean:set_option linter.style.longFile 1700
Jeremy Tan (Apr 04 2025 at 03:06):
MeasureTheory.Measure.Typeclasses: #23649
Jeremy Tan (Apr 04 2025 at 03:07):
(it seems like every time one of the splitting PRs gets merged, another one goes over the limit!)
Kim Morrison (Apr 04 2025 at 03:45):
Reviewers shouldn't be merging anything that increases the file length limit, please. :-)
Jeremy Tan (Apr 04 2025 at 04:05):
Jeremy Tan said:
(really, the branch name for the above PR should have been
gwalior)
(just kidding here, of course)
Jeremy Tan (Apr 04 2025 at 04:49):
Algebra.Order.Floor: #23652 (pinging @Eric Wieser for pushing this over the limit)
Jeremy Tan (Apr 04 2025 at 05:17):
Data.Num.Lemmas: #23655
Yaël Dillies (Apr 04 2025 at 05:52):
The point of writing "Pushed over the limit by deprecations" is to avoid people splitting up the file because it was only transiently too big. Please do not split files on the sole basis that they are >=1500 lines long.
Ruben Van de Velde (Apr 04 2025 at 06:01):
Kim Morrison said:
Reviewers shouldn't be merging anything that increases the file length limit, please. :-)
On the contrary, reviewers should not block a pr that increases a file from 1499 to 1501 lines. That just leads to people trying to cram code into fewer lines than is reasonably or putting things in the wrong file
Yaël Dillies (Apr 04 2025 at 06:10):
(I read Kim's message as a joke, but to be clear yes I agree with Ruben here)
Jeremy Tan (Apr 04 2025 at 07:45):
Yaël Dillies said:
The point of writing "Pushed over the limit by deprecations" is to avoid people splitting up the file because it was only transiently too big. Please do not split files on the sole basis that they are >=1500 lines long.
I got a better thought-out split; see the updated #23652
Jeremy Tan (Apr 04 2025 at 16:59):
@Anne Baanen see my reply here and branch#ao-floor-hybrid
Jeremy Tan (Apr 06 2025 at 10:20):
Topology.Basic: #23717
Kim Morrison (Apr 07 2025 at 01:58):
Ruben Van de Velde said:
Kim Morrison said:
Reviewers shouldn't be merging anything that increases the file length limit, please. :-)
On the contrary, reviewers should not block a pr that increases a file from 1499 to 1501 lines. That just leads to people trying to cram code into fewer lines than is reasonably or putting things in the wrong file
Hmm, I actually wasn't intending any joke, and instead that the PR should wait until someone can split the long file first!
Eric Wieser (Apr 07 2025 at 02:19):
Even when the PR is something like adding a docstring or fixing a typo in a theorem name and deprecating the old one?
Kim Morrison (Apr 07 2025 at 03:01):
Yes, we don't have a sustainable mechanism that will prevent long files creeping back, unless when we reach "no long file", we turn it into an non-overridable error...!
It would be great to have such a mechanism, of course, because I agree, of course, that this would be annoying to contributors (and doubly annoying to reviewers if they had to remind contributors not to "compress" things).
Jeremy Tan (Apr 07 2025 at 03:18):
In preparation for the split of Algebra.Order.GroupWithZero.Unbundled: #23755
Jeremy Tan (Apr 07 2025 at 03:18):
(this just moves files, no splitting yet)
Jeremy Tan (Apr 08 2025 at 05:22):
Preparation for splitting MeasureTheory.Integral.Lebesgue, moving it to ...Lebesgue.Basic: #23807
Johan Commelin (Apr 08 2025 at 05:55):
Johan Commelin said:
I am working on Nobeling
I am relinquishing this lock. My experiment did not converge.
Jeremy Tan (Apr 08 2025 at 13:08):
Algebra.Order.GroupWithZero.Unbundled: #23828
Jeremy Tan (Apr 08 2025 at 13:09):
small chunks of MeasureTheory.Integral.Lebesgue.Basic: #23819
Jeremy Tan (Apr 09 2025 at 07:35):
It was the longest file in mathlib (before I split the small chunks out). Because of that, I have two proposed splits of MeasureTheory.Integral.Lebesgue.Basic.
My main proposed split is #23860, which shuffles all the twisted declarations around into four new files and a renamed fifth file (because it accepts results which expand its scope)
Jeremy Tan (Apr 09 2025 at 07:37):
If the above "deep split" is not acceptable, I have a less ambitious split at #23855 which still clears the tech debt
Jeremy Tan (Apr 09 2025 at 10:22):
The purpose of the deep split #23860 is not only to reduce the tech debt but also to expose theorems that may have been proved with too much
Jeremy Tan (Apr 09 2025 at 10:23):
e.g. surely lintegral_eq_zero_iff doesn't need Markov's inequality
Jeremy Tan (Apr 09 2025 at 14:21):
Oh, and by the way
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean:set_option linter.style.longFile 1600
Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean:set_option linter.style.longFile 1800
Mathlib/MeasureTheory/Integral/SetIntegral.lean:set_option linter.style.longFile 1700
Mathlib/MeasureTheory/Integral/SetToL1.lean:set_option linter.style.longFile 1800
Mathlib/Topology/Category/Profinite/Nobeling.lean:set_option linter.style.longFile 2000
Jeremy Tan (Apr 10 2025 at 02:38):
Algebra.BigOperators.Group.Finset.Basic: #23897
Jeremy Tan (Apr 10 2025 at 03:57):
Topology.Category.Profinite.Nobeling: #23898
Johan Commelin (Apr 10 2025 at 04:39):
@Jeremy Tan Thanks. Could you please make all the new files refer back to .Basic for the proof idea?
Johan Commelin (Apr 10 2025 at 04:39):
(Just add 1 line to their module docstrings.)
Jeremy Tan (Apr 10 2025 at 04:43):
Johan Commelin said:
(Just add 1 line to their module docstrings.)
Done :+1:
Jeremy Tan (Apr 10 2025 at 05:23):
The remaining three long files are all in MeasureTheory.Integral. I'd like to have #23860 (Lebesgue.Basic) merged first, since the other two long files transitively import it
Jeremy Tan (Apr 10 2025 at 13:28):
Then I would split SetIntegral and then SetToL1 would be the very last split of all
Jeremy Tan (Apr 15 2025 at 08:32):
MeasureTheory.Integral.SetIntegral: #24070
Michael Rothgang (Apr 15 2025 at 09:24):
There is now a single long file left: Mathlib/MeasureTheory/Integral/SetToL1.lean :tada:
Jeremy Tan (Apr 15 2025 at 10:39):
MeasureTheory.Integral.SetToL1: #24075
Jeremy Tan (Apr 15 2025 at 10:54):
And then there were none
Johan Commelin (Apr 15 2025 at 12:02):
@Jeremy Tan Thanks for your great effort to push this over the finish line!
Ruben Van de Velde (Apr 15 2025 at 13:00):
Time to lower the cut-off
Michael Rothgang (Apr 15 2025 at 13:47):
#24081 tries exactly that --- if only to find out which files are still somewhat long.
Michael Rothgang (Apr 15 2025 at 13:48):
Among the first 1000 files, there are 11 such files.
Jeremy Tan (Apr 15 2025 at 14:31):
Kim Morrison said:
Yes, we don't have a sustainable mechanism that will prevent long files creeping back, unless when we reach "no long file", we turn it into an non-overridable error...!
It would be great to have such a mechanism, of course, because I agree, of course, that this would be annoying to contributors (and doubly annoying to reviewers if they had to remind contributors not to "compress" things).
#24083 provides exactly that mechanism
Damiano Testa (Apr 15 2025 at 14:37):
An alternative implementation would be to simply remove the longFile linter option and make the linter perform the check regardless...
Damiano Testa (Apr 15 2025 at 14:37):
(Note: I am not suggesting that I would be happy with this hard rule!)
Yaël Dillies (Apr 15 2025 at 14:37):
I am strongly against making the error non-overridable. I am still dealing with consequences of past eagerly split files...
Jeremy Tan (Apr 15 2025 at 14:38):
I think the existing longFile linter behaviour would still be desirable for downstream projects, so I have kept it
Michael Rothgang (Apr 15 2025 at 14:39):
(This post contained a list of all files with over 1200. I have deleted that - since I believe there are now more useful ways to tackle technical debt --- such as removing erws.)
Yaël Dillies (Apr 15 2025 at 14:39):
Can't wait for 50 lines long files...
Michael Rothgang (Apr 15 2025 at 14:40):
(deleted)
Michael Rothgang (Apr 15 2025 at 14:41):
Damiano Testa said:
An alternative implementation would be to simply remove the
longFilelinter option and make the linter perform the check regardless...
Or we could add an option to the set_option linter which complains about the longFile linter being set. (That seems more elegant than the "hard" linter version.)
Jeremy Tan (Apr 15 2025 at 15:27):
I will stick with my longFileHard. I could not find a way to tweak the setOption linter to ensure that a warning is generated when the option for making the longFile linter hard is turned off
Jeremy Tan (Apr 15 2025 at 15:29):
set_option linter.style.setOptionLongFile true
set_option linter.style.longFile 0
set_option linter.style.longFileDefValue 8000
set_option linter.style.setOptionLongFile false -- should emit a warning
Michael Rothgang (Apr 15 2025 at 15:33):
Sure - but there seems to be no consensus for merging that into mathlib. Yes, there are probably files that could be split, but mere file length doesn't look like a good heuristic any more: i.e., imho this can happen on a case by case basis.
Kim Morrison (Apr 16 2025 at 00:34):
If anyone is looking for "reorganization" type tasks, similar to the recent work on long files (perhaps you, @Jeremy Tan!), I would love to see further progress on reducing the occasional crazy dependencies we have between top-level directories, i.e. as #23088 tries to prevent.
Relatedly, we have a lot of content in Mathlib/Data/ that really doesn't belong there.
Both of these sorts of changes require some amount of patience, as they will typically need some discussion on Zulip as well as just hitting merge on PRs!
Joseph Myers (Apr 20 2025 at 10:53):
A typical example of a crazy dependency that shouldn't be hard to fix (move one file and update imports of it): Topology imports probably don't belong in LinearAlgebra, so why is ContinuousAffineEquiv under LinearAlgebra.AffineSpace when ContinuousAffineMap is under the more appropriate (in terms of such dependencies) Topology.Algebra? (I do have an open PR #23732 to ContinuousAffineEquiv in its current location; that could of course readily be updated after any move of the file.)
Bolton Bailey (Apr 21 2025 at 04:25):
:tada: #mathlib4 > Technical Debt Counters @ 💬 :tada:
David Ang (May 03 2025 at 16:47):
Not really a long file, but #21356 splits Affine.lean and Group.lean into Affine/Basic.lean, Affine/Formula.lean, and Affine/Point.lean which I promised about two months ago but only had the chance to come back to it now...
Xavier Roblot (May 04 2025 at 13:35):
The file NumberTheory.NumberField.Embeddings is also not a long file but still at 1250 lines on its way to become one, so #24478 splits it into 4 files:
InfinitePlace.Embeddings: results about complex embeddingsInfinitePlace.Basic: definitions and basic results about infinite placesInfinitePlace.Ramification: ramification of infinite places in extensionsInfinitePlace.TotallyRealComplex: stuff about totally real and totally complex number fields.
Anne Baanen (May 05 2025 at 06:53):
Looks like file#Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean went over the limit. (Should we just disable the possibility of increasing the limit?)
Kevin Buzzard (May 05 2025 at 07:45):
There was pushback against this the last time it was suggested. I would be happy to disable the possibility though, especially if there are now no long files (is that the case?)
Ruben Van de Velde (May 05 2025 at 07:51):
Again, no, we shouldn't. That just leads to people working around it in worse ways
Kevin Buzzard (May 05 2025 at 08:47):
Ok then how about we have two limits? A "it's ok to go above this length but you're now on a naughty list and someone needs to start thinking about splitting" and an "you absolutely can't go above this length because then you're classed as causing work for other people"
Kevin Buzzard (May 05 2025 at 08:48):
eg over 1500 is ok (but adds you to to the technical debt list) but CI fails if the file is over 2K and that's the end of it
Eric Wieser (May 05 2025 at 11:36):
Any hard limit is going to be a pain for Kim
Eric Wieser (May 05 2025 at 11:37):
If we're right up against it, this now incentivizes not writing adaptation notes to avoid lengthening the file, which is surely a worse outcome than allowing the length over an arbitrary limit
Kevin Buzzard (May 05 2025 at 12:03):
My naive hope was that we never get near to the hard limit because someone interested in the area has to react when we get to the soft limit
Eric Wieser (May 05 2025 at 12:09):
Is that different to the status quo?
Kevin Buzzard (May 05 2025 at 12:25):
Yes: I was proposing a hard limit which you couldn't get around by disabling a linter.
Andrew Yang (May 05 2025 at 12:34):
It is impossible to go from under 1500 straight to 2K without having a 500+ diff and the PR will most likely be blocked for being too big.
Other than this, the file has passed the soft limit to begin with and I don't think we should punish the PR author (who we agree shouldn't take on the responsibility of splitting the file) for this.
Kevin Buzzard (May 06 2025 at 11:05):
Ok, you've convinced me that the status quo is fine.
github mathlib4 bot (Jun 04 2025 at 11:37):
3 files exceed the length limit (1500).
Ref commit: 151dd12
Damiano Testa (Jun 04 2025 at 11:38):
The above is a test of a new weekly workflow.
Michael Rothgang (Jun 04 2025 at 14:14):
This is great! What do you think about adding a short header: "The following are the 10 longest files in mathlib" or so?
Damiano Testa (Jun 04 2025 at 14:25):
#25438 would produce
Damiano Testa (Jun 04 2025 at 14:26):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: 6455ba8ab6
Damiano Testa (Jun 04 2025 at 15:15):
I am going to trigger the action once more, with the added title.
EDIT: looks alright!
github mathlib4 bot (Jun 04 2025 at 15:16):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: a037050
github mathlib4 bot (Jun 09 2025 at 04:10):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 02aed45
David Ang (Jun 09 2025 at 12:31):
Are there any plans to shift the 1500 soft limit down further, perhaps to 1000? I’m aware that 1000 is supposedly the recommended limit, but it’s not marked by the linter
Damiano Testa (Jun 09 2025 at 16:06):
I don't know of any such plans, but as a first step, maybe this report could extend to show all files above 1400 lines. Currently, it simply prints the 10 longest files.
Johan Commelin (Jun 09 2025 at 17:00):
There are no concrete plans. For now, I think we should mainly use this bot as incentive to get files below the 1500 limit again.
github mathlib4 bot (Jun 16 2025 at 04:10):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 8744850
Kenny Lau (Jun 16 2025 at 07:47):
What about the 10 longest files to build (i.e. in time)?
Kevin Buzzard (Jun 16 2025 at 08:15):
file#Mathlib/RingTheory/Kaehler/JacobiZariski, file#Mathlib/RingTheory/Kaehler/JacobiZariski, file#Mathlib/RingTheory/Kaehler/JacobiZariski, file#Mathlib/RingTheory/Kaehler/JacobiZariski, ...
Kevin Buzzard (Jun 16 2025 at 08:18):
Kenny you can see a ton of stats at https://speed.lean-lang.org/mathlib4/home . For example https://speed.lean-lang.org/mathlib4/compare/ba9ff5bb-e851-419f-96cf-0874852439fc/to/3c5ce755-9a37-4b0c-bd93-a056b95e94ce shows that the JacobiZariski file is still taking the longest.
Christian Merten (Jun 16 2025 at 08:54):
We could instantly push JacobiZariski off the first spot by merging #21129 :)
Damiano Testa (Jun 16 2025 at 08:59):
My impression is that if the alphabetical ordering of universes is the cause of the slowdown, then the solution should not be to find the "correct" ordering, but to fix make the algorithm stable under sorting order.
In particular, I'd rather keep the file as is, as a test!
Damiano Testa (Jun 16 2025 at 09:01):
Nevertheless, it may be a good idea to have the bot also post the data of the 10 slowest files.
Damiano Testa (Jun 16 2025 at 09:01):
Although, as with all metrics, simply minimising them is not necessarily the intended way forwards!
Christian Merten (Jun 16 2025 at 09:02):
Damiano Testa said:
My impression is that if the alphabetical ordering of universes is the cause of the slowdown, then the solution should not be to find the "correct" ordering, but to fix make the algorithm stable under sorting order.
In particular, I'd rather keep the file as is, as a test!
IMHO, a TODO at the top of the file would suffice for this.
Damiano Testa (Jun 16 2025 at 09:02):
With the TODO, it becomes trickier to measure the effect of the change, though.
Damiano Testa (Jun 16 2025 at 09:04):
If I were the one changing the algorithm, I'd much rather have a simple measure of "how long does it take to build this file", instead of "after I change this file back to what it was before the renames, but not any possible future change, how long does it take to build".
Christian Merten (Jun 16 2025 at 09:04):
Damiano Testa said:
With the TODO, it becomes trickier to measure the effect of the change, though.
Measuring the effect should be done by randomly permuting the alphabetical ordering of the universe variables in this file and testing on each permutation, not just checking if a new algorithm happens to make the current (also arbitrarily chosen) order better.
Johan Commelin (Jun 16 2025 at 09:06):
@Christian Merten That's a good point. Would you mind adding such an explicit TODO to the top of the file, in your PR?
Johan Commelin (Jun 16 2025 at 09:07):
Atm, the code refers to the PR discussion. But there are 41 comments. I feel like you have a good understanding of the problem. If you could summarize that into a github issue, and link to that instead, that would be great.
Having that issue would be very valuable, independent of whether this PR is merged.
Christian Merten (Jun 16 2025 at 09:08):
If there is a consensus that we want the PR to be merged, I am happy to fix the merge conflicts and add a TODO.
Christian Merten (Jun 16 2025 at 09:08):
Johan Commelin said:
Atm, the code refers to the PR discussion. But there are 41 comments. I feel like you have a good understanding of the problem. If you could summarize that into a github issue, and link to that instead, that would be great.
Having that issue would be very valuable, independent of whether this PR is merged.
Will do that.
Bjørn Kjos-Hanssen (Jun 20 2025 at 02:03):
I made a split of AkraBazzi.lean here: #26193
Enjoying the new :fork_and_knife: -based system.
Bolton Bailey (Jun 20 2025 at 17:42):
#26234 splits SimpleGraph/Path.lean and reorganizes the directory structure to group the Walk-related definitions
Bolton Bailey (Jun 21 2025 at 19:31):
#25920 is a feature PR, but it incidentally reduces Finsupp.Basic.
Bolton Bailey (Jun 21 2025 at 19:32):
#26260 splits Fin.Basic
github mathlib4 bot (Jun 23 2025 at 04:35):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: dfe27eb
github mathlib4 bot (Jun 30 2025 at 04:11):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: 162202c
Kevin Buzzard (Jun 30 2025 at 06:54):
I think this effort is great. For some reason 2500 line files used to really annoy me and now things are so much better. Thanks to everyone involved in this push to keep our files manageable lengths.
github mathlib4 bot (Jul 07 2025 at 04:12):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: 449b24f
github mathlib4 bot (Jul 14 2025 at 04:17):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 1ee1c8e
github mathlib4 bot (Jul 21 2025 at 04:18):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 82ecf95
github mathlib4 bot (Jul 28 2025 at 04:19):
The 10 longest files in mathlib
5 files exceed the length limit (1500).
Ref commit: 307188a
Jireh Loreaux (Jul 28 2025 at 04:51):
Projection is on my todo list.
Anne Baanen (Jul 31 2025 at 09:59):
split DedekindDomain.Ideal: #27676
Monica Omar (Aug 01 2025 at 21:41):
split Projection: #27851
Kim Morrison (Aug 03 2025 at 06:13):
@Monica Omar, this is one is still marked as "draft".
Monica Omar (Aug 03 2025 at 14:20):
oh right, my bad
Jireh Loreaux (Aug 03 2025 at 23:31):
Thanks @Monica Omar! I've left some comments.
github mathlib4 bot (Aug 04 2025 at 04:25):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: ad58550
github mathlib4 bot (Aug 11 2025 at 04:18):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: 0025b4a
github mathlib4 bot (Aug 18 2025 at 04:16):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: d77f47f
github mathlib4 bot (Aug 25 2025 at 04:07):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: 4044ad8
Kim Morrison (Aug 26 2025 at 01:12):
Kim Morrison (Aug 26 2025 at 01:13):
Just one to go! :-)
Michael Rothgang (Aug 26 2025 at 07:34):
In turn, #28905 and dependencies pushes three files over the edge...
Harald Husum (Aug 26 2025 at 10:47):
Michael Rothgang said:
In turn, #28905 and dependencies pushes three files over the edge...
Could it make sense to split the affected files before merging those PRs then? I've seen some people make preemptive spliting PRs like that before.
Ruben Van de Velde (Aug 26 2025 at 11:36):
It could, but it's not necessary
Ruben Van de Velde (Aug 26 2025 at 11:37):
The whole reason this is a table on zulip and not a CI requirement is that we don't want to make going over the line so annoying that people start doing unhelpful things to avoid it
Ruben Van de Velde (Aug 26 2025 at 11:38):
(e.g. putting too many things on single lines or removing whitespace or putting things in the wrong (but shorter) file)
github mathlib4 bot (Sep 01 2025 at 04:09):
The 10 longest files in mathlib
1 file exceeds the length limit (1500).
Ref commit: 74f1297
Bryan Gin-ge Chen (Sep 01 2025 at 04:15):
Unfortunately, Combinatorics.SimpleGraph.Walk is about to go over the length limit again in #27460.
Bolton Bailey (Sep 01 2025 at 04:16):
Perhaps now is a good time to reboot #26234 then. Sorry that's a different file.
Bolton Bailey (Sep 04 2025 at 01:54):
#29199 splits file#Mathlib/Data/Fin/Basic
github mathlib4 bot (Sep 08 2025 at 04:03):
The 10 longest files in mathlib
1 file exceeds the length limit (1500).
Ref commit: a3e910d
github mathlib4 bot (Sep 15 2025 at 04:03):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: a807134
github mathlib4 bot (Sep 22 2025 at 04:04):
The 10 longest files in mathlib
2 files exceed the length limit (1500).
Ref commit: 432a037
github mathlib4 bot (Sep 29 2025 at 04:03):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: a1957e2
github mathlib4 bot (Oct 06 2025 at 04:03):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 586e9c3
github mathlib4 bot (Oct 13 2025 at 04:03):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: a778305
github mathlib4 bot (Oct 20 2025 at 04:06):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 9e57458
github mathlib4 bot (Oct 27 2025 at 04:09):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 88d330e
github mathlib4 bot (Nov 03 2025 at 04:08):
The 10 longest files in mathlib
4 files exceed the length limit (1500).
Ref commit: 3655c4d
github mathlib4 bot (Nov 10 2025 at 04:07):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: d6b7d98
github mathlib4 bot (Nov 17 2025 at 04:07):
The 10 longest files in mathlib
3 files exceed the length limit (1500).
Ref commit: 4a5073f
github mathlib4 bot (Nov 24 2025 at 04:12):
The 10 longest files in mathlib
5 files exceed the length limit (1500).
Ref commit: c325a54
github mathlib4 bot (Dec 01 2025 at 04:22):
The 10 longest files in mathlib
6 files exceed the length limit (1500).
Ref commit: dc19f2a
Michael Stoll (Dec 01 2025 at 11:09):
One could split NumberTheory.ArithmeticFunction at the point where the special functions are introduced.
(I won't have time for that, however.)
David Loeffler (Dec 01 2025 at 12:59):
Michael Stoll said:
One could split NumberTheory.ArithmeticFunction at the point where the special functions are introduced.
(I won't have time for that, however.)
See #32304
Etienne Marion (Dec 01 2025 at 19:45):
#32327 splits Probability/Independence/Kernel, separating declarations about random variables in a new file.
github mathlib4 bot (Dec 08 2025 at 04:11):
The 10 longest files in mathlib
6 files exceed the length limit (1500).
Ref commit: 6201e59
David Loeffler (Dec 08 2025 at 19:37):
#32601 splits Mathlib/Topology/OpenPartialHomeomorph (the worst offender).
David Loeffler (Dec 08 2025 at 20:47):
#32605 splits Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.
Antoine Chambert-Loir (Dec 09 2025 at 17:29):
I had a look at the file#Mathlib/GroupTheory/MonoidLocalization/Basic.
It does not seem obvious to split it (except for one or two very small chunks). On the other hand, part of it seems to be deprecated by the more recent development of the Ore localization.
Antoine Chambert-Loir (Dec 09 2025 at 17:39):
It seems that file#Mathlib/Computability/Primrec could be split in one first file (roughly the first half of the file) and several other that show that some types are primitive recursive (sum, lists, etc.). The gain would probably be moderate because that file is only imported by one other file file#Mathlib/Computability/Partrec
github mathlib4 bot (Dec 15 2025 at 04:17):
The 10 longest files in mathlib
5 files exceed the length limit (1500).
Ref commit: 3ea6690
David Loeffler (Dec 15 2025 at 06:52):
ChartedSpace admits a natural shortening by splitting off the inital segment about StuctureGroupoid. That's a small gain since it is only about 10% of the file but would be enough to get it below 1.5k.
Last updated: Dec 20 2025 at 21:32 UTC