Zulip Chat Archive

Stream: new members

Topic: splitting 3590 ?


view this post on Zulip Anatole Dedecker (Aug 02 2020 at 13:15):

I have a few questions about how to manage PR #3590 : as you can see on GitHub, it is becoming quite big (especially if I include the code Patrick suggested), and some parts don't really fit together anymore. In this case, is the best practice to abandon this PR and make smaller ones containing the same things ? Or should I move some parts to other PR and keep this one as the final one ?

Btw, I'm asking here because Patrick seems to be in holidays and I don't want to bother him with this :sweat_smile:

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 14:45):

I am not a maintainer, but my understanding is that the PRs which are hard to review are ones which change 20 files (not 2) or the ones which add 1000 lines (not 200). So I wouldn't be too worried right now...

view this post on Zulip Anatole Dedecker (Aug 02 2020 at 14:59):

Kevin Buzzard said:

I am not a maintainer, but my understanding is that the PRs which are hard to review are ones which change 20 files (not 2) or the ones which add 1000 lines (not 200). So I wouldn't be too worried right now...

Thanks ! The only problem remaining is I created a branch for a new PR (extend_from_subset) that I don't need anymore, and I can't find how to delete it on GitHub :sweat_smile:

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:00):

https://github.com/leanprover-community/mathlib/branches

view this post on Zulip Reid Barton (Aug 02 2020 at 15:01):

what is this black magic

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 15:01):

I learnt that trick from Rob "how about some of you delete your mathlib branches, we now have 300" Lewis' message from a couple of weeks ago.

view this post on Zulip Reid Barton (Aug 02 2020 at 15:02):

I was about to explain how to do it from the git CLI

view this post on Zulip Yury G. Kudryashov (Aug 02 2020 at 20:04):

In Emacs magit you just press b k (it shows help after b), then choose origin/branchname.

view this post on Zulip Notification Bot (Aug 03 2020 at 02:44):

This topic was moved by Scott Morrison to #PR reviews > splitting 3590 ?


Last updated: May 14 2021 at 13:24 UTC