github mathlib repo tag q

Stream: general

[Kevin Buzzard]

I've only just noticed that I can change the tags on my mathlib PR's. I currently have three PR's, all tagged "changes requested", and I made the changes. Is it then Ok to remove these tags, or should it just be maintainers who tag stuff?

[Johan Commelin]

No, it's appreciated if you remove the tag and add request-review

[Kevin Buzzard]

So just to be clear (it's the holidays and I'm trying to get into the habit of making more PR's when I find holes and generally being a good mathlib person) -- if I make a PR (typically it will be small or a docstring PR), I tag it with "request-review" and then one or more people make some comments, and maybe someone changes the label to "changes requested", and then if I can deal with all the changes requested I push again and then change the tag back to "request-review"? The last thing I want to do is to start being annoying with tags, I've never used them before and haven't been watching how the community has adopted them.

[Bryan Gin-ge Chen]

That looks right. I think it'd be hard to be annoying with tags unless you started setting a bunch of random PRs to "ready-to-merge".

[Scott Morrison]

Yes, I think it's super helpful if everyone is proactive (and "optimistic") about changing tags. I often filter by tags to find what needs looking at.

[Scott Morrison]

Similarly, I think it's great if PR authors click "resolve conversation" themselves, for anything that feels safe. It's always confusing if you come in as a second reviewer, and have to read conversations to decide whether they are resolved or not.