Upstreaming to Mathlib

Stream: PrimeNumberTheorem+

[Oliver Nash]

I'd like to suggest contributors consider PRing to Mathlib as much as possible. It's a lot more work but work that lands in Mathlib is a huge benefit to everyone.

[Riccardo Brasca]

I cannot agree more. We did this for flt-regular (at least until it was reasonable), and the benefits are much bigger than the drawbacks.

[Ian Jauslin]

That's the plan! We are working on a separate repo to host the blueprint, but everything will be PR'd to mathlib as it becomes ready

[Oliver Nash]

I haven't paid proper attention to what has been upstreamed and what has not. Is there a rough estimate for the size of the upstreaming effort at the moment?

[Vincent Beffara]

I didn't really look at that - is the folder Mathlib in PNT+ intended as a staging area for PRs? (I used it to import contents from PRs to Mathlib that were not yet in because it felt most convenient, sorry if that was not the point.) If indeed it is a staging area then it is at least 3k lines of code ready for PR.

[Ruben Van de Velde]

It seems like the repo is nearly up to date with mathlib, so everything should be upstreamable

[Vincent Beffara]

Yes I last bumped Mathlib version on Sunday