Working with dependent PRs

You make a branch with some cool feature:

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit
   checkout master

Loading

Then you build another PR on top of that

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit
   branch feature-2
   commit
   commit

Loading

Then your first PR gets some changes in review

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit
   branch feature-2
   commit
   commit
   checkout feature-1
   commit
   commit

Loading

Then your first PR gets bors merged and squashed into a commit on staging

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit
   branch feature-2
   commit
   commit
   checkout feature-1
   commit
   commit type: HIGHLIGHT
   checkout master
   commit
   branch staging
   commit id: "someone-elses-feature1"
   commit id: "feature-1" type: HIGHLIGHT
   commit id: "someone-elses-feature2"

Loading

And then bors finishes, deleting your branch

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch "feature-1 (deleted)"
   commit
   commit
   commit
   branch feature-2
   commit
   commit
   checkout "feature-1 (deleted)"
   commit
   commit type: HIGHLIGHT
   checkout master
   commit
   commit id: "someone-elses-feature1"
   commit id: "feature-1" type: HIGHLIGHT
   commit id: "someone-elses-feature2"

Loading

Approach 1: merge²

TODO: recover from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Dependent.20PR.20-.20merge.20conflict/near/277015458

Recreate the deleted branch, and git merge the-copy-of-feature1. This merge should go through cleanly, but if it doesn't you should choose all the changes from master (TODO: what's the command for this?).

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit type: HIGHLIGHT
   branch feature-2
   commit
   commit
   checkout feature-1
   commit
   commit type: HIGHLIGHT
   checkout master
   commit
   commit id: "someone-elses-feature1"
   commit id: "feature-1" type: HIGHLIGHT
   checkout feature-1
   merge master
   checkout master
   commit id: "someone-elses-feature2"

Loading

Checkout your feature-2 branch, and git merge feature-1. This merge will contain only the actual conflicts

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch feature-1
   commit
   commit
   commit type: HIGHLIGHT
   branch feature-2
   commit
   commit
   checkout feature-1
   commit
   commit type: HIGHLIGHT
   checkout master
   commit
   commit id: "someone-elses-feature1"
   commit id: "feature-1" type: HIGHLIGHT
   checkout feature-1
   merge master
   checkout master
   commit id: "someone-elses-feature2"
   checkout feature-2
   merge feature-1

Loading

Approach 2: rebase

TODO: add exact command. You need to specify where to rebase from!

%%{init: { 'logLevel': 'debug', 'theme': 'base', 'gitGraph': {'showBranches': true, 'showCommitLabel':true,'mainBranchName': 'master'}} }%%
gitGraph
   commit
   branch "feature-1 (deleted)"
   commit
   commit
   commit type: HIGHLIGHT
   commit
   commit
   checkout master
   commit
   commit id: "someone-elses-feature1"
   commit id: "feature-1" type: HIGHLIGHT
   commit id: "someone-elses-feature2"
   branch feature-2
   commit
   commit

Loading