Maximum Length for a PR

Stream: new members

[Sebastian Monnet]

Is there a maximum length for a PR? If so, what is it?

Thanks!

[Reid Barton]

This probably isn't the right question to be asking.

[Reid Barton]

If you feel the need to ask this question, then you should make your PR smaller.

[Alex J. Best]

In general, smaller / more focussed PR's will end up getting reviewed faster. So splitting up large PRs is more convenient for all involved. Some good ways to split are by file, or more generally splitting off background / general results about basic structures, splitting off definitions and basic API from the main results.

[Johan Commelin]

A ballpark estimate for preferred PR length: ≤ 300 lines.

[Reid Barton]

But still, smaller is better. So I hesitate to suggest any number.

[Reid Barton]

It also depends on the extent to which you are adding entirely new material, versus extending/refactoring existing things

[Arthur Paulino]

In the contributing guidelines, the only information about it is this:

depending on the size of the PR; smaller PRs will get quicker responses

Maybe some new contributors feel the need for a more straightforward baseline

[Stuart Presnell]

Don’t forget you can look at all the recently merged PRs that add new features to get a sense of roughly how big they are: https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+is%3Aclosed+feat

[Stuart Presnell]

It might be worth adding something to the guidelines with that link or something like it

[Sebastian Monnet]

So, I have a fairly large project that I would like to start PRing. I have defined the Krull topology on Galois groups in one file, and proved that it is profinite in another. What's the usual way to break such a project into pieces to PR? Do I create a new file and just put the lemmas and definitions in one at a time?

[Eric Rodriguez]

yeah, so you could PR the definition of the Krull topology (and basic lemmas), and then add a couple results per PR after that

[Sebastian Monnet]

The definition is still around 180 lines, since it requires quite a few lemmas - do you think that's too long for a single PR?

[Ruben Van de Velde]

That sounds fine

[Sebastian Monnet]

Great, thanks