coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.83k stars 646 forks source link

PR depending on PR just don't work #7167

Closed gares closed 6 years ago

gares commented 6 years ago

They were never easy to deal with, but with the new merging process it is just unbearable.

In particular the code-owners business applies to all commits in the PR. Hence a PR 2 touching (only) file A but depending on PR 2 touching file B gets the code owners of file B in the loop. The shepherd has then to take pen and paper to check what was reviewed and what not.

I open this issue to have a discussion. IMO @ejgallego is the most proficient user or such kind of PRs and @Zimmi48 was recommending this, so I put them in the loop. My objective it to ease the job of the shepherd.

gares commented 6 years ago

Question 1: why does one need to open PR 2 in the first place?

One can keep branches in his private repo and use projects to organize his submission of PRs.

ppedrot commented 6 years ago

I can only support this. PRs depending on other PRs are a real mess, including for the PR writer... I'd also advocate for only pushing PRs one-by-one.

ejgallego commented 6 years ago

Well, considering merge time and other factors, if I have to push PRs one by one I won't be able to get any work done at all, I'm afraid.

The only other alternative is is have proper branches, but then you'll have many potential changes grouped together, and a big merge.

Zimmi48 commented 6 years ago

I prefer pushing PRs one by one and this is what I've been advocating as a first solution but I understand that sometimes people want to show what they have in store.

Well, considering merge time and other factors, if I have to push PRs one by one I won't be able to get any work done at all, I'm afraid.

Indeed, I can understand this.

Note that not all PR dependencies have the same problem:

The main mess arrives when people open a large refactoring PR and another one depending on it (like e.g. the Dune PR). Maybe the important thing to consider is that actively searching for code owner approval should only be done once the "needs: merge of dependency" label has been removed, and the PR rebased...

Zimmi48 commented 6 years ago

Maybe the important thing to consider is that actively searching for code owner approval should only be done once the "needs: merge of dependency" label has been removed, and the PR rebased...

Although in this case, there is still the problem that code owners for the PR dependency have had a review requested for no good reason and they can't even remove the request for review even when they are not shown as code owners anymore (the second part is IMO a bug in GitHub).

I think that GitHub staff might be interested in this discussion BTW. Can someone send them the link?

ejgallego commented 6 years ago

I think that we have also seen this pattern of "nested" PRs so often because since the API movement started, we have done a lot of structural work. But I think we are very close to converge in that front, so maybe in the future we will see way less PRs of this nature.

gares commented 6 years ago

Well, considering merge time and other factors, if I have to push PRs one by one I won't be able to get any work done at all, I'm afraid.

This is a sensible issue but I don't understand what advantage opening all the PRs gives you (over opening them one by one).

Where do you gain time?

Stacks of PR are harder to deal with, why should they be processed faster?

gares commented 6 years ago

I think that GitHub staff might be interested in this discussion BTW. Can someone send them the link?

I think we need to converge first. For example I don't feel confident asking for "more support for stacks of PRs" since I don't yet understand why we do it (to my eyes we are just looking for troubles).

maximedenes commented 6 years ago

My experience is that stacked PRs basically shifts the burden from the author of the PR to the merger and reviewers. So it's a tradeoff.

@ejgallego often uses stacked PRs as an optimistic pipeline: if PR B depends on A (and the two conflicts), and A is merged unchanged, the author doesn't need to rebase B after A is merged.

Opening B only when A is merged is also sensible, but then you can't get reviews for B until A is merged, which is also a source of delay.

I'm afraid I have no good solution to suggest.

ejgallego commented 6 years ago

This is a sensible issue but I don't understand what advantage opening all the PRs gives you (over opening them one by one).

Where do you gain time?

It allows for much more time for review, also early feedback improves dev turnaround. It is often that I implement significant changes. A canonical example is the Dune PR, see the queue, and tell me not to submit things one by one.

Also, submitting PR 1 that depends on PR 2 helps reviewers of PR 2 to understand motivations for it.

My experience is that stacked PRs basically shifts the burden from the author of the PR to the merger and reviewers.

I disagree, having to do a stacked PR is way more of a burden for the author, and it actually lessens the burden on the reviewer / merger. Think that the alternative would be to submit a big, merge branch. Not so long ago we were discussing about the large PRs Hugo does and how they should be split because they were harder to review. So indeed, there is a contradiction somewhere in your statement.

maximedenes commented 6 years ago

I disagree, having to do a stacked PR is way more of a burden for the author, and it actually lessens the burden on the reviewer / merger. Think that the alternative would be to submit a big, merge branch. No t so long ago we were discussing about the large PRs Hugo does and how they should be split because they were harder to review. So indeed, there is a contradiction somewhere in your statement.

I was comparing to the solution suggested above, not to large PRs containing unrelated changes, of course.

ejgallego commented 6 years ago

I was comparing to the solution suggested above, not to large PRs containing unrelated changes, of course.

Yeah, but note that if you split this kind of PRs you indeed do get dependency issues. The reality is that any non-trivial change to the codebase is going to result in a few reviewable logical changes that depend on each other.

ejgallego commented 6 years ago

In fact, I've just becomed very convinced that indeed splitting and making dependent PR makes the codeowners system work better, even with the current setup. Example, #7135, this PR could be split in 2 PRs. If we would do so, the first PR would get a smaller codeowner, more focused codeowner set and i'd bet the change would have already be in Coq. The depending PR would get at first the same codeowners, so we are not worst than in the split case. However, in the split case, after 3 days the first PR is merged and the set of codeowners for the depending one is already better. So in all cases it looks to me like a net gain.

But yeah, we could standardize the Depends: field and have the code review tool understand it.

ejgallego commented 6 years ago

For instance, once a PR with Depends is submitted the bot could adjust the reviews, or maybe post some meta information. I'd be cool if after submitting a PR the bot would say "The most likely candidate to assign this PR to is foo, reviewers blah and shit are only here because of deps".

gares commented 6 years ago

Example, #7135, this PR could be split in 2

I Think you are missing an important point: splitting changes in multiple dependent PRs is perfectly fine. The topic here is: opening them (and expecting actions on the ones with dependencies) is a pain.

But for mistakes on my side (sometimes I miss the Depends: metadata) I stopped doing any action on PRs with dependencies. Indeed if B depends on A and I do some work on B:

The depending PR would get at first the same codeowners, so we are not worst than in the split case. However, in the split case, after 3 days the first PR is merged and the set of codeowners for the depending one is already better.

I think code owners are attached to a PR once and forall when it is opened, so you always get the union of all code owners. Even if you rebase after A is merged, the set of code owners stays the same!

gares commented 6 years ago

JFTR, I'm fine with my way of doing (ignoring PR with dependencies). So you guys can still open them, but I find my "solution" very extreme and defeating any point in making PRs with dependencies.

So maybe we can find a better solution (for both authors and shepherd).

ejgallego commented 6 years ago

But for mistakes on my side (sometimes I miss the Depends: metadata) I stopped doing any action on PRs with dependencies. Indeed if B depends on A and I do some work on B:

I think you are only focusing on B, and indeed it makes the life of those involved in B slightly more complicated as B now depends on A and you have to be aware of that fact.

However, you should also see the other point of view, those that care about A. The people who care about A, now has a much better time reviewing and dealing with the PR than if A+B would have been submitted. And as you mention, the problem for B-people is only temporary as it will correct itself when A is merged.

So yeah, not sure any other alternative is gonna be better. Of course, the best is to submit independent PRs, but many times it is not possible.

gares commented 6 years ago

he people who care about A, now has a much better time reviewing and dealing with the PR than if A+B would have been submitted.

You insist in reading my issue as "don't submit A and B, submit A+B" while my issue is "please only submit A to not pollute the set of open PRs (unless B is crucial to understand what A is for)".

Anyway, I've the needs: merge of dependency label and it seems it can be used to completely ignore PRs that depend on PRs, so I'll just close the issue.

ejgallego commented 6 years ago

You insist in reading my issue as "don't submit A and B, submit A+B" while my issue is "please only submit A to not pollute the set of open PRs (unless B is crucial to understand what A is for)".

I think I've read your issue correctly, see my remarks above on why holding on B would delay review and testing by an amount I consider hard to deal with.

Zimmi48 commented 6 years ago

GitHub now allows removing requests for review from code owners. Consequently, when a PR depends on another PR, we can manually adapt the list of reviewers. Similarly, when a secondary maintainer takes over or when we choose to not wait for reviews of trivial changes. We could even consider adding a new check in the merge script that there are no requests for change and no pending requested reviews.