Zulip Chat Archive

Stream: new members

Topic: splitting 3590 ?

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:

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...

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:

Kevin Buzzard (Aug 02 2020 at 15:00):

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

Reid Barton (Aug 02 2020 at 15:01):

what is this black magic

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.

Reid Barton (Aug 02 2020 at 15:02):

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

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.

Notification Bot (Aug 03 2020 at 02:44):

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

Last updated: Dec 20 2023 at 11:08 UTC