Advice about pushing PR to mathlib

Stream: maths

[Antoine Chambert-Loir]

I need advices about the reasonable way to push to mathlib my work on the Jordan theorem (for symmetric groups), the Iwasawa criterion and simplicity of the alternating group which is at branch#acl-Wielandt .

One intermediate result is of independent interest but fairly long (3000 lines), contained in https://github.com/leanprover-community/mathlib/blob/acl-Wielandt/src/acl-sandbox/group_theory/jordan/conj_class_count.lean : it studies the centralizer of a permutation, shows that it is a semi-direct product of a product of symmetric groups (on the cycle factors of given size) by a product of cyclic groups, and, as a consequence, derives the classical formula for the number of permutations of given cycle type. In a second file https://github.com/leanprover-community/mathlib/blob/acl-Wielandt/src/acl-sandbox/group_theory/jordan/conj_class2.lean, I prove the criterion for two alternating permutations of same cycle type to be conjugate in the alternating group (at most one cycle of each length, all odd, and at most one fixed point).

(I can't find the way do point directly to a theorem of a given branch/file… the counting result is equiv.perm_with_cycle_type_card, at line 3689)

[Scott Morrison]

A few comments:

• Your line counts are overestimates, as your files have large sections of comments that presumably will be dropped.
• Nevertheless the files probably each need to be split into several parts.
• You should begin PR'ing the background material. Your section boundaries might be good approximations of how much to PR at a time.
• Your imports are nearly completely ported to mathlib4. You should work out what is missing, and consider just PR'ing directly to mathlib4. You can run your files through mathport "one shot" to (optimistically) translate them to Lean 4.

[Kevin Buzzard]

Just to stress this: mathlib4 is not open to refactors but will certainly accept PRs which eg add new files

[Eric Rodriguez]

if we're adding new files that are based on existing lean3 files, surely it's just easier to add them to mathlib3 and let them be run through mathport there?

[Ruben Van de Velde]

Getting the mathport output is easier, but it means two pull requests for the author to make and for the maintainers to review rather than one

[Eric Wieser]

There's no obligation for the author to make the (edit: not forward-) porting PR; and optimistically, all they need to do is run start_port.sh (which generates a PR that is trivial to review)

[Kevin Buzzard]

If you can't translate your own code into lean 4 then just run mathport oneshot on it. PRing to mathlib3 adds an unnecessary extra layer

[Eric Wieser]

I don't fully agree. The reviewing experience is better for mathlib3 (due to github annotations and lean --json not working in Lean 4), and when someone says "oh this lemma belongs in another file" then you don't end up with random lemmas missing from mathlib3

[Scott Morrison]

Yes, but we really want to close off the mathlib3 PR pipeline sooner rather than later, and I think this outweighs ergonomic issues about reviewing.

[Ruben Van de Velde]

It's probably a good idea to improve mathlib4 ergonomics anyway, if that's a blocker

[Yury G. Kudryashov]

IMHO, until we formally declare a deadline for closing mathlib3 for PRs, authors (esp. those who have no experience with PR review etc) are welcome to make PRs to mathlib3 if they want.

[Yury G. Kudryashov]

@Antoine Chambert-Loir You may start with small PRs. E.g., a couple of lemmas that were missing in an existing file. Or all your lemmas about cardinal.to_part_enat.

[Yury G. Kudryashov]

Be prepared that reviewers will ask you to rename lemmas, move them to other files, adjust formatting to mathlib style etc.

[Yury G. Kudryashov]

Also be prepared that reviewers will golf your proofs a lot. E.g., your le_stabilizer_iff is just iff.rfl.

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

Antoine Chambert-Loir You may start with small PRs. E.g., a couple of lemmas that were missing in an existing file. Or all your lemmas about cardinal.to_part_enat.

I am completely lost in front of the task and how to do even just that.
Should I put it in a new file ? otherwise, in which one?
(Should I write the mathlib4 file ?
Or shouldn't I convert everything to lean4 now that the port is almost done?)
What if, in a later review, people observe that these lemmas are not so useful?

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

Also be prepared that reviewers will golf your proofs a lot. E.g., your le_stabilizer_iff is just iff.rfl.

Nobody's ever enough prepared for that, but in this case I'm not sure that this lemma can just be proved by iff.rfl.

[Eric Wieser]

What if, in a later review, people observe that these lemmas are not so useful?

Even if they're not ultimately useful to the end result you're working on (i.e. because you found a shorter proof), usually the sort of helper lemmas you build along the way belong in mathlib anyway; especially if their statements are very simple.

[Antoine Chambert-Loir]

OK, so let's try as @Yury G. Kudryashov suggested!
The easiest way is to go step by step, open inga new branch with just the intended few files?

[Eric Rodriguez]

yes, even a single file at a time can often be good, because PRs of that form are both easy to review and edit

[Eric Rodriguez]

editing PRs with multiple files that depend on each other can end up being a yellow bar of hell invitation...

[Eric Rodriguez]

(but sometimes unavoidable)