Mathlib is open for refactoring!

Stream: mathlib4

[Scott Morrison]

We've just made the port-complete tags on both the old and new repositories!

What does this mean:

• While we hope that it will remain viable to use mathport to port lean 3 projects which depend on mathlib3 to Lean 4, the mathlib4 and mathlib3 repositories will start to diverge faster now.
• Some people porting lean 3 projects may find that it works better to port to the port-complete tag of mathlib4, and then bump up to the latest. Please let us know how this goes, and ask for the help you need!
• PRs marked after-port are now fair game for merging!
• Mathlib is open for refactoring PRs!
• We finished^*!

Caveats:

• there's still quite a few not-too-late PRs on mathlib3, that we would like to get merged and forward ported. But besides that, mathlib3 is done, and closed.
• there is a lot of documentation, and other pages on the community webpage, that still need updating. Contribution to this work is very much appreciated.

[Scott Morrison]

I'm somewhat amazed that we got there!

[Scott Morrison]

I hope we can plan a bit of a PR review sprint sometime soon. It would be great to start off afresh on Mathlib with persistently smaller backlogs of PRs. :-)

[Yury G. Kudryashov]

#queue3 #queue

[Yury G. Kudryashov]

I've recently copied topic labels (t-*) to mathlib4. It would be nice if PR authors will apply them to their PRs.