Steps after first approval in pull request?

Stream: mathlib4

[Sabbir Rahman]

Hi, I created a PR yesterday and it was approved by a reviewer. Reading up on https://leanprover-community.github.io/contribute/index.html , I was under the impression that a maintainer-merge label will be added to the pr. But that didn't happen, am I missing any steps? It's my first time, so not sure

[Vasilii Nesterov]

"Approve" in these guidelines actually means "respond with maintainer merge," not a GitHub approval. Could you give a link to your PR?

[Scott Carnahan]

Permission to apply the maintainer-merge label is limited to a select class of people. If you want to bring your PR to their attention, I think it is best to use the "PR reviews" channel.

[Kyle Miller]

Rough steps for approval, minus intervening steps where a PR goes through cycles of improvements:

• If someone in the community thinks the PR is ready, they can use the GitHub interface to approve it. This can also be a mathlib reviewer or a mathlib maintainer who does this, if they might want someone else to look at it.
• If a mathlib reviewer sees it and thinks it is ready to merge, they give it a maintainer merge, which puts it into a queue for maintainers to take a quick look and merge.
• If a mathlib maintainer sees it and thinks it is ready to merge, they give it a bors merge, which tells the bot to put it on the merge queue.

Mathlib reviewers and maintainers pay attention to community approvals — and anyone is welcome to review that way. People who leave good reviews can be invited to become trusted mathlib reviewers.

[Sabbir Rahman]

here's the PR link https://github.com/leanprover-community/mathlib4/pull/22588

[Sabbir Rahman]

"Approve" in these guidelines actually means "respond with maintainer merge," not a GitHub approval. Could you give a link to your PR?

understood, maybe the community article could reflect this in a better way

[Sabbir Rahman]

• If someone in the community thinks the PR is ready, they can use the GitHub interface to approve it. This can also be a mathlib reviewer or a mathlib maintainer who does this, if they might want someone else to look at it.
• If a mathlib reviewer sees it and thinks it is ready to merge, they give it a maintainer merge, which puts it into a queue for maintainers to take a quick look and merge.
• If a mathlib maintainer sees it and thinks it is ready to merge, they give it a bors merge, which tells the bot to put it on the merge queue.

ok, I was just afraid if I missed any step that caused the lifecycle to stop.

[Kevin Buzzard]

What causes the lifecycle to be slow is just the fact that as well as your PR there are 1300 other PRs.. That's the real fact of life :-( When I make a PR I just sit and wait. I've had PRs which have sat unreviewed for a month and then just randomly get merged. I'm not in a hurry though so this is ok.

[Kyle Miller]

20 hours is a young PR, everything is ok :-)

All you need to make sure of yourself are (1) that CI is passing, which it is, and (2) that there aren't any labels that indicate the PR is waiting you, like awaiting-author.

The new-contributor tag will help push you to the front of the queue.

By the way, I removed easy. It's best to leave that one alone until you know what counts as easy (fixing typos are definitely easy). This one lemma you're adding could take a couple minutes to evaluate.

[Michael Rothgang]

A small trick: this webpage will show all your pull requests (which are not marked as draft), and if there's anything preventing it from being on the review queue.

[Sabbir Rahman]

I think the main confusion came from my part due to not knowing there are 3 kinds of approvals. Reading the contribution guideline I assumed there were 2 kinds of approvals

[Jon Eugster]

I've recently had a discussion with somebody about the exact same confusion. I think it would be good to update https://leanprover-community.github.io/contribute/index.html and be more deliberate with the usage of the word "approve"

[Yaël Dillies]

Sorry, I was the one writing those paragraphs

[David Loeffler]

In this community we tend not to use GitHub's own "approval" button at all, so we tend to forget it exists. Anyway, I have maintainer-merged the PR.

[Yaël Dillies]

I will rephrase the contribution guide

[Pim Otte]

I took the liberty of proposing a modified text in this PR

[Michael Rothgang]

Thanks a lot; I took a detailed look a your PR.