Dependent PRs

Stream: general

[Wrenna Robson]

Is there written down somewhere the procedure for properly making a PR dependent on another in a way that will make Bors happy on merge? I want to build off one of mine.

Also, can a PR be dependent on multiple PRs?

[Johan Commelin]

Yes and yes. See the default commit message when you open a PR on github.

[Johan Commelin]

<!-- The text above the `---` will become the commit message when your
PR is merged. Please leave a blank newline before the `---`, otherwise
GitHub will format the text above it as a title.

To indicate co-authors, include lines at the bottom of the commit message
(that is, before the `---`) using the following format:

Co-authored-by: Author Name <author@email.com>

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->

[Damiano Testa]

I use this all the time and I am quite happy with the setup. What I also find, though, is that once a dependent PR gets merged, there is no escaping having to merge master into the now-less-dependent PR to get the diff to change. This applies regardless of whether there actually are further changes or not.

This is a relatively painless step, but if you touch one file with one PR and a different one with the second one, once the first file is in, you will need to merge the updated master on the branch with the second file to get the diff to shrink.

Writing it, it now sounds obvious, but it took me some time to realize what was going on! And maybe someone will now tell me that there is a way to avoid the "merge to shrink the diff" step!

[Alex J. Best]

It would be great if the merge step was automated somehow

[Wrenna Robson]

When I make the PR, should I used:
leanproject pr foo
and then git merge bar, where foo depends on bar? Then, after bar has merged, use git merge master?

[Yury G. Kudryashov]

Yes, you merge the master branch

[Yury G. Kudryashov]

But you need to update it first (git pull)