Pull request policy

Another example of a blocked PR is https://github.com/coq/coq/pull/8228. In this case, it is blocked because a middle ground cannot be found between the submitter and a single reviewer, leading to a not-merging-nor-closing situation. It’s a pretty good case (even if the proposed change is simple) where online asynchronous discussion is just not the right tool, and face to face (or visio) discussion should happen to unblock things. We clearly don’t spend as much time doing this as we should. On the one hand, there are trivial PRs that nobody is blocking that we should become more efficient at merging, on the other hand, there are either simple or complex PRs that raise debate, that we should become more efficient at managing in another way to eventually take a decision which is not just “the submitter abandons”.

I would say we should more have a “water flowing around rocks” type of policy than a “honed steel cog-wheel” type of policy. Of course this still means we should have a policy. And this policy should include that draft PRs should be used in the cases were it obviously makes sense.

Regarding GitHub: so let’s write some feedback to GitHub (you or me?) and use draft PRs following a “soft” policy and tighten the rules a but when GitHub enhances the feature.

I can do it if you want.

I would prefer if you do it - you have a better overview.

For the record we have discussed about this in person for many hours :smiley:

This is more of a case of the reviewer being too strict, rationally, the PR just goes back to what the 8.8 situation was, and no harm can happen [and indeed the reviewer failed to produce a single bad behavior that the abstraction prevents as there is none].

On my side, I cannot close the PR as indeed quite a few works depend on that core part of the API, including for example the latest efforts you can see Kaiyu form Princeton doing [in the SerAPI channel].

OK but then this is a case where it should be brought in front of the WG and a vote should happen. What I meant was really we need to have a process for unblocking things even if the reviewer and the submitter can’t find a common ground (including after talking face to face).

[Note however, that while I hadn’t really paid attention to this PR until now, I read it entirely today, and I find that, while Pierre-Marie’s blocking wasn’t very clearly justified, you didn’t detail the use cases very much either (back in September).] But this is not the topic here anyways.

I am not sure technical issues should be resolved with a vote. The infamous Debian TC is known to have taken some weird decisions.

The use cases are obvious by the way, that’s the only way to query what’s seen by the kernel! In the same way you absolutely need access to the local environment, you of course may want to query the global one. I did justify many cases.

I didn’t justify that back so much in the day as it was a critical API regression from 8.8 and the author of the commit making the thing opaque (Gaëtan) agreed to revert and said the change was not intended. So this is a case of reviews causing trouble.

Anyways, I feel like we are having a discussion that doesn’t belong here but to a GH issue; IMHO I do think that for this kind of discussions we shouldn’t duplicate venues and stay on GH.