split Nat/Prime.lean

Stream: mathlib4

[Ralf Stephan]

I'm planning to split Data/Nat/Prime.lean into its own directory. Motivation is that Factorization/Basic imports Data/Nat/Prime.lean and I have a new lemma for Prime that needs stuff from Factorization/Basic, but that lemma (and many others) certainly does not belong in the main Prime that gets imported for the Prime definition. Prime.lean is simply ripe for splitting IMO. I would like to hear opinions on the whole matter, and pointers to documents or threads are highly appreciated, as this would be my first maintenance attempt.

In Detail, I think a case can be made to have:

Nat/Prime/
+-- Basic.lean
+-- MinFac.lean
+-- Infinitude.lean
+-- Misc.lean

Is there consensus for names like Misc, Lemmas, Other, or such?

[Kim Morrison]

Generally we prefer Defs / Basic / Lemmas as the "generic" names.

[Kim Morrison]

(And I am strongly in favour of, where possible, splitting definitions into Defs files, which then depend as little as possible --- but no less --- on non-Defs files.)

[Ralf Stephan]

So I propose

Nat/Prime/
+-- Defs.lean
+-- Basic.lean
+-- MinFac.lean
+-- Infinitude.lean
+-- Lemmas.lean

[Michael Rothgang]

Ralf Stephan said:

So I propose

Nat/Prime/
+-- Defs.lean
+-- Basic.lean
+-- MinFac.lean
+-- Infinitude.lean
+-- Lemmas.lean

Looks reasonable, on first glance. (If Basic and Lemmas are meaningfully different or should rather be merged is not something I can judge without looking at the files. A reviewer will certainly opine on this :-))

[Ralf Stephan]

The criterion could be whether a lemma is used or not.

[Eric Wieser]

One option to speed up (at least partial) review might be to not do all the splits at once

[Kevin Buzzard]

Note that any PR splitting files should make no changes other than splitting the files, ie don't add your new lemmas at the same time. The tedious part of splitting is that you need to create new copyright headers and this is typically done by looking at git history (probably in this case in both the lean 3 and lean 4 repos).

[Eric Wieser]

I do wonder if we should switch to using Copyright mathlib contributors, but I guess we still want to maintain the Authors list which can be helpful for requesting reviews

[Kim Morrison]

Kevin Buzzard said:

Note that any PR splitting files should make no changes other than splitting the files, ie don't add your new lemmas at the same time. The tedious part of splitting is that you need to create new copyright headers and this is typically done by looking at git history (probably in this case in both the lean 3 and lean 4 repos).

I would like to promulgate the following rules for copyright headers:

• It's okay to simply reproduce the copyright header of the file you are splitting. (After all, it sufficed before the split, for the same content.)
• Forensics into git history should be entirely optional, but welcome.

[Matthew Ballard]

Can Copilot chat help here?

[Kevin Buzzard]

Looking forward to seeing it make up some random people in the lean community.

[Matthew Ballard]

This is assuming it has access to the git history for mathlib and mathlib4

[Matthew Ballard]

No. It doesn’t

[Ruben Van de Velde]

Yeah, that seems like a bad idea

[Eric Wieser]

Maybe a compromise is a "needs-archaology" label for PRs where the archaeology has been skipped? Then either someone else can come along before they're merged, or do a cleanup pass after (removing the label either way).

[Ralf Stephan]

Or, anyone that appears in git blame?

[Kim Morrison]

A tension here is that the authors line has always been ambiguous --- it is somewhere in between

• capture everyone who has touched this file
• identify the people who promise to be available long term to help maintain and update this file

[Kim Morrison]

The first would be ridiculous for many files. (I suspect I have touched every file in Mathlib. :-)

[Kim Morrison]

The second goes too far in ignoring significant contributions.

[Kim Morrison]

But the truth is that we are in some ill-defined compromise between the two of these.

[Mario Carneiro]

I think I would phrase it as "these are people who contributed significantly to the file" (with an emphasis on mathematical contributions, and specifically excluding updates from large scale refactors caused by changes to an earlier file or upstream)

[Mario Carneiro]

it should be a subset of the first bullet but it's probably incomparable with the second

[Mario Carneiro]

also it includes people who contributed significantly to an earlier version of the file, even if their contributions are no longer visible due to a subsequent major refactor

[Yaël Dillies]

I agree with Mario's interpretation. If we wanted to improve clarity, we could have both "Authors" and "Maintainers"/"Owners" (in the style of codeowner)/"Referent"/"Keeper"/however we want to call the people who take responsibility for a file

[Ralf Stephan]

Please review #14286.

[Ralf Stephan]

I'm now adding a second PR that only moves 4 theorems from Prime/Basic to Prime/Defs to enable changing the import in Data/Nat/Factors to Prime/Defs. It's remarkable by how many modules Factors is indirectly imported, so this should be worth the effort, besides resolving my circular dependency problem.