Hint about merging

Stream: general

[Yury G. Kudryashov]

I often find myself in the following situation:

• I start branch A.
• I decide that A is too large for 1 PR, so I cherry-pick some changes to another branch B, and start a separate PR.
• Then I make changes to branch B (e.g., because of reviewers' comments).
• Then branch B is merged into master, and I have conflicts in branch A.

I guess other people may have the same problem, so let me share my way of dealing with it without need to manually resolve conflicts.

• Once I cherry-pick changes from A to B, I merge the new branch B to A (you can do it later with git merge sha1hash).
• When B is merged to master, I do git checkout master && git pull && git checkout B && git merge master && git checkout A && git merge B. Often all merges happen without conflicts.

[Eric Wieser]

You can abbreviate that last command to

git fetch origin && git checkout B && git merge origin/master && git checkout A && git merge B

Which saves moving your working tree to master and back

[Eric Wieser]

But yes, the key trick is to merge bors' copy of your PR back into the branch it came from before merging that branch into follow-up PRs. The other trick is to run leanproject get-cache --rev origin/master immediately after that process, to start your cache rebuild somewhere reasonable.

[Alex J. Best]

Can we put these tips in the docs or somewhere less transient/easier to find than zulip?

[Yury G. Kudryashov]

Feel free to pr!

[Floris van Doorn]

An addition to this trick: I'm sometimes faced by the fact that I worked on branch B on a different machine, and so my current machine doesn't have the latest commit on branch B. This is annoying, since bors has deleted branch B in the meantime, so git fetch --all won't even fetch the commit you need to do this merge trick.
In this case, what you can do is first find the full commit hash of the last (non-bors) commit of PR B and then run
git fetch origin <full-commit-hash> && git checkout <full-commit-hash> && git checkout -b temp && git merge origin/master && git checkout A && git merge temp && git branch -D temp

[Floris van Doorn]

(btw: if someone wants to add this to https://leanprover-community.github.io/tips_and_tricks.html, that would be great!)