Triage role

Stream: std4

[Scott Morrison]

@Mario Carneiro, could we hand out the triage role to all contributors to Std? I think it is super helpful if authors can take responsibility for switching labels awaiting-review / awaiting-author / WIP on and off by themselves.

[Mario Carneiro]

I'm not sure there is an easy way to give it to all contributors, but I gave it to the recently active ones and anyone else can request it. I have seen this handled using a bot though in other repos, I think the triage role allows a bit more than just changing labels and also it prevents having protected labels that should only be set by a bot

[Mario Carneiro]

Thanks to std#232, we no longer need to hand out the triage role to contributors, and can stick to the usual github permissions model. To tag your PRs, just comment with awaiting-review / awaiting-author / WIP on your PRs. (Note, there cannot be anything else in the comment body, it has to be just a bare awaiting-review etc.)

[Scott Morrison]

The biggest hurdle here is going to be teaching people that this exists. Perhaps to make it easier we should all get in the habit of using this mechanism when triaging, so others can see how it works.

[Mario Carneiro]

Can the bot automatically mark new PRs with awaiting-review?

[Mario Carneiro]

We can also put some hints about this in the PR template

[Scott Morrison]

Perhaps we should add the awaiting-CI label, and have new PRs come labelled with awaiting-CI and awaiting-review, and have the same Mathlib bot that removes awaiting-CI.

[Eric Wieser]

Do we need this machinery at all? Can't we use the draft / changes requested machinery of github to track review/WIP status?

[Jon Eugster]

Mario Carneiro said:

We can also put some hints about this in the PR template

A short "how to contribute" section/page in the README.md might also be another good idea. I'm generally always searching for these on any github repo.

[Eric Wieser]

Or can only maintainers "request changes"?

[Mario Carneiro]

I agree re: draft PRs, but "request changes" is supposed to be a reviewer's response to a PR, it is not a good replacement for awaiting-review

[Mario Carneiro]

also if a maintainer requests changes, the PR author can do nothing to clear that status

[Mario Carneiro]

Anyone can "request changes" though, not only maintainers (they are shown in a different way though)

[Mario Carneiro]

I think the main advantage of the labels is that you can use them for filtering the PR list

[Eric Wieser]

You can use draft/review status for filtering too

[Scott Morrison]

The labels are much superior to draft / review status. For one, they are much visually clearer on the PR list!