Number of open PRs

Stream: mathlib4

[Jeremy Tan]

(btw there are now less than 1000 open PRs in mathlib4)

[Jeremy Tan]

image.png

[Kevin Buzzard]

(It currently oscillates around 1000)

[Kim Morrison]

(which hopefully everyone involved in reviewing agrees is an embarrassing disaster :-)

[Yaël Dillies]

I think it's not so embarrassing when you see we are keeping the queue at around 200

[Michael Rothgang]

I'd like to take a closer look at those PRs before making such a blanket statement: of these 1000 PRs,

• about 200 are ready for review
• about 150 are blocked by other PRs (these are fine; as long as PRs get reviewed quickly, this is an expected transient state)
• about 230 are awaiting-author
• 65 just need merge conflict
• about 230 are marked WIP
• the remaining ones I'd need to check more carefully; there are certainly a number of "experiment", "tracking PRs", "testing Lean branch" etc. PRs

[Michael Rothgang]

(By the way: I could add such statistics to the prototype review dashboard. Do you think this would be helpful?)

[Jon Eugster]

Also 166 are marked drafts (which overlaps the categories above). You should probably filter these out separately before analysing the labels on the rest.

[Michael Rothgang]

Indeed, I plan to use a slightly more sophisticated classification scheme: draft status or WIP labels should both count the same, and if labels overlap, one would need to decide which status the PR is in. I have code for both already.

[Michael Stoll]

I have closed two of my PRs (which were experiments that are superseded by the two PRs mentioned in the next sentence). Is there interest in reviving #12679 and/or #12778 (@Yaël Dillies who effectively blocked the latter in view of their planned order vs. algebra refactor)?

[Michael Stoll]

(BTW, shouldn't this thread be in the mathlib4 channel?)

[Notification Bot]

This topic was moved here from #general > Number of open PRs by Johan Commelin.

[Michael Rothgang]

The dashboard now has a section with statistics. The code takes great care to only assign one status to each PR (say, a PR which is awaiting-author, WIP and a merge conflict is considered as "work in progress").