Welcome and first steps

Stream: triage team

[Michael Rothgang]

Hello everybody! I'm so glad all of you are interested in helping out with PR triage. I have some ideas, but am neither perfect nor a dictator --- so let's figure out what we want this to mean in practice.

[Michael Rothgang]

Here are some ideas what triage could look like

1. look at PRs without an area label and see if any PR in that list should be labelled CI, IMO, t-something. I did so last week, so I guess there may only be a few ones remaining. (Eyeballing it now, perhaps the 10 first could use a label.)

[Michael Rothgang]

2. Find assignees for PRs which need one. This list shows PRs which have not received updates in the past two weeks, and don't have an owner.
   If you see somebody suitable, you can certainly ask them directly. An easier way is to use automated suggestions: there is a bot making suggestions (for always 10 PRs); this file contains the current ones (in the format number: handle; right now, it would suggest assigning #22231 to @ocfnash.
   This will be automated soon, but until then, some manual work is useful.

When I was assigning PRs, I would also look at the comment history: if somebody already made one or more review rounds, it's natural to ask them. (Except if they say "I'm not an expert, these are just superficial comments" :-)) In general, your guess doesn't have to be perfect --- one can always re-assign!

[Michael Rothgang]

3. Look at stale pull requests and try to clarify their status.
   Some are clearly obsolete (such as, "Lean testing PRs" corresponding to already-merged Lean core PRs). For some, you can see what action might be required, and it's fine to ask the author to do so. For others, things are more controversial and what's really needed is a decision if the PR's change is considered really desired. An ideal response could be to prompt discussion about the PR --- but even just asking here and hearing a second opinion is fine.

4. You may have other ideas, feel free to do your own! There are lots of PRs, there should be lots of useful work --- as long as we end up doing something useful regularly, I think that's great.

[Michael Rothgang]

With all that said: would somebody like to volunteer for doing triage this week?

[Edward van de Meent]

Should the domain of PRs we look at include draft PRs/PRs marked WIP?

[Edward van de Meent]

(i suspect these should at the very least be of lower priority)

[Michael Rothgang]

I would say yes, and agree with your second commit. Sometimes, PRs are wrongly marked as draft (or draft PRs have served their purpose and can be closed). That's probably the less common case, though.

[Paul Lezeau]

I probably won’t be able to do much for the next two or so weeks, but I’d be happy to volunteer for triage the week after!

[Michael Rothgang]

Thanks a lot, Paul! So, let me put you in for next week (May 26 until June 1).

[Michael Rothgang]

Would somebody like to step in for this week? One straightforward way to help could be by assigning reviewers. Automatically doing so hit a snag, so manual work could be very useful until CI issues are resolved.

[Michael Rothgang]

Steps to do so:

• visit https://leanprover-community.github.io/queueboard/automatic_assignments.json. Each entry in that file maps a PR number to a suggested assignee.
• go through that list one by one: in the simplest case, you can simply open the PR and assign it to the person on the list
• advanced version: see if a mathlib reviewer or maintainer already reviewed the PR. If they did, assign it to them. If somebody else reviewed, I would be careful with assigning to them --- but you could ask if they have further comments, for instance.

Once you went through the file, wait for a day and repeat :-)

[Paul Lezeau]

Michael Rothgang said:

Thanks a lot, Paul! So, let me put you in for next week (May 26 until June 1).

Slightly hectic week - I haven't been able to make a start on triage yet, but hopefully will tomorrow!