Zulip Chat Archive

Stream: general

Topic: PR labels


Johan Commelin (Sep 12 2020 at 05:33):

Sometimes, as reviewer, I want have reviewed a PR, and I'm quite happy with it. But I would like to ask the author a thing or two... not really changes, just some extra info, or their thoughts on an issue.
In such a case I don't add the changes-requested label, because it doesn't really seem fit.
Should we add a new label along the lines of response-requested or questions-for-author?

Pros: having such a label is a clear flag for the author that the PR requires some action on their side. Maybe I would even remove the request-review label, when adding this label.

Cons: We already have a lot of labels.

Scott Morrison (Sep 12 2020 at 05:52):

I think changes-requested is still reasonable as a catch all: "the ball is in your court". Although I agree that sometimes it seems too "aggressive" --- often I've asked "should it be like X, or like Y", where I'm happy to accept either answer if there's an explanation, but putting changes-requested can seem to imply "not-whatever-it-is-currently".

Johan Commelin (Sep 12 2020 at 06:11):

Exactly...

Johan Commelin (Sep 12 2020 at 06:11):

I'm also happy with changing changes-requested to something that sounds less aggressive

Johan Commelin (Sep 12 2020 at 06:11):

author-action-required

Johan Commelin (Sep 14 2020 at 07:17):

@maintainers :ping_pong:

Anne Baanen (Sep 14 2020 at 09:06):

I agree, renaming the label to something like author-action-required better indicates our intent.

If we change the name, it will also change on all the labeled issues, right? Then I'd say just go ahead and rename the label, we can always change it back.

Johan Commelin (Sep 14 2020 at 09:10):

My only dislike of that label name is its length

Johan Commelin (Sep 14 2020 at 09:10):

Would action-requested be ok?

Eric Wieser (Sep 14 2020 at 09:13):

I've seen waiting-on-author used before too

Johan Commelin (Sep 14 2020 at 09:14):

Aha, sounds good to me

Rob Lewis (Sep 14 2020 at 09:14):

waiting-on-author sounds better to me. action-requested could mean "requested from reviewers."

Eric Wieser (Sep 14 2020 at 09:14):

(which i saw used here: https://github.com/numba/numba/labels)

Johan Commelin (Sep 14 2020 at 09:15):

See https://github.com/leanprover-community/mathlib/pulls

Johan Commelin (Sep 14 2020 at 11:52):

The big downside that I've discovered is that w is towards the end of the alphabet...

Johan Commelin (Sep 14 2020 at 11:52):

I wish github sorted PR labels by how often they are applied

Scott Morrison (Sep 14 2020 at 12:00):

I'm already really pleased with the change!

Johan Commelin (Sep 14 2020 at 12:01):

Can we rename it to aiting-on-authorw?

Rob Lewis (Sep 14 2020 at 12:04):

anticipating-author-response?

Johan Commelin (Sep 14 2020 at 12:04):

author-where-are-you?

Scott Morrison (Sep 14 2020 at 12:08):

awaiting-author?

Johan Commelin (Sep 14 2020 at 12:11):

Done.

Johan Commelin (Sep 14 2020 at 12:11):

If we can pull off a similar trick with request-review, then I'll be one very happy PR-labeler.

Rob Lewis (Sep 14 2020 at 12:15):

awaiting-reviewer is the obvious one, hah

Johan Commelin (Sep 14 2020 at 12:16):

Ok, I like awaiting-review

Johan Commelin (Sep 14 2020 at 12:17):

https://github.com/leanprover-community/mathlib/issues/labels look at those two cute labels at the top

Johan Commelin (Sep 14 2020 at 12:19):

https://github.com/leanprover-community/leanprover-community.github.io/pull/128

Patrick Massot (Sep 14 2020 at 12:30):

They are so cute I opened a PR just to try them out.

Johan Commelin (Sep 14 2020 at 12:31):

PR number or it didn't happen

Patrick Massot (Sep 14 2020 at 12:33):

#4145

Patrick Massot (Sep 14 2020 at 12:34):

I doubt you'll find this one to your taste.

Johan Commelin (Sep 14 2020 at 12:35):

Still, I like its label (-;

Patrick Massot (Sep 14 2020 at 12:36):

You should re-learn measure theory though. I forgot almost everything before I started on this long series of PR because I wanted to differentiate under the integral sum.

Johan Commelin (Sep 14 2020 at 12:37):

@Patrick Massot said (at #4145)

Those two lemmas, as well as measurable_norm and integrable_norm sound a bit silly. But integration theory is full of lemmas requiring measurability and integrability of many functions, and those proofs really get out of control quickly, so every shortcut is precious.

Ouch... from my brief experiment with integrals in Lean... I know that this is painful.

Patrick Massot (Sep 14 2020 at 12:38):

I'm not too worried about the big picture here. We know that one day we'll have tactic like continuity for measurability and integrability. I'm not pushing because continuity is so slow that I usually write the proof by hand anyway, but one day it will be fast enough :four_leaf_clover:

Patrick Massot (Sep 14 2020 at 13:42):

Those new labels are so pretty I opened 4 PRs.

Patrick Massot (Sep 14 2020 at 13:43):

Now I'm stuck, the next ones will rely on those 4 PRs so I can go back to real work.

Sebastien Gouezel (Sep 14 2020 at 14:19):

Patrick Massot said:

Now I'm stuck, the next ones will rely on those 4 PRs so I can go back to real work.

ok, you can come back to imaginary work now.

Kevin Buzzard (Sep 14 2020 at 17:05):

So does awaiting-author look like the PR needs an author?

Mario Carneiro (Sep 14 2020 at 17:17):

not to be confused with please-adopt

Kevin Buzzard (Sep 14 2020 at 17:28):

exactly

Johan Commelin (Sep 14 2020 at 17:29):

Feel free to suggest something better. But make sure it starts with an a (-;

Johan Commelin (Sep 14 2020 at 17:29):

I want to exploit the "a"-bug for github labels.

Kevin Buzzard (Sep 14 2020 at 17:33):

I think awaiting-author-response is better but is it too long?

Johan Commelin (Sep 14 2020 at 17:35):

It is long. But maybe clear and long is better than short and ambiguous.

Johan Commelin (Sep 14 2020 at 17:35):

It's not something we have to type, so that's fine. But it might clutter the PR page

Johan Commelin (Sep 14 2020 at 17:36):

await-review and await-author-act

Johan Commelin (Sep 14 2020 at 17:36):

Not proper English, but it gets the message accross?

Jalex Stark (Sep 14 2020 at 18:50):

Johan Commelin said:

It is long. But maybe clear and long is better than short and ambiguous.

certainly we feel that way about decl names

Johan Commelin (Sep 14 2020 at 18:51):

But we also truncate english words in decl(aration) names

Ruben Van de Velde (Sep 14 2020 at 20:08):

You could always go back to the previous names and prefix them with a- or 1-

Eric Wieser (Sep 14 2020 at 20:15):

Lots of projects use numeric prefixes to deal with this type of thing

Eric Wieser (Sep 14 2020 at 20:16):

Or alphabet ones like status:


Last updated: Dec 20 2023 at 11:08 UTC