meta code reviewers

Stream: mathlib4

[Kevin Buzzard]

I remembered a few days ago that mathlib4 has a #queue4 ! I had spent months ignoring pretty much everything on it other than porting PRs, and then when the port got done I spent a couple of weeks ignoring it completely (because we were done, right?). But now it's dawning on me that we're back to the good old days and can start writing and reviewing each other's PRs, and growing mathlib in the directions we like.

I was delighted to see that top of the queue was a PR by Scott (which I was completely oblivious of until recently) on presheaves of modules, and I've just reviewed that one (which drops it to the bottom of the queue). This now means that the top eight PRs on the queue are all tagged t-meta which means that they're out of my league. It might also indicate that we have a problem with not enough meta reviewers? Is this an issue which other people are concerned about?

[Jon Eugster]

To what extend would reviews (together with the maintainers merge command) by non-maintainers be welcomed?

[Eric Wieser]

Reviews are certainly always welcome, though maintainer-merge is strictly only recognized by people lists as mathlib reviewers.

[Jon Eugster]

ok perfect! :+1:

[Scott Morrison]

Reviews are very welcome from everyone. You can even make an effort to review the PRs of people who provide reviews, initiating a virtuous spiral of mutual reviewing. :-)

[Mario Carneiro]

Also note that we look at reviews when considering people for addition to the mathlib reviewers and mathlib maintainers teams, so if you are interested in joining these teams then doing reviews will be very helpful!

[Arthur Paulino]

Here's a fun idea: create a reward system for reviews. Person A would get:

1. 3 points per review cycle done by A on a PR not open by A
2. 1 point for each :+1: (not given by A) on review comments made by A on a PR not open by A
3. 1 point for each member (excluding A) that agrees on a :+1: given by A on a review comment not made by A on a PR not open by A

• (1) is an incentive to actually review
• (2) is a mechanism for review validation
• (3) is an incentive to strengthen review validation

For example, suppose there's a certain PR not open by Alice.

• Alice does a review and gains 3 points. She left two comments
• Bob :+1: the first comment, so Alice gets an extra point
• Bob does his round of review and leaves one comment (let's not care about Bob's points)
• Alice agrees with that comment and :+1: it
• Carl comes in and :+1: Bob's comment, so Alice gets an extra point

This is obviously not bullet proof (I didn't even try for it). The system is based on the trust that collaborators already share (people get invites to be collaborators!). There can be seasons, which are good for celebration and also to iterate/improve on the point system.

Note: this is pretty much a form of decentralized consensus algorithm for reviews. It's easy to go crazy on the rules, but it's probably better to start off with something to avoid paralysis by analysis scenarios.

[Eric Wieser]

I think a more coarse approach would be to just count "how many PRs was a person involved in reviewing", and publish that as a stat alongside the commit stats shown in mathlib 3

[Eric Wieser]

Review is a very important part of making mathlib work, so if we're going to leaderboard-ize commits, we probably should do so for review also!

[Arthur Paulino]

Eric Wieser said:

I think a more coarse approach would be to just count "how many PRs was a person involved in reviewing", and publish that as a stat alongside the commit stats shown in mathlib 3

That's definitely a nice start. "being involved" is a bit vague though. The "like"-points I proposed are pretty much incentives to make people really involved with the review process, potentially even increasing review quality. But that's an extra