Document and improve PR merge policy

[MartinSpiessl]

I would really welcome if this procedure were documented somewhere.

I know that we say that a PR can be merge if it has at least one approving review.
I think that is is actually underspecified and leads to problems. If more than one review was requested, shouldn't we wait for the other reviewer to finish his review? Currently we do not seem to do this. We could combine this with a grace period (e.g. if review or at least comment by reviewer with ETA doesn't happen after 48 hours it is OK to merge). It happened to me that someone else approved a PR where I already made a review and demanded changes. It was decided within hours that the changes made addressed my concerns and the PR was merged. Later I looked at it and it turned out that the problems were not addressed. If I knew I had 12 or 24 hours to respond I could manage, but since there is no such policy I would have to check the repo every hour currently (even that would probably not be enough).

We could also add a policy on how to give reviews, e.g. using the comment format described at https://conventionalcomments.org/. This would make it clearer if a comment in a review is actually blocking or not.

For example @dbeyer just approved PR #1141, but also requested changes from the author immediately before approving. This sends mixed signals. As by our current policy he could already have merged it. So was this request for changes a non-blocking suggestion?

[dbeyer]

Thank you for your thoughts on this!

after 48 hours it is OK to merge

Often it happens that developers wait for a PR to be merged before they can progress. I saw this often in the PR descriptions. 48 hours waiting time would be way too much in such situations.

This would make it clearer if a comment in a review is actually blocking or not.

The review in GitHub provides you with three options: blocking, just comment, approve.
If I see a blocking review from somebody, then I will not merge it until that person has approved.

You have sometimes used "comment" instead of "request changes" and I remember that I once approved a change
for which I verified that it addressed your request. Since you did not block it, it was OK for me to go ahead.

Re #1141: I will merge that soon. My change request was not blocking. I wrote it because I think it would be great to have that, but getting the PR into the master is a higher priority than waiting for the name added.

[MartinSpiessl]

Please quote in full, the sentence hat an "e.g." inside, so I never set the 48 hours in stone. If you want this to be 24 or even 12 hours, fine.

The review in GitHub provides you with three options: blocking, just comment, approve.

Yes, but it doesn't allow you to leave multiple reviews or even update an existing one (maybe it exists but I never saw this option). This review-feature is a bit inflexible e.g. if I discover a blocking, easy to fix thing after I approved. I am not sure whether I can change the status of the existing review then.

If I see a blocking review from somebody, then I will not merge it until that person has approved.

Then maybe we should put blocking reviews less reluctantly 👍. But still I do not see why we cannot wait an acceptable time for explicitly requested review, and why writing down a simple policy would be such a big problem.

[PhilippWendler]

Yes, but it doesn't allow you to leave multiple reviews or even update an existing one (maybe it exists but I never saw this option). This review-feature is a bit inflexible e.g. if I discover a blocking, easy to fix thing after I approved. I am not sure whether I can change the status of the existing review then.

Just add a review. You can do so at every time, no matter how many reviews there are and by whom.