Pull request policy

We have talked a lot about issue and pull request triage recently, especially in the last Coq working group. Since @SkySkimmer is currently closing lots of stale PRs, I’d like to share this draft of a PR policy that I have recently prepared. It relies heavily on the newly introduced GitHub “draft PR” feature. The idea is that when you create a PR, you can mark it as draft, in which case it won’t trigger automatic review requests until you mark it as ready for review. It should allow us to reduce noise quite efficiently and solve the problem of stacked PRs.

Here is the proposal:

  • Pull requests are a good way to communicate about work in progress: the use of draft pull requests is encouraged for any actively developed branch on a developer’s fork (even if it is far from being ready, and even if it contains lots of commits).
  • Pull requests must be opened in draft state until all relevant checkboxes (of the PR template) are checked. In particular, no feature should be marked as ready for review without complete, precise and accurate documentation.
  • If it turns out that a PR in review state is not ready for review, it should be closed and reopened as draft. In particular, we get rid of the needs: review label, and the needs: progress, needs: independent fix, and needs: feedback labels are reserved to draft PRs.
  • The use of stacked PRs is discouraged. Instead, the developer should use draft PR pointing to a single branch with possibly many commits, and only split up into multiple simpler PRs when ready for review (one PR ready for review at a time, no stacked ready for review PRs). In particular, we get rid of the needs: merge of dependency label.
  • Draft pull requests that do not represent actively developed branches only create noise: PRs corresponding to branches that are not pushed to for 30 days are closed (we could also say 3 months, which would correspond to GitHub’s definition of stale branches). The author is then encouraged to use an alternative form to record the idea: new issue, documentation, Discourse post or blog post that can be linked to from a relevant issue or piece of documentation…
  • PRs in review that create too much discussion (more than 50 comments, maybe an even lower number) are either not ready and should be closed and reopened as draft, or require fundamental discussion and should be closed and reopened as CEPs / RFCs, or as Discourse posts if they are not yet ready to become CEPs. In particular, we get rid of the needs: discussion label.

We can start discussing and experimenting this policy, and if we like it we can enact it on the next Coq working group. @coqbot could also help automatically closing pull requests following the above criteria.

1 Like

I like most of the things here, but I disagree with this one. A single review on documentation can create maybe 20-30 very small comments (“change the tense of this word”, “use this form instead of that form for proper grammar”, “clarify this sentence”, etc.). I think comments of this form, where there is no objection to the PR, just minor suggestions, should not count as “too much discussion”

It is indeed a nice document, thanks @Zimmi48. Similarly to @JasonGross, I like the spirit of the document; here are my comments:

  • first, I am not sure we should move development discussion here; this is key policy and not all devs are here; IMVHO, this discussion belongs to a GitHub issue. It is not like Discourse is giving us any advanced stuff here, like threading.
  • regarding the closing and reopening of PRs, I am not sure I like that as a norm, except for very specific cases. IMHO if the PR needs work, it should be completed in a reasonable timeframe. Unless the author wants indeed to move to a draft state. Closing PRs, triggers all kind of spurious notifications. It would be different if GH would allow to downgrade to Draft without closing.
  • the case for stacked PRs is complex, I would be more flexible here, but in principle yes, I do agree that while not perfect using a draft PR seems better than what we do now. But having all the eggs in one basket is dangerous game for people working in the scope that I work; usually you want to have 1 PR per feature. @herbelin used to have large branches and he paid for it.
  • the rule of 30 days to close is IMHO too strict. For example I have some non-draft pull request that are not worth to rebase due to conflicts with PRs likely to be merged before. They should also be not closed. When you have the very slow merging process we have you cannot punish PR authors like that. The lack of review/merge is in fact an extremely more serious problem than the one we are dealing with here [having too many open PRs] Also, some work just takes time, for example the work on proof global took 10 months of continuous work, Dune also took many months.
  • I am not sure why a PR generating discussion is bad, on the contrary, it is a good sign; so here I am lost.

After a bit more thinking, the proposal is IMO too complex for the problem that is solving (PR overpopulation), which is, TTBOMK, pretty minor.

A terser alternative could be:

A Pull Request should be submitted as draft when: a) it is not ready for review but you want to announce the work; b) documentation or test-cases are still missing; c) it depends on other, not yet merged PRs and thus would create review spam

Another minor point: it seems I cannot close a PR and reopen it as a draft. This is very inconvenient.

Here is the list of all the PRs with the largest number of comments. The fact that most were eventually merged seems to indicate indeed that counting the number of comments is not the right tool to decide when a PR should be moved back to the CEP stage. However, I do still think that we have a tendency to have design discussions in PR thread, which tends to lose the focus on the review of the implementation (leading to accepting things that were not reviewed as carefully when the design discussion ends) and we should try to make sure the design discussion happens more often before a PR is opened.

GitHub provides us PRs and a bug tracker. There are many kinds of discussions that are not suited for either (typically discussions that are not expected to be “closed”, such as support questions and open discussions). I’m just using Discourse like I would be using a mailing list. If there is any hope that the Discourse forum will subsume the Coqdev mailing list, it needs all the developers to be here (I don’t see why this couldn’t be the case). Following the development category of the Discourse forum will certainly be easier than following all the issues on GitHub.

This is just about reducing the review request noise. GH doesn’t allow going back to Draft unfortunately but OTOH this can be explained by the fact that once you have requested reviews automatically, the harm is done. Activity on an in-progress PR where reviews were requested too early also generates lots of spurious notifications for reviewers. That’s quite annoying.

Having large and complex PRs containing all the work necessary to go in one direction (including bug fixes) is useful for the developer, and it’s useful to share the branch with the world for demonstration. But it’s unreviewable. The problem we had in the past is that people still expected these kinds of PRs to be reviewed, while splitting was the way to go. But splitting too early and submitting all the spitted PRs at once is also not great because of the stacked PRs noise, and because every time you have to rebase, it is more work. On the other hand, splitting one or a few commits to a ready for review PR to get it merged, while pointing to the large draft PR for context on how this is getting things closer to the end goal would be very useful, and that would be a workflow that doesn’t create these problems. I think it would be in particular very useful for you @ejgallego, because you often mention to us that you have branches where you have made huge progress on such or such front, and you cannot share them with us because the merging rate is too slow. Opening such a large draft PR would provide insights and motivation for reviewers to act quickly on preliminary infrastructure PRs.

My point is that you probably have a main branch that you are actively working on and which contains all this work. Then, having several additional PRs in review open at the same time is counter-productive (more work for you). If there are less PRs to review, it will help accelerate the review process. In particular, you can say: “Look at all the beautiful things that are waiting on this trivial thing to get merged!”

PR with very long discussions are also making the reviewers’ job a nightmare. Overall, it seems to me that you are putting the blame of long PR reviews on reviewers only, and while it has definitely something to do with this, this is also a problem of process. (And while you are the main one complaining from long review processes, you are not exempt from cases where you are the slow reviewer / have been delaying PRs for too long).

Sure, we can add this sentence to the contributing guide. I wouldn’t call it a “policy” though. My point about introducing a policy was to have rules to decide when a PR should be closed (in particular) and to be able to quickly understand the status of a PR.

1 Like

I appreciate clear policies and this is definitely a step in the right direction.

I think one should also take into account that some contributors do this in there spare time which usually varies. One might find an issue in the review of a PR which might take a bit to fix and the contributor simply might not have the time for this right now. Of cause one can then close the PR and later open a new PR, but linking the discussions together likely produces more noise than what is reduced by closing a PR which is not touched at all for a few months. Actually I don’t see how branches which are not touched at all produce noise, but I see that going from “ready to review” back to development produces noise.

Do I understand it right that it is possible to close a PR and reopen the same PR as draft PR? Or does one have to create a new PR if one switches from non draft to draft?

In case it is difficult to switch from non draft to draft, we might want to ask GitHub to change this and wait with using this feature until this has been changed by GitHub.

No, this is not possible unfortunately.

Maybe the time limit should be longer: another option is 3 months, which is the norm of GitHub to decide when a branch is “stale”. But even if this is a PR by a contributor who cannot work actively on it, I am not sure of the point of keeping a PR open for more than 3 months if it has not received a single push (either a new commit or a rebase).

In general I don’t care about “we can get rid of some label”, it is
neither + nor - for me.

Pull requests are a good way to communicate about work in progress:
the use of draft pull requests is encouraged for any actively
developed branch on a developer’s fork (even if it is far from being
ready, and even if it contains lots of commits).

The use of stacked PRs is discouraged. Instead, the developer should
use draft PR pointing to a single branch with possibly many commits,
and only split up into multiple simpler PRs when ready for review (one
PR ready for review at a time, no stacked ready for review PRs). In
particular, we get rid of the needs: merge of dependency label.

Sounds fine.

Pull requests must be opened in draft state until all relevant
checkboxes (of the PR template) are checked. In particular, no feature
should be marked as ready for review without complete, precise and
accurate documentation.

This feels like heavier process and I’m not sure of the gain but OK.

If it turns out that a PR in review state is not ready for review, it
should be closed and reopened as draft. In particular, we get rid of
the needs: review label, and the needs: progress, needs: independent
fix, and needs: feedback labels are reserved to draft PRs.

This close-and-open dance sounds quite painful, let’s not.

Draft pull requests that do not represent actively developed branches
only create noise: PRs corresponding to branches that are not pushed
to for 30 days are closed (we could also say 3 months, which would
correspond to GitHub’s definition of stale branches). The author is
then encouraged to use an alternative form to record the idea: new
issue, documentation, Discourse post or blog post that can be linked
to from a relevant issue or piece of documentation…

OTOH that makes sense, OTOH I’m afraid that we have no great place to
move discussion to (CEPs have not been especially useful AFAICT,
issues are basically PRs but without associated code, maybe discourse
will work but who knows). I guess we don’t lose much by trying.

PRs in review that create too much discussion (more than 50 comments,
maybe an even lower number) are either not ready and should be closed
and reopened as draft, or require fundamental discussion and should be
closed and reopened as CEPs / RFCs, or as Discourse posts if they are
not yet ready to become CEPs. In particular, we get rid of the needs:
discussion label.

Long discussions on github are certainly a pain, but moving them to
CEPs doesn’t change that. I don’t see the point of reopening as draft.
If discussion is needed apart from code issues moving it to
issues/discourse may help, I’m fine trying that.


We have basically 2 issues wrt PRs:

  • lack of manpower, particularly reviewer time and also developer time
    to fixup PRs
  • some noise problem? I see people mentioning noise in this thread but
    I haven’t experienced it as a problem so don’t know what it’s about.
  • github UI problems, particulary with high comment numbers (high
    rebase numbers too now that github shows them in the timeline) and
    stacked PRs

Maybe we should look for something with a better UI than github?

Indeed that could happen and that’s fine; my point is that this bit of policy seems critical and not all devs are here, thus this makes this medium unsuitable for discussion today.

Indeed I welcome draft PRs very much. However, when I talk about splitting is mostly due to risk minimization, it is often that I have two PR that conflict with each other, let’s call them A and B. I could stack A on top of B or viceversa, but giving how unpredictable and non-rational our current review process is, you never know whether A or B will be blocked for months. So from the point of view of risk minimization, it is better for me to submit A and B separate, as this gets a better chance to get one of them merged.

I cannot do that for the reasons pointed above, it is way too risky. It is better to put the eggs in many baskets.

Anyways I fully support Draft PRs and most of my PRs will indeed likely come to life in this form.

I am not placing blame on them or in nobody. I just have plenty of evidence that we are not doing a good job on that. Like a PR that is ready and approved for 10 days, but nobody has 5 minutes to merge, forcing half a dozen of rebases of the PR and the overlays. That’s easy to see, just look at what Gaëtan merged this last days, PRs he’s not in charge and nobody was taking care [and he did while not supposed to]

First, I am not alone on thinking like that; and second, I am not sure what your line of reasoning is here. It seems to me that you have a tendency to personalize [like in the warnings PR] and I am not sure how what I personally do is relevant in any way to the general discussion about policy taking place here. Now that you mention it, what you say actually borders falsehood as I am sure that while not perfect, my performance as a reviewer / assignee is for sure going to be among the top performers in responsiveness, as I take very seriously the cost that neglecting reviews/merging has on others.

I do subscribe Gaëtan comments, and I’d like to add an additional thought about how I perceive the review culture in the project.

Indeed, in my opinion, we not only have a manpower problem in the review process, but also, a cultural one. I’d call it “the curse of the academic review culture”

Most people involved in the project come from an academic background. It is not necessary to state how broken the academic review system is and in particular how frustrating it is for authors of papers. I’ll spare you folks from that as it is easy to find many info with Google, but indeed, a key misfeature of the academic review process is that reviews are many times focused in finding flaws than in enabling the positive to shine. Another misfeature of the academic reviewer is the lack of consideration for tradeoffs.

I feel the current review process still has a flavor of that. Our default PR policy seems many times to be “reject”, and it is easy to see PRs blocked without considering global tradeoffs, etc…

This discussion is not meant to enact anything / take any decision, just to share ideas, discuss them, and try them. For that purpose, I think Discourse is as good as other means, probably better than GitHub given that most developers tend to ignore most issues. Since you reminded me that not all developers were there, I advertised the discussion on Coqdev, so people should at least be aware that it is happening.

Going back to the topic, I feel like what you are proving to me is that this PR policy is critically lacking content on the review process (like what is expected from reviewers). But the main reason why this doesn’t talk about it is because we were already supposed to have a policy for this (the MERGING document). It’s just not working well enough, so indeed we should think about what to do to fix this.

In https://github.com/coq/coq/blob/master/dev/doc/MERGING.md#reviewing, you can read:

When none of the maintainers have commented nor self-assigned a PR in a delay of five working days, any maintainer of another component who feels comfortable reviewing the PR can assign it to themselves. To prevent misunderstandings, maintainers should not hesitate to announce in advance when they shall be unavailable for more than five working days.

Obviously this was not there from the beginning. I did add this to enact something that was already happening and maintainers that are not responsive should expect that kind of action. This is better than nothing but this doesn’t fix the issue of reviewers blocking PRs from getting merged, without being available to help get it into a shape that satisfies them. Here, I’m talking about PRs such as:

(This are the current examples but there have been many more in the past obviously.)

I assumed you would bring that particular PR into the discussion, I am afraid it is a special case and thus not suitable for discussion about policy. Just to get you an idea, I’ve likely spent more time trying to get the diffs PR in shape in the last year than in all other PRs I’ve shepherded combined, including the IW where I spend the majority of my time trying to get the original PR in a mergeable state.

In fact the original PR is an example where precisely we did not adhere to our usual blocking policy and used a more lax one as not to block the things for years; but there is a limit on what we can do.

Note that by the way I am not a maintainer of the printing.

I’d say that the review process is fatally flawed as the way it is it turns out that the maintainers of the subsystems have little control over their own PRs, as they are at the mercy of the non-maintainers, leading a bit to a “design by committee” model.

This seems pretty hard to fix tho.

I’ve not participated in the previous discussion on this topic, such as in the Coq working group. The goal of reducing the noise for reviewers is a good one. My thoughts:

  • I’m uneasy applying quantitative criteria automatically (close a PR after 30 days or more than 50 comments) instead of applying reviewer judgement and perhaps having discussion between the reviewer(s) and the submitter. (Can you reopen a closed PR or do you have to create a new PR?)
  • Sometimes it’s taken more than 30 days to get a review.
    Closing the PR in such cases is not appropriate.
  • Having to close one PR and open a new one just to change it from regular to draft or vice-versa seems very awkward.
  • What is a CEP? How does one submit CEPs and RFCs? I’m not sure how useful such mechanisms are in practice.
  • Perhaps we could get most of the envisioned benefit of the proposal with a new needs: review flag, which triggers sending notifications to reviewers only when it’s set, plus an easy way to filter PRs on that flag.
  • Perhaps we could get most of the envisioned benefit of the proposal
    with a new |needs: review| flag, which triggers sending
    notifications to reviewers only when it’s set, plus an easy way to
    filter PRs on that flag.

That would mean handling review request through the bot, since github
doesn’t have any such feature.

Gaëtan Gilbert

An example is my pr #8512 on the merge-pr.sh script. Basically it works but Maxime found that it does not work if more than one email is attached to the used gpg key. It is not hard to fix this, but a bit hard to test - I thought about adding another email to my github pgp key but I am not sure if I want this - and that is the reason I didn’t finalize it as yet. And then I need a PR to merge to really test it. But since this PR affects a single file which doesn’t change frequently, there is no issue with not rebasing it.

I think there are many other types of PRs which have similar properties, like adding packages to the Windows installer (even if windows build scripts change, the changes are usually very localized and easy to merge) or adding new features to the standard library in a new file.

I really think that we need an easy way to switch back from “non-draft” to draft and we should ask GitHub for this feature.

That’s a good example as well: in this case, the reviewer who found the flaw should provide help in testing fixes IMHO.

Agreed, I should have fixed it and asked Maxime to test it - I will do this asap.

But my main point is that the aging rate of PRs is very different dependent on the nature of the PR. Some will be hard to rebase even after just one week, other can be rebased automatically after 6 months. I agree with Jim, that there should be no automatism, but we should move PRs back to draft as we see fit. And for sure I wouldn’t have a problem to move #8512 to draft state, if this would be possible.

Do you have objections against a feature request to GitHub and waiting a few months for it?

I don’t mind. It doesn’t prevent us from testing draft pull requests in the meantime. I think GitHub are very eager to hear early feedback on this kind of stuff anyway. However, they never provide timelines or guarantees that they will respond to a feature request.

Note that relying on draft pull requests achieve two things:

  • Not triggering review requests from code owners. This is usually too late when you go back to draft state. However, this would still be useful to avoid triggering review requests from more code owners (if the in-progress PR starts touching new components for instance).
  • Helping to see the status of the PR at a glance. A label can also achieve this and this is the point of the “needs: progress” label.

Anyways, it’s clear that everyone is against the heavy burden of closing a PR and reopening as draft. I think that to start with, the terser alternative that @ejgallego proposed is good enough: