PR labels

Stream: general

[Johan Commelin]

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]

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]

Exactly...

[Johan Commelin]

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

[Johan Commelin]

author-action-required

[Johan Commelin]

@maintainers :ping_pong:

[Anne Baanen]

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]

My only dislike of that label name is its length

[Johan Commelin]

Would action-requested be ok?

[Eric Wieser]

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

[Johan Commelin]

Aha, sounds good to me

[Rob Lewis]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

I'm already really pleased with the change!

[Johan Commelin]

Can we rename it to aiting-on-authorw?

[Rob Lewis]

anticipating-author-response?

[Johan Commelin]

author-where-are-you?

[Scott Morrison]

awaiting-author?

[Johan Commelin]

Done.

[Johan Commelin]

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

[Rob Lewis]

awaiting-reviewer is the obvious one, hah

[Johan Commelin]

Ok, I like awaiting-review

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

PR number or it didn't happen

[Patrick Massot]

#4145

[Patrick Massot]

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

[Johan Commelin]

Still, I like its label (-;

[Patrick Massot]

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]

@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]

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]

Those new labels are so pretty I opened 4 PRs.

[Patrick Massot]

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

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

not to be confused with please-adopt

[Kevin Buzzard]

exactly

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

await-review and await-author-act

[Johan Commelin]

Not proper English, but it gets the message accross?

[Jalex Stark]

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]

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

[Ruben Van de Velde]

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

[Eric Wieser]

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

[Eric Wieser]

Or alphabet ones like status: