Let's not have big files?

Stream: mathlib4

[Scott Morrison]

I'm doing some more minimization, and ... I am a bit grumpy about some of the files in mathlib. It is not reasonable to have the definition of MetricSpace be on line 2800 of the file called MetricSpace/Basic.lean Everything before it should be in another file.

Please, all reviewers, let's start rejecting changes to files that are over 1000 lines long until they are split, or insist that when adding generalizations, files are split appropriately.

Similarly I suspect the world "archimedean" just should never appear in Mathlib.Analysis.Normed.Group.Seminorm; why is this not in its own file?

[Adam Topaz]

Should we add something to the style linter?

[Scott Morrison]

Huh, I guess we could add exceptions for the existing files, I hadn't thought of that.

[Ruben Van de Velde]

I don't disagree (at all), but do we want to do much of the splitting work during the port?

[Johan Commelin]

There's a file pretty close to the top of the unported queue with over 3000 lines... We should probably split it in 4 pieces asap.

[Johan Commelin]

I'll attempt to split analysis.calculus.fderiv

[Johan Commelin]

#18995

[Yaël Dillies]

Scott Morrison said:

Please, all reviewers, let's start rejecting changes to files that are over 1000 lines long until they are split, or insist that when adding generalizations, files are split appropriately.

Splitting files is not an easy task. I don't want to put the charge of splitting a file on a random contributor (or on a hurried contributor: I am still unhappy with some of the splits you made back in November for the sake of the port). I also don't want to set a hard limit because often the way a file should be split only becomes evident once it has a lot more material.

[Yaël Dillies]

However having online a list of big files to tackle makes sense. Then someone competent in the relevant area can do the split calmly and pertinently.

[Riccardo Brasca]

ring_theory.polynomial.cyclotmic.basic should be quite easy to split (it's a little over 1000 lines), for examples results about the roots can go to a separate files, and similar for characteristic p results. I can do it next week.

[David Loeffler]

#19004 splits up analysis.special_functions.gamma (1500 lines) into 3 chunks. It'll be a long while before the port reaches this one, but I had some changes I wanted to PR to it anyway, so I thought I'd do a split at the same time.

[Ruben Van de Velde]

I think I'd recommend against doing the split and the new code in the same PR

[David Loeffler]

Ruben Van de Velde said:

I think I'd recommend against doing the split and the new code in the same PR

Fair point: I've backed out the content changes and they can go into a separate PR once #19004 is merged.

[David Loeffler]

I am working on splitting up analysis.special_functions.pow. It divides up quite neatly into 3 sections for power operations on complex, real, and nnreal; but it is imported in a large number of other files so it is painful to work out which other files need to import which chunk.

[David Loeffler]

David Loeffler said:

I am working on splitting up analysis.special_functions.pow.

PR ready for review at #19006