review/triage meetings

Stream: mathlib4

[Kevin Buzzard]

As many people reading this channel will be aware, mathlib has a huge PR backlog: there are currently 1,171 open pull requests https://github.com/leanprover-community/mathlib4/pulls at the time of writing and this number slowly increases over time.

I'm proposing running weekly triage meetings on Zoom on Mondays for the next 9 weeks, 1 hour long and at varying times of day so as to maximise the possibility that interested people will be able to come along. A bunch of people who review PRs for mathlib will be there, and we will try and get the queue moving along by either reviewing, or merging, or assigning reviewers to PRs. Anybody is welcome to come.

The times of the remaining meetings are

2025-02-10T10:00:00Z
2025-02-17T17:00:00Z
2025-02-24T09:00:00Z
2025-03-03T14:00:00Z
2025-03-10T10:00:00Z
2025-03-17T15:00:00Z

(these should display in your local time zone) and here is the Zoom link.

It is worth stressing that anyone can review a mathlib PR, you don't have to be a maintainer or an "official" reviewer of any kind; all contributions are welcome!

[Jireh Loreaux]

Kevin Buzzard said:

It is worth stressing that anyone can review a mathlib PR, you don't have to be a maintainer or an "official" reviewer of any kind; all contributions are welcome!

In fact, if you would like to get a better understanding of what considerations are involved in review, this is a good opportunity to learn from experienced reviewers.

[Riccardo Brasca]

@Kevin Buzzard I think you should post this in #announce !

[Kevin Buzzard]

OK done!

[Shreyas Srinivas]

So are these like review tutorials?

[Ruben Van de Velde]

Not only, but they can be that as well

[Kevin Buzzard]

We'll see what they turn out to be. But we've run a few of these in the past and my vision is that we isolate "problematic" PRs (e.g. ones which have been on the queue for too long without moving forwards) and we try to figure out how to move them forwards (e.g. by closing them or explciitly approaching someone and asking them if they could review or by making a few comments on the PR or...)

[Yaël Dillies]

I would also encourage people who are willing to learn how to review to come along

[Yaël Dillies]

Oh, I wrote this message several hours ago

[Kevin Buzzard]

Just a reminder that the first of these meetings is in 15 minutes.

[Kevin Buzzard]

ALso a reminder that we have the #queueboard nowadays.

[Kim Morrison]

Oops, I'd written down the wrong time for this meeting. How did it go?

[Yaël Dillies]

I arrived 45min late myself, but it felt like we didn't hit many particularly difficult PRs. Most of them I could have reviewed on my own

[Kim Morrison]

I guess we need some of both -- triage meetings that just plough through easy stuff, so new reviewers can see what's going on, and triage meetings that make hard decisions.

[Michael Rothgang]

I can well imagine that just going over the oldest entries in the queueboard will turn from "oh, here are lots of PRs that kind of got forgotten" to "so, we have to make a hard decision about this one".

[Kim Morrison]

I think a good way to deal with the hard decisions is to come up with some decision, which won't be perfect, post a new thread on the mathlib reviewers stream linking to the PR and proposing an outcome (often: "I propose to tell the author that we are going to close."), wait a few days for emoji reactions or complaints, and then proceed.

To me this feels much "safer" than deciding on the spot to close something, which we are all still cautious about.

[Yaël Dillies]

Happening now

[Kim Morrison]

Let's try to have announcements a day (or even hour) ahead of time. Scheduled messages help here.

[Yaël Dillies]

Yes, sorry! I was busy until the time, and also half-expecting Kevin to have sent a reminder

[Kevin Buzzard]

I have a working calendar so don't need reminders. I would have no idea how to set up an automatic reminder. But then again it's me setting the times of the meetings :-)

[Johan Commelin]

Next to the big purple "send this message" button, there are three dots with a menu. You can schedule a message there.

[Yaël Dillies]

Okay, I have scheduled a message for next week

[Kevin Buzzard]

Johan Commelin said:

Next to the big purple "send this message" button, there are three dots with a menu. You can schedule a message there.

Oh I had no idea it was so easy! Thanks!

[Dagur Asgeirsson]

When is the next meeting?

[Yaël Dillies]

2025-02-03T10:00:00+01:00

[Riccardo Brasca]

Can we add this to the official calendar?

[Kim Morrison]

@Kevin Buzzard, could you confirm if there is an ongoing plan? As far as I can see above there is just the announcement of three individual sessions.

[Kevin Buzzard]

The top of this thread gives the times of the next two meetings. There will be meetings throughout Imperial's term (so 9 in total, of which we've had 2). The only reason I have not timetabled all 9 is that some people at Imperial were talking about organizing a study group on learning tactics which might occur on Mondays and which I'd like to attend.

[Violeta Hernández]

I like this initiative, I'd just like to mention that the meetings so far have been at high midnight in my timezone.

[Kevin Buzzard]

OK I am reluctant to change meetings which I've already scheduled but how about we have the one in 2.2 weeks about 8 or so hours after the one we're going to have in 0.2 weeks?

[Yaël Dillies]

Next triage meeting happening in 24 hours!

[Yaël Dillies]

Happening in one hour!

[Riccardo Brasca]

Can someone send the zoom link?

[Yaël Dillies]

I was doing that just now :wink: : https://imperial-ac-uk.zoom.us/j/93990100310?pwd=eTRqiY7b7e2gS4ps8aXIeh8MuGpSa7.1

[Kevin Buzzard]

All the info is in the first message in this thread

[Michael Rothgang]

This is still waiting for a host to start the meeting, right?

[Pietro Monticone]

No, the meeting has already started.

[Michael Rothgang]

Wow, zoom kept me waiting for some time. I see it's started now.

[Yaël Dillies]

@Kevin Buzzard, when is the next meeting happening? I was expecting 2025-02-10T15:00:00+01:00 but from the way you edited your original post I'm thinking it might be 2025-02-10T11:00:00+01:00 instead?

[Violeta Hernández]

(I hate to say this but I might actually be available at 4 AM tonight)

[Kevin Buzzard]

Yes it's the latter. I don't know why you're expecting the former or even mentioning it, as far as I know I never mentioned that time and so you're just causing confusion

[Yaël Dillies]

Oooh, I thought the "The next few meetings are" part of your message was the first few meetings, and the other ones would follow the same days and times on a two weeks cycle :see_no_evil:

[Kevin Buzzard]

No, they were necessarily at random times for reasons I won't go into and will continue to be random (OK so I went into them below)

[Kevin Buzzard]

But I am now finally in a position to timetable them for the rest of term because the one external decision I was waiting for was made last Friday

[Kevin Buzzard]

OK done. Sorry about the delay timetabling these, I knew I had a regular commitment on Mondays starting today but I didn't know when the actual time was until a few days ago.

[Kim Morrison]

You say "OK done", but where is the decision?

[Yaël Dillies]

In the original message: #mathlib4 > review/triage meetings @ 💬

[Yaël Dillies]

There's a typo in your message, Kevin. There are apparently two meetings on Feb 17

[Kevin Buzzard]

Thanks -- fixed (I blame Feb for having 0 mod 7 days)

[Riccardo Brasca]

Is this happening in 20 minutes?

[Andrew Yang]

Is it starting now? I can’t get in.

[Kevin Buzzard]

You're the second person to say this

[Kevin Buzzard]

I must be on the wrong link or something?

[Kevin Buzzard]

Apologies, let's try this!

[Kevin Buzzard]

Next meeting starting in three minutes!

[Kevin Buzzard]

Next meting now!

[Riccardo Brasca]

Trying to fix my internet connection :sweat_smile:

[Riccardo Brasca]

my zoom keep on crashing for some reason, see you next week!

[Kevin Buzzard]

Usually updating Zoom fixes that for me

[Michael Rothgang]

Should we try the new queueboard feature of "links with state" for today's meeting in 15 minutes? For instance, one could use https://jcommelin.github.io/queueboard/review_dashboard.html?sort=10-desc&length=25#queue to see all PRs on the queue, sorted by "longest overall time waiting for review".

[Michael Rothgang]

Has the meeting started? Zoom tells me it hasn't, but that wasn't always reliable in the past...

[Kim Morrison]

There was no announcement, so I guess no one showed up.

[Michael Rothgang]

Kevin, Pietro and I were there (and went over the 20 oldest PRs).

[Eric Wieser]

Can we add these to https://calendar.google.com/calendar/embed?src=231afa9634d9885edc7d39194879135b688661754a1f3e984647ea4769f8ac73%40group.calendar.google.com ?

[Michael Rothgang]

(That calendar is also missing the mathlib community meetings, right?)

[Kevin Buzzard]

There's only one meeting left, which is in 1 week and 3.5 hours.

[Eric Wieser]

I think the issue is that almost no one has write access to that calendar right now (pretty much just the admin team). I'll ask the maintainers if we can change that.

[Michael Rothgang]

The next meeting is tomorrow at 4pm Berlin time, i.e. in 28:02 hours - right?

[Kevin Buzzard]

Yes that agrees with what is in my diary. Tomorrow is the last Monday of term for me -- I shall be away for the two Mondays afterwards so can't lead any potential future. Maybe after the final meeting we can discuss what the series achieved and if we want to continue it in some form.

[Eric Wieser]

Eric Wieser said:

Can we add these to https://calendar.google.com/calendar/embed?src=231afa9634d9885edc7d39194879135b688661754a1f3e984647ea4769f8ac73%40group.calendar.google.com ?

Now done for the 5 previous meeting and the upcoming one

[Kim Morrison]

2025-03-18T02:00:00+11:00

[Yaël Dillies]

Now!

[Johan Commelin]

https://imperial-ac-uk.zoom.us/j/93990100310?pwd=eTRqiY7b7e2gS4ps8aXIeh8MuGpSa7.1