bors closed a PR?

Stream: mathlib4

[Kevin Buzzard]

What just happened with #23726?

I made a suggestion, bors d+'s the PR, edited the suggestion and then this happened:

Screenshot 2025-04-22 at 16.28.07.png

Did bors really just delete master and randomly merge this PR and not mark the PR as [Merged by Bors]? Could I have pressed a wrong button?

[Kevin Buzzard]

Doesn't look like the PR is merged. Do I just reopen?

[Eric Wieser]

bors closed the base branch, and also claims to have deleted master. This happens whenever you create dependent PRs "the github way", and reopening is the correct action

[Kevin Buzzard]

Thanks for the explanation! I'd just a few minutes earlier merged the dependency.

[Junyan Xu]

The base branch was branch#fae_PR_genLT (#23725), which was merged into master and the branch is then deleted by bors. (Displaying this as master being deleted is a GitHub bug that has been there for a long time.) Once the base branch is deleted, bors closes #23726. In this case bors somehow also automatically changed the base branch to master afterwards, so you can reopen the PR immediately; this doesn't happen every time and if it doesn't happen, usually you need to manually go to #23725 to restore the deleted branch, then you can reopen the PR and delete the branch again. (Both things happened to my PRs today.)

[Filippo A. E. Nuccio]

Oh, so I guess that creating a branch from a non-master branch is not a good idea, although it is the "github way"?

[Aaron Liu]

What I do usually is create a branch from master and merge the branch I want

[Filippo A. E. Nuccio]

Yeah, that has always been my way as well, but I thought that opening a child branch from a branch looked neater. Apparently I was wrong ...

[Junyan Xu]

It happens often that you want to add materials on top of a branch A which is already PR'ed or is ready to be PR'd, in which case it's natural to create another branch B out of A. When you open a PR from branch B, it's also natural to set the base branch to A to reduce diff and ease reviews (I often do this). The GitHub/bors workflow is not exactly friendly to this approach, but we can live with it.

[Yury G. Kudryashov]

It's OK to create a new branch from a non-master branch. WHen you open a PR, you should set master as the base branch. Otherwise you tell it that you want to merge your changes into the base non-master branch, and it gets confused.

[Yury G. Kudryashov]

It would be nice to better automation for dependent PRs (show my PRs as a color-coded tree, do the right thing when the base branch is merged etc), but this is not an easy task.

[Yury G. Kudryashov]

E.g., when A depends on B and B is merged, then the right thing to do is to merge master into B (to get the same state as on master, but with the right history), then merge B into A. This is better than merging master directly, if you modify the same file both in A and B.

[Filippo A. E. Nuccio]

But all this should be done between the moment B is merged to master and it is deleted, right?

[Yaël Dillies]

Yury G. Kudryashov said:

when A depends on B and B is merged, then the right thing to do is to merge master into B (to get the same state as on master, but with the right history), then merge B into A. This is better than merging master directly, if you modify the same file both in A and B.

The better thing IMO is to rebase A over master, dropping the commits from B

[Filippo A. E. Nuccio]

Well, but as Kevin noticed (in my PR...) if Bis merged and deleted, A is automatically closed.

[Yaël Dillies]

... if the base of A is B. I personally always make the base of A be master

[Filippo A. E. Nuccio]

Yes, I agree that this seems to be the better solution: branch out from your first PR branch, but make master the base of this new branch.

[Filippo A. E. Nuccio]

And at any rate the delegation by @Kevin Buzzard is no longer valid (probably because of the closing-reopening business...)

[Kevin Buzzard]

@Filippo A. E. Nuccio I am a bit confused about the state of this PR #23726 now. We have that #23725 is merged and it contains Mathlib/Algebra/Order/Group/Cyclic.lean which is 66 lines on ordered cyclic groups. But they're still showing up in the diff of #23726 . Can you merge or rebase master (don't ask me which one) so we can see what's actually going on in the PR?

[Filippo A. E. Nuccio]

Done