stacks of pull requests

Stream: mathlib4

[Antoine Chambert-Loir]

Damiano Testa said:

For instance, this is how the latest batch of Joël's "big PR" looks like.

I have a question to @Joël Riou and git experts:

• what is the procedure to pile up PR like this?
• what happens every time one PR is accepted after modifications?

[Damiano Testa]

I do not know what Joël's approach is, but I would regularly git merge the PRs with modifications and manually take care of breakage.

[Damiano Testa]

(At least this is what I normally do when I have PRs that are blocked by other PR.)

[Damiano Testa]

I know that you get slightly better merge behaviour if you "start right": I normally branch off bigger changes from smaller ones. I think that simply starting merging a small PR into a bigger one probably sets you up correctly anyway.

[Damiano Testa]

I am pretty sure though that, even in the absence of merge conflicts, there is no automation to automatically reduce the diff to master, once the smaller pieces have landed.

[Anatole Dedecker]

I think one of the reasons we don't have more documentation on this is that the precise setup depends on everyone's taste. What is common is the following:

• from GitHub's/bors' point of view, there is no dependence between branch, so if you have multiple PRs depending on one another you have to indicate it in the way suggested when creating a PR
• at any point you can merge the changes from any branch A into your current branch B by doing git merge origin/A (or git merge A if you specifically want to use your local copy of branch A, but I think in most cases that's not what you want). This includes pulling into B some changes that you made in A (e.g during the review) or, keeping B up do date with origin/master (e.g after A has been merged)

[Antoine Chambert-Loir]

So the idea would be:

• PR a little thing
• PR that little thing plus something else as a second PR and tag the first PR in the comment
• etc.
  so that when the PR are accepted in the natural order, each PR is merged in the next one.
  But if some substantial modification is made in the first one, it will have to be echoed many times, that could be a nightmare…

[Damiano Testa]

Antoine, yes, this is how I have been doing it.

[Damiano Testa]

After all, if you change the first PR, then the subsequent ones will likely have to adapt and there is virtually no support for automating that, right now.

[Damiano Testa]

(Not saying that this is ideal, simply that I do not have a better alternative.)

[Joël Riou]

@Antoine Chambert-Loir: I have a working draft branch where all the material is, and then I copied chunks of code into new PRs as you suggested.

In this particular case, the dependence tree is not completely trivial: I have a paper where I have written the numbers of the PRs and the names of the branches, so that if one PR is changed, I know which other PRs I need to update.

[Antoine Chambert-Loir]

Thanks!

[Kevin Buzzard]

@Siddhartha Gadgil this discussion might be relevant to you.

[Jireh Loreaux]

Note that if B depends on A, and then A gets merged with lots of changes, and B has not changed, then an easy way to incorporate all the new changes is: merge -X theirs master.

However, take care: If there are merge conflicts other than the ones created by the changes from A, this may not do what you want. Nevertheless, I find it useful.

[Jireh Loreaux]

There is an alternate strategy: keep one big PR, make all changes there, and then cherry pick them into the dependencies. I find this harder to do, but sometimes it's better.

[Yaël Dillies]

Personally I replace "one big PR" with "a separate repo with instructions for future me"

[llllvvuu]

--update-refs option helps with updating the stack: https://andrewlock.net/working-with-stacked-branches-in-git-is-easier-with-update-refs/

also note: don't make the mistake I did of basing each PR off of the previous PR. While that makes the diff cleaner, mathlib or bors seems to automatically delete branches upon merging, which will close any PRs based upon it, with no way to re-open.

[Yaël Dillies]

llllvvuu said:

... with no way to re-open.

That's wrong, you can reopen them, but you first need to undo bors' closing of the base branch in the previous PR

[llllvvuu]

TIL, thanks!

[Joachim Breitner]

Jireh Loreaux said:

Note that if B depends on A, and then A gets merged with lots of changes, and B has not changed, then an easy way to incorporate all the new changes is: merge -X theirs master.

However, take care: If there are merge conflicts other than the ones created by the changes from A, this may not do what you want. Nevertheless, I find it useful.

The safer way is to go back to A's branch, run git merge origin/master (should go through without conflict), then go to B's branch and run git merge -. This two step process helps git to understand the “conflicts” between A's changes on A's branch and A's squashed commit. I've been using this regularly on lean repository.

[Joachim Breitner]

At a previous project which only allowed strict squash merges, I automated the process (https://github.com/nomeata/git-post-squash). This won't work on mathlib or lean4, but the above manual two-merge should work reasonably well.

[Eric Rodriguez]

I wonder if the Facebook people really are onto something with their stacked diffs or whatever it is

[Joachim Breitner]

Is that phabricator? GHC used it for a while, supposedly really much better UI for that use case.

[Eric Rodriguez]

Yeah it appears so! Just heard anecdotally of it not sure of the precise differences

[Jireh Loreaux]

Joachim Breitner said:

The safer way is to go back to A's branch, run git merge origin/master (should go through without conflict), then go to B's branch and run git merge -. This two step process helps git to understand the “conflicts” between A's changes on A's branch and A's squashed commit. I've been using this regularly on lean repository.

That's nice indeed, but it also comes with a small hiccup. There could be issues with git merge origin/master into A's branch if there were edits made in the GitHub UI before merging, and you don't have the latest version locally (and the branch on GitHub was deleted by bors); this can happen especially with delegated PRs. Nevertheless, this is a minor inconvenience and I think your approach is better.