No tag on a PR

Stream: mathlib4

[Yongxi Lin (Aaron)]

Is there a reason why the bot did not automatically add the tag t-measure-probability to #34298?

[David Ledvinka]

I also noticed the bot did not add the tag to #34138 and added it manually (did not report it because I thought maybe it was just some one off mistake).

[Weiyi Wang]

I thought it was because I touched multiple folder when it happened to mine, but given your example it looks like something else

[Jon Eugster]

Thanks for reporting them, it's useful to have a list of PRs where this happens!

[Jon Eugster]

David Ledvinka said:

I also noticed the bot did not add the tag to #34138 and added it manually (did not report it because I thought maybe it was just some one off mistake).

This one had multiple applicable labels, so it didn't add anything:

Notice: Applicable labels: #[t-algebra, t-measure-probability]
Notice: not adding multiple labels: #[t-algebra, t-measure-probability]

This is something I plan to address in #34066 and follow-ups, i.e. that in this combo t-algebra should be dropped from the list because t-measure-probability "depends on it" or "has higher priority".

[Jon Eugster]

Yongxi Lin (Aaron) said:

Is there a reason why the bot did not automatically add the tag t-measure-probability to #34298?

This one is a mystery... the log looks like it found t-measure-probability and it did apply the label, or at least the curl command did get executed which creates the label (in replacement of using gh). So my guess is that the curl-command is broken, didn't get through or got interrupted somehow, idk.

[Yongxi Lin (Aaron)]

#34298 depends on #34289, which is sth about algebra. Maybe this is one of the causes (similar to #34138)?

[Jon Eugster]

Ah yes, your right, thanks. I looked into the wrong logs.

https://github.com/leanprover-community/mathlib4/actions/runs/21274901161/job/61232602054

this is the run which adds the labels which has indeed Applicable labels: #[t-algebra, t-measure-probability].

I got confused because I just looked at CI from the first commit in the PR (which added t-measure-probability but to a different PR, name the one it depends on), the "first" commit of this PR is somewhere in the middle.

So nothing bugged out here :D

[David Ledvinka]

Is it not better to just add both tags rather than none since reviewers may use the tags to determine what to review?

[Michael Rothgang]

One issue with this are tracking PRs: if a PR has dependencies, these may cause the parent PR to grow tags that are no longer relevant once the dependencies are merged. PRs are not auto-relabeled after the initial opening.

[Michael Rothgang]

I think #34066 is a good approach. In any case, authors can always override these choices.

[David Ledvinka]

I don't think there is currently a way to add these tags for contributors who don't have the ability to manually remove tags (from the branch days). I just did a test and it seems carleson, FLT work etc... but not data or t-data.

I guess adding a way to add and remove these (or writing the syntax on the documentation page if it does exist) would fix the issue.

[Jon Eugster]

indeed, automabelling always worked under the assumption that the author has the permission to set/remove the tags manually:eyes:

[Jon Eugster]

David Ledvinka said:

I don't think there is currently a way to add these tags for contributors who don't have the ability to manually remove tags

#34504 added all topic labels, so writing t-data or -t-analysis should work now. #34683 proposes to add even more labels to be managed through comments.

The functionality and available labels are documented under Contribute: Lifecycle of a PR