Merging github repos and history

Merging the git history

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
|

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

Loading

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

Advantages:

• Mathlib4 commit messages of the form feat: some feature (#XXXX) still auto-link to the right PR

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

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.

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

Advantages:

• 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