new PR approval process

Stream: general

[Rob Lewis]

Today we've said goodbye to an old friend and welcomed a new one to the community. mergify[bot] has moved on to explore new opportunities. Stepping up in its place, helping the maintainers merge your pull requests: please welcome bors[bot]! Ignore its robotic exterior. bors[bot] is very gentle and caring on the inside.

What this means to you: instead of seeing your PRs approved and tagged with a green label, you'll see the maintainers commenting bors r+. bors is more clever about queue management than mergify was. So instead of approved PRs landing on master one after the other, 1-3 hours apart, you'll notice them landing in batches. The overall wait time should be much lower. Soon The green labels will show up automatically.

leanprover-community-bot and mergify[bot] never got along very well, but mergify[bot] was too timid to stand up for itself. bors[bot] is more assertive. So you'll see leanprover-community-bot making some pull requests instead of pushing directly to master.

We owe a huge round of applause to @Gabriel Ebner and @Bryan Gin-ge Chen for setting this up! It's a huge improvement.

[Rob Lewis]

Bryan wrote a fantastic explanation of the setup, which is in the docs folder here: https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/bors.md

[Rob Lewis]

One point that's relevant for contributors. If a mantainer comments bors d+ (or bors delegate+) on your PR, it means that you can tell bors to start merging your PR whenever you're ready. You communicate this by commenting bors r+ yourself.

[Reid Barton]

Commit messages are taken from the first post of the PR. This is much nicer than mergify / Github's default which just combines all commit subject lines into one. We have set things up so that the text after "TO CONTRIBUTORS" is automatically ignored. Note that contributions from other users will have to be added explicitly to the first post with "Co-authored-by:" trailers; they aren't automatically added like how mergify and Github previously did.

:heart: :heart: :heart: It's already so much better.
When creating a PR, does Github automatically build the first post of the PR from the commit message(s) in the branch plus the contributor template?

[Patrick Massot]

I think so.

[Bryan Gin-ge Chen]

One more important change worth announcing here: Previously with mergify, it was OK to add commits to a PR with the "ready-to-merge" label. Now, if you add commits to a PR after it's been approved with bors r+ then the approval will be canceled and someone will have to re-approve it.

[Kevin Buzzard]

To be honest that sounds like a step in the right direction!