New contributor label

Stream: mathlib4

[joseph hua]

Two (possibly related) questions:

1. How can I earn the removal of the new-contributor PR label? I have several merged PRs now. I thought it would automatically be removed.
2. How can I add a topic label manually/ensure automatic label assignment? Some of my PRs, e..g #29284 is being thrown around because it hasn't been assigned to the right person. It should have t-category-theory.

[Christian Merten]

1. The label is added on the first 5 PRs of a contributor.
2. I just added the label, maybe there is some comment command to add it, but I don't know.

[Damiano Testa]

With regards to the new-contributor label: the bot should stop assigning that label once you have 5 (or maybe strictly more than 5) closed PRs.

However, it turns out that identifying automatically who you is, is tricky. The reason is that GitHub has several different places where it might try to guess what your identity is and not everyone has the same exact id on every single machine that they use.

[Damiano Testa]

So, even though it looks like you have 6 merged PRs, it may be that they are somehow associated to different "names", so it may take a little longer for the label to stop being applied.

[Damiano Testa]

With respect to the autolabelling by topic, that looks just at the first time CI runs on the PR and uses the paths to the modified files to make its decision of what label to apply.

[Damiano Testa]

If there are multiple labels that could match, it applies none.

[Damiano Testa]

So, the autolabelling works for PRs that basically touch only one file or multiple files sharing at least the same top-level dir, possibly a little more than that even.

[Damiano Testa]

If that does not apply to your PRs, you can always manually apply a label yourself.

[Damiano Testa]

The fact that the bot will not touch your PRs after the first CI run, means that your PR will not be automatically relabeled!

[Chris Henson]

I think it is that the 6th PR was merged a few hours ago, while the other open PRs are older. For instance, when it checked for your newest PR, it detected four. So I would guess it gets picked up on your next PR.

[Damiano Testa]

Ah, that would definitely explain why the label was added!

[Damiano Testa]

However, the label may also be added sometimes later. Many of the people who have been contributing for years get the new-contributor label every once in a while... :man_facepalming:

[Damiano Testa]

However, if you still get the label for your next couple of PRs, mention it, and I can take a look at what is going on.

[joseph hua]

Damiano Testa said:

If that does not apply to your PRs, you can always manually apply a label yourself.

Thanks for the detailed response. I suppose I can only add topic labels manually once I am no longer a new-contributor. (right now the gear button does not appear on the top right)

[Damiano Testa]

Ah, does it work if you comment on your PR with the name of the label that you want to add?

[Damiano Testa]

If you want to add the t-category-theory PR, a comment with just

t-category-theory

may add the label.

[joseph hua]

I tried that, but Christian Merten beat me to it by about 3 seconds.

[Damiano Testa]

I don't remember if we implemented this fully or not. It should work with some labels, though maybe not with all.

[joseph hua]

I can try in the future

[Damiano Testa]

You can try with

-t-category-theory

[Damiano Testa]

That should remove the label.

[Damiano Testa]

I see that your comment was not picked up. I'll try myself.

[Bryan Gin-ge Chen]

I'm not sure if topic labels work yet, it might just be the short list here: https://github.com/leanprover-community/mathlib4/blob/10d128b540e23ca0f27026e1663814513756b4a9/.github/workflows/labels_from_comment.yml#L28

[joseph hua]

It didn't remove the label

[Damiano Testa]

Ok, and it is not a matter of permissions, since also my comment did not remove the label.

[Jireh Loreaux]

@joseph hua I just gave you triage access, so you should be able to remove the label yourself now.

[Damiano Testa]

Ah, I had forgotten about triage access! :man_facepalming:

[joseph hua]

Thank you @Jireh Loreaux !

[Iván Renison]

In #30069 something strange happen: the label was added after a bot made an automatic commit
I have not had the new contributor label in a while now

[Damiano Testa]

Iván Renison said:

In #30069 something strange happen: the label was added after a bot made an automatic commit
I have not had the new contributor label in a while now

Presumably this is the action picking up that the bot does not have at least 5 merge PRs and is therefore a new contributor.

[Damiano Testa]

I think that this behaviour can only happen when the bot is currently the last "owner" of a commit. If you remove the label and add further commits, the label should not be added again.

[Chris Henson]

Yeah, the CI run shows it counting PRs (0) for the bot. Maybe it should be added as an exception in the script.

[Damiano Testa]

Maybe we could, but I like it that sometimes I feel young again when a new-contributor label is incorrectly applied to my PRs... :upside_down: