Frustration around existing tooling and the review process

Stream: mathlib4

[Emilie (Shad Amethyst)]

I'm sending here the frustration I shared about earlier on #9477:

I expected a first contribution to be reviewed and merged in a day or two, but a combination of things has drawn this process out much longer than that, and it has caused my experience to slowly feel frustrating. Let me break down the factors that led to this, that me and other people have identified; some are out of anyone's control, while I think some could be solved by improved documentation or tooling:

• Lean together happened last week, so a lot of active users were busy with preparing or attending talks
• There was already a bit of backlog on the pull requests (there are ~5 pages of PRs that are actively maintained)
• I'm new and haven't yet fully internalized things like the naming scheme, the way to_additive works, etc.
• There isn't an easy way to run lints locally
• There isn't a formatter (there are talks about it on #7217, but no robust solution exists yet)
• There isn't an easy way to build documentation locally

---

For lints, you can run #lint, but I think it'd be nice to have a lake exe lint command that would do it for you (ideally it would accept as input a list of files to check), so that this step can quickly be ran from the terminal.

---

There are talks about writing a formatter, and there have been some attempts before. I do believe that getting a formatter up and running should be a big priority, since it would move most of the coding style issues that may be be pointed out in a review to something solved automatically, and done from the terminal.

---

From what I can see, documentation isn't built on non-master branches in the CI, so I have to build things locally if I want to check that I didn't screw up something. Doing so has been surprisingly difficult:

• the instructions in the README are incorrect (you first need to run lake -R -Kdoc=on update to retrieve the doc-gen4 dependency, then lake -Kdoc=on build Mathlib:docs to start the build, and the output is placed in .lake/build/doc, not in build/doc)
• the docs take ages to build (~2h for a cold run, and ~10' for a hot run); this is in contrast with languages like Rust where a cold run takes 2 minutes at most
• re-running lake -Kdoc=on build Mathlib:docsdoes not update files changed; instead, I have to nuke the corresponding generated file in the build directory for it to behave as expected
• the above issue means that when switching branches or rebasing, the docs have to be rebuilt from scratch (which takes 2 hours ☺)
• there are quirks related to documentations that aren't caught by linter rules:
  • if --/ is put at the end of a comment and the comment is multi-line, then a - will be placed on a new line after the text above, turning it into a title or creating an empty list (as in the module documentation of docs#CategoryTheory.MorphismProperty.IsCompatibleWithShift)
  • to_additive doesn't copy over documentation by default (as in docs#FreeAddMonoid.uniqueAddUnits)
  • etc.

---

I do think that the last three issues are something that, if solved or improved, would make contributions much easier for both new contributors, old contributors and reviewers.

[Anatole Dedecker]

Regarding documentation, the current solution is quite simple: we don’t expect contributors to check that the documentation is generated correctly during the PR process. Of course it would be better to have the tooling, but for now I’d say you can count on the reviewer to point out mistakes, and if anything bad happens you can open a PR with the "easy" tag to fix it and it will probably be merged in at most a day.

[Yury G. Kudryashov]

Emilie (Shad Amethyst) said:

I expected a first contribution to be reviewed and merged in a day or two, but a combination of things has drawn this process out much longer than that,

In the past year or two, the project became much bigger and our procedures and tooling are still adjusting. We're working on this but most people here are volunteers who contribute in their free time, not paid developers. In particular, AFAIK, there are exactly 0 people who are being paid for reviewing PRs.

Thank you for your feedback!

[Anatole Dedecker]

Regarding the timescale, unfortunately the reality right now is that your expectations are usually not met. I don’t have precise data points, but from experience I would say that the typical time for a new contributor to get his first PR merged is about a week, and it can get much longer for too ambitious PRs. Of course we would all love to get that time down, and any feedback on that is much appreciated, but I just want you to know what to expect.

[Emilie (Shad Amethyst)]

In the past year or two, the project became much bigger and our procedures and tooling are still adjusting. We're working on this but most people here are volunteers who contribute in their free time, not paid developers. In particular, AFAIK, there are exactly 0 people who are being paid for reviewing PRs.

That is true, I should have phrased this differently, please pardon my clumsy wording. I wasn't expecting the review to be done in a few days, but I was hoping that the review process would allow me to synchronously write my contributions and get them merged.

I really do appreciate all the work that has gone into mathlib, and I think mathlib is one of humanity's most honorable ongoing projects :)

[Emilie (Shad Amethyst)]

Regarding the timescale, unfortunately the reality right now is that your expectations are usually not met.

I'll have to adapt my working style around that, yeah. In the past I spent a lot of time on projects where I could simply rebase branches willy-nilly onto one another, and it would take me long enough to implement changes on new feature branches that by the time I'm done, the previous changes that I rely on were most likely already merged.

I'll be attempting a different method, inspired by LeanAPAP, where I do all of the contributions in one go on a draft branch, then split those over time into small, neatly-separated PRs, cherry-picking suggestions made in reviews back to the main draft branch.

[Anatole Dedecker]

Yes, I think a lot of people here use that kind of workflow.

[Alex J. Best]

Regarding the linter you can run lake exe runLinter Mathlib locally indeed for the main linters (and a separate script in scripts for the style linters.). Almost everything that CI does is inside the main mathlib repo (or a dependency). Why do we not recommend this to newcomers so often though? One reason is that in order to lint all of mathlib you need to build all of mathlib, and this takes some time so many people choose to let CI do it for them. Of course if you have a great machine to work on this workflow may not be optimal for you

[Alex J. Best]

Regarding the formatter, there is some basic work on autofixes in the aforementioned style linter scripts https://github.com/leanprover-community/mathlib4/blob/master/scripts/lint-style.py. Looking at your PR the <- being changed to a left arrow is absolutely something that script could and should do for you. Myself I have these linters and auto-fixers run automatically whenever I save a lean file

[Alex J. Best]

But yeah I agree with many of your points, and many of us would like to see these things improved. It is simply a question of enough motivated people having enough time available to do so, it's not a conscious choice of this community not to try and improve the first PR experience or anything like that.

[Patrick Massot]

I think you also very very much underestimate the difficulty of writing a code formater for a language that is as extensible as Lean. This has nothing to do with writing a code formater for python or javascript.

[Patrick Massot]

And I'm also very curious to know what are the open source projects that you contributed to and where PRs get merged in a day or two.

[Yury G. Kudryashov]

Patrick Massot said:

And I'm also very curious to know what are the open source projects that you contributed to and where PRs get merged in a day or two.

When I opened my first mathlib3 PR (very messy, didn't complete it), I've got a very detailed review next day (AFAIR, from Mario). For me, this was probably the most important argument for joining the project. But the library was so much smaller back then, both in size and in the number of open PRs...

[Winston Yin (尹維晨)]

Anatole Dedecker said:

Regarding the timescale, unfortunately the reality right now is that your expectations are usually not met. I don’t have precise data points, but from experience I would say that the typical time for a new contributor to get his first PR merged is about a week, and it can get much longer for too ambitious PRs. Of course we would all love to get that time down, and any feedback on that is much appreciated, but I just want you to know what to expect.

My first PR took at least a couple of months. My second PR, took over a year, even after detailed review and verbal approval. I try to understand that reviewing PRs is hard work, especially by volunteers, but the experience is definitely frustrating, by nobody’s fault. In fact, I’m very impressed by the detailed review I did get, from the four or so reviewers I encountered.

All this also depends on the area of maths you work on. There’s definitely a bias towards algebra, and I usually take any delay in reviews to mean I’m doing something new, and fewer people are comfortable reviewing it.

But I wonder if there’s a better system to prevent very constructive PRs from rotting for months just because the one or two relevant reviewers get too busy. Perhaps there should be a process / standard for training and onboarding more and more qualified reviewers.

[Winston Yin (尹維晨)]

Has anyone made a plot of (PRs per day)/(number of reviewers) as a function of time? I argue it should be at least linear.

[Winston Yin (尹維晨)]

On second thought, the growth of mathlib looks linear, and we ought to have been attracting more and more contributors, so my hypothesis is that the growth is reviewer-limited. This suggests directing more resources to training more reviewers.

[Kim Morrison]

I think specifically it is more "willingness" / "availability" than "expertise" / "credentialling" that is the limiting factor.

While there is a designated status "reviewer", of course anyone and everyone can and should review. That status is a combination incentive/reward and signal that the maintainers will typically quickly merge something approved by a "reviewer".

I do tend to agree with the idea that review availability may well be the principal limiting factor.

[Jireh Loreaux]

Note, we do have a PR review guide which teaches the basics of reviewing Mathlib PRs to any interested party. In fact, it is even designed to be graduated in the sense that it teaches the easiest tasks associated with reviewing first and then progresses to harder questions to answer.

[Jireh Loreaux]

Note also: the squeaky wheel often gets the grease. If you have a PR languishing, explicitly requesting a review (or what it would take to finish up) on Zulip can help be the impetus.

[Michael Rothgang]

Winston Yin (尹維晨) said:

On second thought, the growth of mathlib looks linear, and we ought to have been attracting more and more contributors, so my hypothesis is that the growth is reviewer-limited. This suggests directing more resources to training more reviewers.

We don't have statistics for the length of the PR (or the review) queue, right? (Rust has this, which is great.) My impression is that the queue is getting longer and longer (with the usual fluctuations), which makes me believe reviewer capacity is definitely a bottleneck here.

[Kim Morrison]

#queue is at ~170 right now. Before the Lean 3 to Lean 4 transition I recall it rarely being above 100.

[Martin Dvořák]

Winston Yin (尹維晨) said:

This suggests directing more resources to training more reviewers.

I think we need more reviewers, too.
I would especially like to point out that on the list
https://github.com/leanprover-community/mathlib4?tab=readme-ov-file#maintainers
there are currently no maintainers dedicated to the Computability and Data sections.
As a result, I frequently have trouble finding people to review my PRs in these areas.

[Martin Dvořák]

On the side of tooling, however, I think Lean 4 is doing great for how young the language is!

[Jireh Loreaux]

#queue will be coming down soon I believe. Looking at it the Monday or Tuesday after Lean Together isn't really representative. The week before I think it was closer to 100.

But yes, more people participating in review (note: they don't need to be labeled as "reviewers" with that title) is essential. This is the reason we have the PR review guide.

[Jireh Loreaux]

@Martin Dvořák are you having trouble with getting any reviews (indicative of the fact that we have very few people working in computability as a whole) or with getting already reviewed (even by a non-maintainer) PRs merged?

[Martin Dvořák]

Jireh Loreaux said:

Martin Dvořák are you having trouble with getting any reviews (indicative of the fact that we have very few people working in computability as a whole) or with getting already reviewed (even by a non-maintainer) PRs merged?

Troubles with getting PRs merged are expected. Waiting for reviews could be cut down, however.

[Jeremy Tan]

I actually named the branch for #9736 trabant because just after that PR was opened there were exactly 601 open PRs