PR labels as a new contributor

Stream: mathlib4

[Paul Schwahn]

In the pull request guidelines it says (emphasis mine):

On the main page for a PR, on the right-hand side, there should be a sidebar with panels "reviewers", "assignees", "labels", etc. Click on the "labels" header to add or remove labels from the current project. (Labels can only be edited by "GitHub collaborators", which is approximately the same as "people who have write access".) Anyone can edit the labels by writing the following commands in a comment on the PR (each on its own line):

• awaiting-author will add the "awaiting-author" label
• -awaiting-author will remove the "awaiting-author" label
• WIP will add the "WIP" label
• -WIP will remove the "WIP" label

I have an easy PR where I would like to add the "easy" label, but commenting "easy" on the PR did nothing. Is this because I am a new contributor? Did I misunderstand something?

[Damiano Testa]

I am not sure that easy is a label for which there is this automation. Did you try adding the label directly? It might work...

[Kevin Buzzard]

Surely nobody can add labels directly any more and the actual diagnosis is that the guidelines are out of date since we moved to the fork model.

[Kim Morrison]

Everyone who used to have write access should still have triage access, which is sufficient to add and remove labels.

[Kim Morrison]

I'm happy to give out triage access to anyone who asks.

[Damiano Testa]

It is also easy to add the automation that labels easy on comment and also add that this automation exists in the guidelines.

[Damiano Testa]

And possibly adding that the list in the guidelines is exhaustive, since it is easy to generalise that any label can be added via the same mechanism, but this is not actually what the action does.

[Kevin Buzzard]

So does this mean that future contributors should ask for triage access?

[Kim Morrison]

I'd kind of prefer to not have that overhead of responding to the requests?

[Kim Morrison]

But it's fine

[Michael Rothgang]

Damiano Testa said:

It is also easy to add the automation that labels easy on comment and also add that this automation exists in the guidelines.

We could crib an idea from the Rust project: you comment

• @rustbot author to make a PR as awaiting-author
• @rustbot ready to make it as ready for review
• something like @rustbot label -S-waiting-on-author +S-waiting-on-review to add or remove labels

(this page has more information about the possible commands). If we want to be selective about not supporting any label, that could certainly be implemented.

[Bryan Gin-ge Chen]

Here's our current label from comment workflow file; it supports exactly the commands in the list on the pull request guidelines quoted above, but as Damiano said, it would be easy to add easy :slight_smile:

[Michael Rothgang]

So new contributors cannot manually relabel their PR (say, if autolabel had a bug or a PR spans multiple areas), right? Allowing to add those seems useful.

[Bryan Gin-ge Chen]

Right, we could also add topic tags to the label-from-comment workflow.

[Artie Khovanov]

Kim Morrison said:

I'd kind of prefer to not have that overhead of responding to the requests?

I guess ultimately there needs to be some sort of change, right? Because eg new contributors wouldn't be able to remove the "awaiting author" label?

[Bryan Gin-ge Chen]

They already can by commenting "-awaiting-author" on the PR.

[Michael Rothgang]

Does that workflow have a bug, in that typing -WIP would re-add the label again?

[Michael Rothgang]

My impression is that both wip (source) and removeWip (source) would be true for a comment "-WIP"...

[Artie Khovanov]

Bryan Gin-ge Chen said:

They already can by commenting "-awaiting-author" on the PR.

Does that still work? !bench doesn't work anymore, you need to add the bench-after-CI label

[Bryan Gin-ge Chen]

Michael Rothgang said:

My impression is that both wip (source) and removeWip (source) would be true for a comment "-WIP"...

It's possible that there are bugs... I can look later.

Artie Khovanov said:

Does that still work? !bench doesn't work anymore, you need to add the bench-after-CI label

The workflow is triggered on issue_comment and doesn't require the triggering user to have any particular permissions, so the issues that affect !bench are separate.

[Paul Schwahn]

Kim Morrison said:

Everyone who used to have write access should still have triage access, which is sufficient to add and remove labels.

I think I was one of the last people who was granted write access before we moved to the fork model, but I don't think I have triage access now because I could not edit the labels.

[Paul Schwahn]

But I suppose the best solution would just be to add the "easy" label to the aforementioned workflow, right?

[Bryan Gin-ge Chen]

I'll try and expand the list of tags that the workflow can handle when I look at it. Thanks for bringing this up, by the way; I had been meaning to come back to this after adding the - functionality in #25723 but it slipped my mind.

[Damiano Testa]

#26456 restructures the previous action managing labels from comments. I kept awaiting-author and WIP. I also added easy, and nothing else.

[Damiano Testa]

My intention was to make the action easily extensible, so that adding more labels should be completely straightforward: the labels that the action manages are simply an array that forms an input to the code.

[Damiano Testa]

The current workflow for adding/removing labels should allow the following. On any comment, if a line consists of awaiting-author, WIP or easy up to whitespace, and possibly preceded by -, then the corresponding label will be added (if - is not present)/removed (if - is present).

[Damiano Testa]

If multiple lines refer to the same label, then the script will follow the latest instruction.

[Damiano Testa]

This has received very little testing, so if something does not seem to work, please report it.

[Damiano Testa]

If this works, then adding awareness to more labels should be a very simple change.