Merging github repos and history

Merging the git history

Reasons to do this:

• It makes git blame trace back to mathlib3
• It make the github contributor stats reflect not just the porting effort, but also the mathlib3 effort
• It gives us the option of merging the repos without breaking links to commits.

The approach I suggested is to avoid rewriting any history, and instead carefully structure merge commits to produce

gitGraph
   branch mathlib3
   commit
   checkout main
   commit
   checkout mathlib3
   commit
   checkout main
   commit id: "last porting commit in mathlib4"
   commit
   checkout mathlib3
   commit id: "last commit in mathlib3" tag: "port-complete"
   checkout main
   commit id: "last forward-porting commit in mathlib4" tag: "port-complete"
   checkout mathlib3
   branch fix-hist
   checkout main
   branch _
   checkout main
   commit
   checkout fix-hist
   commit id: "mathport output"
   checkout main
   commit
   checkout fix-hist
   merge _ id: "Merge of last mathport output into master, discarding all changes from mathport"
   checkout main
   commit
   checkout fix-hist
   merge main id: "Combine the mathlib3 and mathlib4 repos"

Loading

Zulip message:

* "Combine the mathlib3 and mathlib4 repos"
|\
| * Merge of last mathport output into master, discarding all changes from mathport
| |\
| | * automated fixed (Mathbin -> Mathlib)
| | * mathport output for last commit in mathlib3, with lean3 versions deleted
| | * last commit in mathlib3
| | |
| |
* | misc mathlib4 features that happen
* | misc mathlib4 features that happen
|/
/
|
* last forward-porting commit in mathlib4
* last porting commit in mathlib4
* misc mathlib4 commits
|

Merging the repos

Option 1: do all future work in leanprover-community/mathlib4

This is the "do nothing" option, where the merged history is pushed to mathlib4, and mathlib3 is left alone.

Advantages:

• Mathlib4 commit messages of the form feat: some feature (#XXXX) still auto-link to the right PR
• We continue with a "clean" issue tracker that doesn't have ancient lean3 issues in it

Disadvantages:

• Mathlib3 commit messages of the form feat: some feature (#XXXX) do not link correctly

Option 2: do all future work in leanprover-community/mathlib

In this option we push the merged history to mathlib3, and rename the current mathlib3 master branch to lean3-master. We then transfer all the open issues, copy across all the branches, and then ask contributors to re-open their PRs (we can write a bot that gives them a link to do this)

Advantages:

• Mathlib3 commit messages of the form feat: some feature (#XXXX) still auto-link to the right PR
• We don't have to type a 4
• Existing mathlib3 PRs can be revived by merging master!

Disadvantages:

• Mathlib4 commit messages of the form feat: some feature (#XXXX) do not link correctly
• Open PRs have to be re-opened, and discussion is discontinuous as a result.
• We inherit all the old lean3 issues and PRs

Option 3: rename leanprover-community/mathlib to leanprover-community/mathlib3, leanprover-community/mathlib4 to leanprover-community/mathlib

Advantages:

• Mathlib4 commit messages of the form feat: some feature (#XXXX) still auto-link to the right PR
• We don't have to type a 4
• Full URLs to mathlib4 issues and PRs automatically redirect to urls without the 4

Disadvantages:

• Mathlib3 commit messages of the form feat: some feature (#XXXX) do not link correctly
• Any full URLs to mathlib3 issues and PRs now break