dependent PRs

Stream: mathlib4

[Reid Barton]

I don't understand our workflow of, on the one hand, merging master into older PRs (versus rebasing) but, on the other hand, rebasing (and squashing) PRs onto master when they are merged. Once a PR has had master merged in, it seems to become impossible to tell what changes were intended to be part of the PR. How do people deal with this?

[Reid Barton]

For example, in mathlib4#1256, the PR adds some files which were part of other PRs, and master has also added those files (by those PRs getting merged), but with different contents.

[Reid Barton]

I guess I'll just assume the PR in question did not try to change those files, but this seems awkward in general

[Chris Hughes]

You can see from the diff with master that only two files were changed. Probably rebasing is better I guess, but I just use the mathlib3 workflow because it's all I know.

[Ruben Van de Velde]

I merged master into the open PRs

[Kevin Buzzard]

I changed some global config on my git which...might be relevant here?

[Ruben Van de Velde]

There's not really a great way to do dependent PRs in github

[Eric Wieser]

The right thing to do here is to merge master into any dependent PRs so that the diff view shows the right thing, before setting bors on the PR

[Eric Wieser]

Rebasing is possible too but usually requires a lot more work and for no payoff given that bors squashes everything

[Reid Barton]

The problem is that merging master into PRs is likely to result in big merge conflicts, because of the rest of the workflow

[Eric Wieser]

It shouldn't do

[Eric Wieser]

In the cases where it does, there is a standard solution that always works

[Eric Wieser]

But also, I don't think github will even let you merge a PR if you don't solve those conflicts anyway?

[Reid Barton]

I don't understand what you mean

[Reid Barton]

Of course, there may be conflicts

[Reid Barton]

It's quite likely if one PR is branched off another, and then the other PR has been merged after further changes

[Eric Wieser]

See my instructions here

[Patrick Stevens]

It's a massive pain, but you could recreate the merge commit for the closed PR locally, and then merge it into the WIP branch… (cries in Pijul)

[Eric Wieser]

That's exactly what I describe in the link above, isn't it?

[Patrick Stevens]

It is, sorry

[Scott Morrison]

If I want to see changes relative to master, I either look at the diffs on github (which seems to pretty reliably get it right, unless an earlier dependent PR has been merged into master, but master hasn't been merged back to the PR branch), or merge master into my local copy of the PR branch and then git diff.