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

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/353 drops a file that was already upstreamed (+5 −332)

[Alex Kontorovich]

We've so far been running things with "Outstanding Tasks" in Zulip (and manual adjustments based on claims), but other collaborations run using Issues (or whatever it's called) in GitHub. Is that model better/easier to manage? If so, would now be a good time to transition to it? (And if so, can someone help me learn how to set it up?)

[Shreyas Srinivas]

Alex Kontorovich said:

We've so far been running things with "Outstanding Tasks" in Zulip (and manual adjustments based on claims), but other collaborations run using Issues (or whatever it's called) in GitHub. Is that model better/easier to manage? If so, would now be a good time to transition to it? (And if so, can someone help me learn how to set it up?)

In the equational theories project we developed a system using github projects and CI. This setup can be copied almost as it exists from there, ideally by a project maintainer.