Zulip Chat Archive

Stream: general

Topic: Pull request etiquette


Patrick Lutz (Sep 01 2020 at 19:12):

Recently I was part of a PR to mathlib. It has gone through the usual round of request review, changes requested, making the necessary fixes and then back to request review. But that's where it's been sitting for the past few days. What's considered the best practice in this situation? Should I ping the reviewers in some manner (either on here or on github)? Should I just wait longer? If "wait longer" is the appropriate response that's fine with me, I just want to check what the norms of this community are.

Kenny Lau (Sep 01 2020 at 19:13):

which PR?

Patrick Lutz (Sep 01 2020 at 19:13):

#3913

Mario Carneiro (Sep 01 2020 at 19:14):

There are a lot of open PRs, and the ones with people actively working on them get more attention. So don't be afraid to ping, especially if you know someone in particular who is well suited to review

Patrick Lutz (Sep 01 2020 at 19:15):

Is it best to ping here or on github? Or does that depend on the person you're pinging?

Mario Carneiro (Sep 01 2020 at 19:16):

Either is fine

Johan Commelin (Sep 01 2020 at 19:18):

@Patrick Lutz Note that there is a dedicated stream for PR reviews. That would be a perfect place for pinging. :ping_pong:

Mario Carneiro (Sep 01 2020 at 19:22):

Right now @Johan Commelin and @Anne Baanen are still listed as "changes requested" in the github UI, I guess because the last review they gave was changes-requested. It's probably best to first ping these people to see if they no longer suggest any changes

Patrick Lutz (Sep 01 2020 at 19:22):

I've pinged @Anne Baanen in the PR stream.


Last updated: Dec 20 2023 at 11:08 UTC