Workflow for contributing several lemmas

Stream: mathlib4

[Vasily Ilin]

I want to contribute several lemmas to mathlib 4 that depend on each other. I have several choices, and would like to know which one is best (they all seems suboptimal):
1) Make a series of small PRs that depend on each other. Drawback: if a reviewer suggests a change to the root lemma, I will need to change each PR in the chain.
2) Make the first PR, wait till it's merged, then open the second PR, etc. Drawback: since it seems to take about one day to approve the PR and another day for Bors to merge it, I am looking at about a week of daily back-and forth for a series of 3 contributions. That's a lot of context-switching.
3) Make one medium-size PR with all the lemmas in it. Drawback: potentially longer review time.

I understand that 1) or 2) are the recommended workflows but they both introduce quite a bit of overhead for the contributor because of the context-switching (opening VSCode and remembering what's what takes a non-trivial amount of time).

[Thomas Browning]

I usually do (2), but only because I don't mind the context-switching.

[Thomas Browning]

(also, maybe this should be moved from lean4 to mathlib4?)

[Johan Commelin]

@Vasily Ilin What is the total size? If the lemmas belong to one topic, then a PR with ~300 lines of code isn't a problem.

[Notification Bot]

This topic was moved here from #lean4 > Workflow for contributing several lemmas by Johan Commelin.

[Kim Morrison]

Further, making sure you write "these lemmas are for the central limit theorem" (as you have!) significantly adds to reviewers' enthusiasm, compared to PRing the preliminary lemmas without explanation.

[Vasily Ilin]

Johan Commelin said:

Vasily Ilin What is the total size? If the lemmas belong to one topic, then a PR with ~300 lines of code isn't a problem.

Less than 300 LOC for sure!

[Johan Commelin]

In that case I would start by putting everything in 1 PR. Then people can look at the whole picture.

[Johan Commelin]

Splitting a PR at a later point won't be harder than splitting it now. So there isn't much "risk" attached to creating a PR with all those lemmas at once.

[Johan Commelin]

And good chances that it doesn't need to be split at all.