Zulip Chat Archive

Stream: general

Topic: github mathlib repo tag q

Kevin Buzzard (Apr 08 2020 at 19:07):

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 (Apr 08 2020 at 19:08):

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

Kevin Buzzard (Apr 08 2020 at 22:49):

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 (Apr 08 2020 at 22:51):

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 (Apr 09 2020 at 02:04):

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 (Apr 09 2020 at 02:05):

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.

Last updated: Aug 03 2023 at 10:10 UTC