Andres Erbsen (Feb 28 2023 at 19:52): Andres Erbsen (Feb 28 2023 at 19:52):I would appreciate reviews on https://github.com/coq/coq/pull/17133, https://github.com/coq/coq/pull/17281, and https://github.com/coq/coq/pull/17022 from maintainers of btauto, stdlib, and typeclasses. I anticipate all of these being on the easy side of Coq reviews. Thanks!
Andres Erbsen (Feb 28 2023 at 19:58):Meta: the teams in question are small: 2, 5, and 2 people. I understand that input from experts of the particular domain is valuable, but it seems that currently review requests fall through the cracks every once in a while. I wonder whether there is something we can do to make contributing to stdlib smoother. Two not-that-thought-trough ideas: (1) perhaps more people could be eligible to review, with the understanding that delicate changes would still involve more experienced maintainers and (2) a (random? rotating?) system to single one team member at a time for a choice to review or pass might get evoke a more immediate response. What do you all think?
Gaëtan Gilbert (Feb 28 2023 at 20:03):1) everyone is eligible to review, the team is just the people who get auto notified
2) IDK
Théo Zimmermann (Mar 01 2023 at 09:06):Regarding 1, and @Gaëtan Gilbert's response, our contributing guide currently says:
Our CODEOWNERS file associates a team of maintainers to each component. When a PR is opened (or a draft PR is marked as ready for review), GitHub will automatically request reviews to maintainer teams of affected components. As soon as it is the case, one available member of a team that was requested a review should self-assign the PR, and will act as its shepherd from then on.
The PR assignee is responsible for making sure that all the proposed changes have been reviewed by relevant maintainers (at least one reviewer for each component that is significantly affected), that change requests have been implemented, that CI is passing, and eventually will be the one who merges the PR.
PRs are merged when there is consensus. Consensus is defined by an explicit approval from at least one maintainer for each component that is significantly affected and an absence of dissent. As soon as a developer opposes a PR, it should not be merged without being discussed first (usually in a call or working group).
It is true that in practice, we are more lenient regarding who can be an assignee and how important it is to get reviews from relevant maintainers, but we should probably clarify this in the contributing guide. In particular, I thought I would read something about the absence of reaction from component maintainers after a few days implied that the assignee could ignore their review request, but apparently, we never wrote this down.
Théo Zimmermann (Mar 01 2023 at 09:08):Regarding 2, GitHub has a feature for randomly / rotatingly selecting a team member when a team is requested a review, but I do not feel like this is convenient for a project where reviewers are volunteers with unpredictable availability. I think we should figure out a smarter mechanism to select specific reviewers or to ping relevant reviewers when no one is taking care of a PR. If we can design such a mechanism, then we can implement it using coqbot, for instance.
Andres Erbsen (Mar 02 2023 at 16:11):It is true that in practice, we are more lenient regarding who can be an assignee and how important it is to get reviews from relevant maintainers, but we should probably clarify this in the contributing guide. In particular, I thought I would read something about the absence of reaction from component maintainers after a few days implied that the assignee could ignore their review request, but apparently, we never wrote this down.
A policy along the lines of what you suggest would be very helpful if there was good agreement to follow it. Would you be willing to create a PR to codify your understanding of what you see as the desirable aspects of current practice? Thanks!
Regarding 2, I agree that respecting the volunteers' flexibility should be a priority; anything like this would require more thought and existing Github features are unlikely to be applicable. I'd be happy to give a try to any endorsed solution to (1) and the return to (2) if necessary.
Théo Zimmermann (Mar 03 2023 at 08:00):OK, I will put this on my to-do for next week. Regarding 2, I'd be willing to implement something if there is someone to co-design it. However, we should probably look into the existing first, and ensure that there doesn't already exist something that would suit our needs.
Last updated: Jun 04 2023 at 19:30 UTC