Dependent PR

Stream: new members

[Anatole Dedecker]

How do you make a PR that depends on things defined in another waiting PR ?

[Yury G. Kudryashov]

You can start a git branch from another branch.

[Kevin Buzzard]

And then in the PR comments say it's blocked by the other PR

[Yury G. Kudryashov]

git checkout -b new_name old_branch

[Anatole Dedecker]

I don't know why I was thinking it would cause problems, I had forgotten how git works :sweat_smile:

[Patrick Massot]

The system is far from perfect because GitHub doesn't have this concept, so it will show the full diff in the second PR by default. You need to explicitly filter out commits if you want to see what's new.

[Patrick Massot]

Usually stacked PRs like this are only a way to put pressure on reviewers.

[Anatole Dedecker]

Huh, I'll wait then

[Yury G. Kudryashov]

It's OK to open a PR now. This way people see why do you need the first PR.

[Johan Commelin]

Patrick Massot said:

Usually stacked PRs like this are only a way to put pressure on reviewers.

I think 1 layer of stacking can be useful. Like Yury said. But stacking more on top of that is typically not helpful.

[Nicolò Cavalleri]

Moreover, to see the differences with respect to the other PR and not the master branch (I guess to highlight the real new features), you can change the base branch on GitHub. If you do so, you should write it clearly in the description so that whoever merges it changes the base branch back to the master branch before the merge, otherwise the branch gets merged into an already approved PR but does not make it into mathlib