No more PRs?

Stream: maths

[Rémi Bottinelli]

Hi,

Assuming the message below states a consensual opinion, should people ideally stop submitting PRs to mathlib3 and help with the port effort?
I've got quite a few PRs waiting and a few in the pipeline too, but if it's going to get increasingly harder to get them approved, and in some sense unwelcome, then I'd rather know and help with the effort.
At what point could one start making PRs to mathlib4 only?

Thanks!

Kevin Buzzard said:

I'm sorry for the delay Michael Stoll . More and more people coming to the opinion that mathlib3 PRs (other than those which actively help with the port to mathlib4) are in some sense now a step in the wrong direction; maintainers are spending less time reviewing mathlib3 PRs and more time porting files to mathlib4. Any new PR to mathlib3 is just making the port harder. In a parallel universe mathlib3 got frozen and no more PRs are now allowed; right now we're trying not to freeze it and port it simultaneously, and we're still just about managing to do this, but already some PRs were drowned by the rising tide, and the situation will only get worse as the tide rises further. The problem is that mathlib3 is kind of a cool hobby for lots of people, but a bunch of people are planning on teaching using mathlib4 in January, so there are some very concrete porting goals which need to be focussed on by the community which is driving resources away from mathlib3.

[Moritz Doll]

If you want to help with the port, then you are very welcome to do so, the wiki page https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki provides good information on how to do the porting and there is a (slightly out of date) video by Scott.

[Ruben Van de Velde]

I'd have to check now that data.set.basic is merged, but I'm not sure there are enough files available for porting right now to have everyone work on that yet. Still, we might get to that point sooner than later

[Kevin Buzzard]

I should say that I am not a maintainer and my "every PR to mathlib3 unrelated to the port is a step in the wrong direction" claim is just my personal opinion

[Oliver Nash]

We haven't made a decision that we want no more Mathlib3 PRs (yet, anyway) but help with the port is definitely preferable to PRs to Mathlib3.

[Rémi Bottinelli]

Besides the docs on how to port, is there any resource on what to work on? I'm aware of the dependency graph, but is there some kind of "first-issue" kind of things to take a stab at?

[Johan Commelin]

See #port-status

[Kevin Buzzard]

In my experience, a good "first issue" is to port a file which you understand the contents of!

[Rémi Bottinelli]

something nice would be to have a way to filter for files which are not modified by a current PR of mathlib 3. I've had an few instances of a PR getting bors' greenlight only to get "merge conflict" later on because someone ported the file in the meantime.

[Eric Wieser]

Yes, having a list of "active mathlib3 PRs touching this file" visible on #port-status would help a lot here

[Scott Morrison]

I'm pretty confident that we now have more parallel tasks available than people actively working on the port, and I expect this to stay true.

[Scott Morrison]

I posted some advice on identifying the most important tasks here.

[Scott Morrison]

And yes, from a long-term point of view, I think that anyone who is interested/willing to work on either mathlib3 or mathlib4, should choose to work on mathlib4.

[Scott Morrison]

If you are a mathlib maintainer and haven't yet merged any mathlib4 PRs, it's time to get up to speed on that. :-)

[Niels Voss]

I have an open PR for mathlib3, adding new content. Would it be helpful to port it to mathlib4 and PR it there instead? I don't think it relies on anything major except for the definition of primes and Fermat's Little Theorem. In other words, does mathlib4 accept new theories and things that aren't ported?

[Yaël Dillies]

Neither of those things is ported yet, so probably PR it to mathlib.

[David Loeffler]

Can I ask for an update on the same question that @Rémi Bottinelli asked a month ago? Are new mathlib PR's still welcome, or should those of us who aren't able to contribute to the porting effort put our contributions on hold until the port is complete?

I'm asking because I have been working for some while on proving a fairly big theorem in analytic number theory -- the analytic continuation and functional equation of the Riemann zeta function -- which @Kevin Buzzard and others had led me to believe would be welcomed in mathlib. Sadly, this seems to be nearing completion just as the door is closing for new mathlib3 contributions. It's a bit harsh to be told after several months of work that one's efforts are "a step in the wrong direction". :frown:

My project uses a pretty wide range of stuff from all over mathlib (measure theory, complex analysis, etc); so it will be months before the prerequisites are ported to mathlib4, even at the current impressive rate of porting progress -- I gather mathlib4 doesn't even have real numbers yet. This also means that I'm unable to contribute anything meaningful myself to porting, since the only mathlib files I feel I understand are far higher up the import hierarchy than the porting project has yet reached. So what should I do with my nearly-complete project?

• Put it on ice for now, and wait (potentially many months) until mathlib4 catches up with its prerequisites?
• Make mathlib3 PR's, and run the risk that no maintainer has time to look at them because they're all busy on the port?

Some general guidance on this would be appreciated. I'm sure I'm not the only contributor to mathlib who is finding the current situation a bit puzzling and frustrating.

[Yaël Dillies]

The second option will definitely be faster, but probably still quite frustating.

[Yaël Dillies]

I personally still very much review mathlib PRs, and a few other reviewers too: Eric, Anne, Yury...

[Riccardo Brasca]

I think it really depends on you medium/long term goals. Of course we really want analytic continuation of the zeta function in mathlib sooner or later, it is an impressive result!

Are you interested in learning lean 4? If yes you can just help with the port and at some point run mathlibport on your project (hopefully it will work even better than today), so the only problem is that you result is not in "official" mathlib, but you can of course publish it on github. Note that updating mathlib is now a fairly easy job, since the rate of accepted PR is quite small.

You can also start opening small PRs, but if you modified already ported files you'll have to learn a little bit of Lean 4 anyway. In any case I think you should make the result public as soon you feel is ready, in mathlib or not it's not very important at the moment.

[Jireh Loreaux]

Currently what I am doing with my own projects and those of my students is to wait for the port to catch up and then I will use mathport to translate them, as Riccardo mentioned. It's not ideal, but hopefully it will all be over after several months.

[Riccardo Brasca]

In any case case porting is much easy that writing from scratch, so I wouldn't say that this was a step in the wrong direction!

[Jireh Loreaux]

(deleted)

[David Loeffler]

I wouldn't say that this was a step in the wrong direction!

I didn't say it -- that was a direct quote from @Kevin Buzzard's post quoted by Remi at the start of this thread.

[Rémi Bottinelli]

From personal experience (since I got @'ed ): helping porting files to mathlib4 is really quite straightforward in the cases I dealt with, so I'd suggest giving that a go; and you get to see new landscapes closer to the foundations of mathlib, which is quite fun.
As for PRs to mathlib3, it definitely feels a bit like swimming against current in some cases, and the policy of keeping ported files in sync makes you think twice before doing a PR on such a file. I guess it depends a lot on what you're working on and the attitude of the maintainer at the other end of the PR.

[Jireh Loreaux]

David, note that Kevin was specifically talking about PRs. Working with Lean 3 with mathlib is certainly fine, and we'll definitely want the results in mathlib at some point, it's just that now might not be the best time to PR and merge them. I'm sure @Kevin Buzzard wouldn't argue that the work you've undertaken was a step in the wrong direction.

[Sebastien Gouezel]

David Loeffler said:

Some general guidance on this would be appreciated. I'm sure I'm not the only contributor to mathlib who is finding the current situation a bit puzzling and frustrating.

Since your project is very much ahead of the tide, I think it's perfectly fine to go on making PRs with the new material if it doesn't touch basic files. And if you ping me I'll try to review them quickly, to make sure that everything has the time to go through before the switch.

[David Loeffler]

OK, so it seems that I was reading too much into Kevin's "step in the wrong direction" comment; I see now that it was extracted from a discussion about #17832, which modifies the very low-level file data.list.basic, a very different scenario to my project. It is good to know that PR's are still welcomed for stuff higher up the import hierarchy.

[Scott Morrison]

That's right. I think that PRs that touch low-level files probably should only be happening if the authors know enough to know that this will help the port, rather than hinder.

If you're only working on advanced material, and in particular if you're proving cool theorems, please keep PRing!

It's a balancing act, obviously, but we really don't want to squash people's enthusiasm for doing maths in Lean. :-)

[Kevin Buzzard]

Hi @David Loeffler and sorry for the delay (start of term).

I think that formalising mathematics is a step in the right direction. I think that in general making more Lean 3 PRs is a step in the wrong direction, but I also think that it's rather more nuanced than that. I think that me saying out loud "making more Lean 3 PRs is a step in the wrong direction" is quite a good way of beginning to deal with the issue that we have over 500 mathlib3 PRs and a few months ago they were still pouring in at a terrifying rate.

In a parallel universe, the mathlib maintainers decided that porting and growing at the same time was not feasible, and announced a freeze on all mathlib3 PRs. In fact this might still happen, although I am now beginning to believe that it won't.

You are not the only person who is in the middle of PRing a big project -- indeed there are people who I "manage" (PhD students and post-docs) in the same situation. The reason I'm not too bothered about the situation is that I am convinced that ultimately their projects and yours will end up in mathlib4 somehow, although I am unclear whether the route is "PR to mathlib3 and then get them ported" or "wait until the port is done and then autotranslate them and PR them to mathlib4" or perhaps a combination of the two.

I believe that porting files from lean 3 to lean 4 will get easier, and by the time mathlib is ported it shouldn't be too difficult to start porting other things (like random PRs to mathlib4 which haven't been merged yet). I do think that it's temporarily a difficult situation right now. But I do wonder whether the general lack of reviewers will discourage people who just want to fiddle, or add a couple of lemmas, and that ultimately what will happen will be that it will just be people working on big projects who get attention (e.g. I might well go back to mathlib3 PR reviewing but might just review stuff in my own area or by people who I believe need encouraging). To prove that right now it is still possible to get big projects into mathlib, the final PR of Oliver Nash's work proving the theorem of Gallagher which pertained to some of Maynard's work just made it into mathlib last week.