Zulip Chat Archive

Stream: new members

Topic: Maximum Length for a PR


Sebastian Monnet (Feb 01 2022 at 14:01):

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

Thanks!

Reid Barton (Feb 01 2022 at 14:02):

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

Reid Barton (Feb 01 2022 at 14:03):

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

Alex J. Best (Feb 01 2022 at 14:06):

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 (Feb 01 2022 at 14:08):

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

Reid Barton (Feb 01 2022 at 14:10):

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

Reid Barton (Feb 01 2022 at 14:11):

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

Arthur Paulino (Feb 01 2022 at 14:14):

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 (Feb 01 2022 at 15:41):

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 (Feb 01 2022 at 15:45):

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

Sebastian Monnet (Feb 02 2022 at 12:39):

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 (Feb 02 2022 at 12:40):

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 (Feb 02 2022 at 12:41):

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 (Feb 02 2022 at 12:41):

That sounds fine

Sebastian Monnet (Feb 02 2022 at 12:42):

Great, thanks


Last updated: Dec 20 2023 at 11:08 UTC