Zulip Chat Archive

Stream: general

Topic: Dependent PRs

Wrenna Robson (Sep 01 2022 at 09:54):

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 (Sep 01 2022 at 10:53):

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

Johan Commelin (Sep 01 2022 at 10:54):

<!-- 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 (Sep 01 2022 at 11:18):

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 (Sep 01 2022 at 11:44):

It would be great if the merge step was automated somehow

Wrenna Robson (Sep 01 2022 at 12:33):

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 (Sep 22 2022 at 21:25):

Yes, you merge the master branch

Yury G. Kudryashov (Sep 22 2022 at 21:26):

But you need to update it first (git pull)

Last updated: Aug 03 2023 at 10:10 UTC