GitHub/leanprover-community.mathlib4
1
0
Fork 0
mirror of https://github.com/leanprover-community/mathlib4.git synced 2026-03-07 02:46:33 +00:00
Code Issues Projects Releases Packages Wiki Activity
Page: Working with dependent PRs
Pages
Alternate names for `List.concat` and `List.append` Computation models for polynomials and finitely supported functions Home Lean 4 survival guide for Lean 3 users Mathlib3 Synchronisation Metaprogramming for dummies Metaprogramming gotchas Migration to PRs from forks Monad map Porting wiki Project setup: following stable releases Project setup: globally shared mathlib installation Project setup: using local development version of a dependency RFC Exp function RFC: drop `Nat.AtLeastTwo` Setting up linting and testing for your Lean project Tradeoffs of concrete types defined as subobjects Using mathlib4 as a dependency Working with dependent PRs
7 Working with dependent PRs
Eric Wieser edited this page 2024-07-02 22:02:08 +01:00
Table of Contents

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

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

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

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"

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"

Approach 1: merge2

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"

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

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