splitting 3590 ?

Stream: PR reviews

[Anatole Dedecker]

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]

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]

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]

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

[Reid Barton]

what is this black magic

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Notification Bot]

This topic was moved here from #new members > splitting 3590 ? by Scott Morrison