long files

Stream: mathlib4

[Johan Commelin]

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]

If you have some mathlib expertise in one of these areas, please help splitting these files!

[Johan Commelin]

#21215 takes care of LinearAlgebra/Multilinear/Basic

[Michael Rothgang]

I can take care of Geometry/Manifold/IsManifold.lean

[Johan Commelin]

#21224 takes care of LinearAlgebra/TensorProduct/Basic

[Michael Rothgang]

#21219 splits IsManifold/Basic.lean in two smaller files

[Bolton Bailey]

#21230 splits Data/Finsupp/Basic.lean

[Etienne Marion]

#21231 for MeasureTheory/Function/L1Space

[Bolton Bailey]

#21232 for Data/List/Basic

[Violeta Hernández]

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]

#21273 for MeasureTheory/Function/StronglyMeasurable/Basic

[Kim Morrison]

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 PSet and ZFSet in 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]

#21308 for Data.ZMod.Basic

[Etienne Marion]

#21580 for MeasureTheory/Integral/Bochner

[Bolton Bailey]

#21567 for Data.Set.Basic

[Kim Morrison]

Thanks both, much appreciated!

[Ben Eltschig]

#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]

#21554 splits Analysis.Normed.Group.Basic and is a first step toward removing Complex.abs

[Bjørn Kjos-Hanssen]

#21623 splits Computability/TuringMachine

[Kim Morrison]

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]

@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]

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]

Makes sense, I've added an explanation.

[Kim Morrison]

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]

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]

Great.

[Violeta Hernández]

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]

#21664 splits UniformSpace/Basic.lean into a Defs.lean and Basic.lean

[Michael Rothgang]

#21783 splits material on (bounded) continuous functions out of MeasureTheory/Function/LpSpace.lean

[David Ang]

#21356 splits the elliptic curve files but it's not 100% ready yet

[Bjørn Kjos-Hanssen]

#22068 splits Computability/TMToPartrec.lean

[Bolton Bailey]

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]

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]

• #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]

• 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]

• 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]

• file#Data/Num/Lemmas, perhaps @Mario Carneiro could take a look at revising this?

[Kim Morrison]

• I'm looking at Mathlib.Algebra.BigOperators.Group.Finset.Basic now: now #22261

[Kim Morrison]

• 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]

• file#Algebra/Order/GroupWithZero/Unbundled, anyone?

[Kim Morrison]

• Ideas for file#Mathlib/Data/Real/EReal?

[Kim Morrison]

• 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]

• Quite a few other files, please post if you have ideas about how to split them!

[Anne Baanen]

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]

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]

#22293 splits the file Calculus.ContDiff.

[David Ang]

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]

split long file Mahtlib.LinearAlgebra.TensorProduct.Basic #22351

[Kim Morrison]

split Mathlib.LinearAlgebra.Multilinear.Basic #22350

[Kim Morrison]

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]

#22374 is my attempt at isolating the first main changes in the 6000+- line diff

[Kim Morrison]

split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace #22384

[Kim Morrison]

split long file Mathlib.Data.Set.Basic #22484

[Kim Morrison]

split long file Algebra.BigOperators.Group.Finset.Basic #22476

[Kim Morrison]

remove some bad simp attributes #22482 (this only incidentally fixes a long file!)

[Bolton Bailey]

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]

(actually seems Kim's message immediately above addresses this file)

[David Ang]

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]

#22697 splits LinearAlgebra.Dual.

[Michael Rothgang]

#22827 splits Topology/Constructions.lean

[Bolton Bailey]

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]

We're number-theory-free :-)

[Bolton Bailey]

#22987 splits Logic/Equiv/Basic.lean

[Michael Rothgang]

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]

chore: split long file Mathlib.Geometry.Manifold.VectorField #23000

[Kim Morrison]

chore: split long file Topology.ContinuousOn #23001

This one will still need a shake, but could be delegated already. :-)

[Kim Morrison]

split long file Topology.Algebra.Group.Basic #23002

[Kim Morrison]

split long file Order.CompleteLattice #23003

[Anne Baanen]

split SetTheory/Cardinal/Basic.lean: #23014

[Anne Baanen]

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 2025-03-18T10:00:00+01:00, feel free to claim it instead :)

[Anne Baanen]

(WIP, feel free to take over while I'm away!): split Ordinal/Arithmetic.lean: #23017

[Kim Morrison]

chore: split long file MeasureTheory/Function/LpSeminorm #23036

[Anne Baanen]

split Ordinal/Arithmetic.lean: #23017 should now be ready for review.

[Anne Baanen]

partial split of Data/Set/Lattice.lean: #23098

[Anne Baanen]

partial split of Equiv/Basic.lean: #23099 (needs a shake)

[Jeremy Tan]

SetTheory.Game.PGame: #23133

[Anne Baanen]

Split Data.Set.Function: #23149

[Anne Baanen]

split iUnion/iInter from Algebra.Pointwise.Set.Basic: #23152

[Anne Baanen]

A tiny bit of progress on Algebra.Pointwise.Finset.Basic: #23156

[Jeremy Tan]

Order.UpperLower.Basic: #23248

[Jeremy Tan]

Order.Hom.Lattice: #23249

[Jeremy Tan]

Order.LiminfLimsup: #23250

[Jeremy Tan]

Data.Seq.WSeq: #23294 (still trying to see if there are any more good splits at time of posting)

[Jeremy Tan]

OK #23294 is ready

[Jeremy Tan]

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]

#23294 (Data.WSeq.Basic) is still awaiting review

[Johan Commelin]

I am working on Nobeling

[Johan Commelin]

Some tiny prerequisites:

• chore(Data/FunLike): add dite_apply and ite_apply theorems #23306

[Johan Commelin]

• chore(Algebra/BigOperators/Finsupp): add Finsupp.sum_apply'' #23305

[Jeremy Tan]

SetTheory.ZFC.Basic: #23354

[Jeremy Tan]

In #23390 I move Data.Real.EReal to Data.EReal.Basic, anticipating the split of this file

[Jeremy Tan]

Data.EReal.Basic: #23428

[Bolton Bailey]

#23429 Algebra.Group.Pointwise.Finset.Basic

[Jeremy Tan]

MeasureTheory.Function.LpSpace.Basic: #23508

[Jeremy Tan]

MeasureTheory.MeasurableSpace.Basic: #23523

[Jeremy Tan]

Data.Ordmap.Ordset: #23529

[Jeremy Tan]

Order.Interval.Set.Basic: #23556

[Jeremy Tan]

Topology.ContinuousMap.Bounded.Basic: #23574

[Jeremy Tan]

I now have four open PRs splitting long files. Would anyone like to review and merge them?

[Jeremy Tan]

Algebra.Order.GroupWithZero.Unbundled: #23620

[Jeremy Tan]

(really, the branch name for the above PR should have been gwalior)

[Jeremy Tan]

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]

MeasureTheory.Measure.Typeclasses: #23649

[Jeremy Tan]

(it seems like every time one of the splitting PRs gets merged, another one goes over the limit!)

[Kim Morrison]

Reviewers shouldn't be merging anything that increases the file length limit, please. :-)

[Jeremy Tan]

Jeremy Tan said:

(really, the branch name for the above PR should have been gwalior)

(just kidding here, of course)

[Jeremy Tan]

Algebra.Order.Floor: #23652 (pinging @Eric Wieser for pushing this over the limit)

[Jeremy Tan]

Data.Num.Lemmas: #23655

[Yaël Dillies]

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]

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]

(I read Kim's message as a joke, but to be clear yes I agree with Ruben here)

[Jeremy Tan]

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]

@Anne Baanen see my reply here and branch#ao-floor-hybrid

[Jeremy Tan]

Topology.Basic: #23717

[Kim Morrison]

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]

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]

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]

In preparation for the split of Algebra.Order.GroupWithZero.Unbundled: #23755

[Jeremy Tan]

(this just moves files, no splitting yet)

[Jeremy Tan]

Preparation for splitting MeasureTheory.Integral.Lebesgue, moving it to ...Lebesgue.Basic: #23807

[Johan Commelin]

Johan Commelin said:

I am working on Nobeling

I am relinquishing this lock. My experiment did not converge.

[Jeremy Tan]

Algebra.Order.GroupWithZero.Unbundled: #23828

[Jeremy Tan]

small chunks of MeasureTheory.Integral.Lebesgue.Basic: #23819

[Jeremy Tan]

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]

If the above "deep split" is not acceptable, I have a less ambitious split at #23855 which still clears the tech debt

[Jeremy Tan]

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]

e.g. surely lintegral_eq_zero_iff doesn't need Markov's inequality

[Jeremy Tan]

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]

Algebra.BigOperators.Group.Finset.Basic: #23897

[Jeremy Tan]

Topology.Category.Profinite.Nobeling: #23898

[Johan Commelin]

@Jeremy Tan Thanks. Could you please make all the new files refer back to .Basic for the proof idea?

[Johan Commelin]

(Just add 1 line to their module docstrings.)

[Jeremy Tan]

Johan Commelin said:

(Just add 1 line to their module docstrings.)

Done :+1:

[Jeremy Tan]

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]

Then I would split SetIntegral and then SetToL1 would be the very last split of all

[Jeremy Tan]

MeasureTheory.Integral.SetIntegral: #24070

[Michael Rothgang]

There is now a single long file left: Mathlib/MeasureTheory/Integral/SetToL1.lean :tada:

[Jeremy Tan]

MeasureTheory.Integral.SetToL1: #24075

[Jeremy Tan]

And then there were none

[Johan Commelin]

@Jeremy Tan Thanks for your great effort to push this over the finish line!

[Ruben Van de Velde]

Time to lower the cut-off

[Michael Rothgang]

#24081 tries exactly that --- if only to find out which files are still somewhat long.

[Michael Rothgang]

Among the first 1000 files, there are 11 such files.

[Jeremy Tan]

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]

An alternative implementation would be to simply remove the longFile linter option and make the linter perform the check regardless...

[Damiano Testa]

(Note: I am not suggesting that I would be happy with this hard rule!)

[Yaël Dillies]

I am strongly against making the error non-overridable. I am still dealing with consequences of past eagerly split files...

[Jeremy Tan]

I think the existing longFile linter behaviour would still be desirable for downstream projects, so I have kept it

[Michael Rothgang]

(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]

Can't wait for 50 lines long files...

[Michael Rothgang]

(deleted)

[Michael Rothgang]

Damiano Testa said:

An alternative implementation would be to simply remove the longFile linter 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]

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]

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]

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]

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]

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]

:tada: #mathlib4 > Technical Debt Counters @ 💬 :tada: