mathlib PR etiquette

Stream: mathlib4

[Vasily Ilin]

What is the polite thing to do to get my PRs reviewed? Both have not been reviewed for a week. PRs: https://github.com/leanprover-community/mathlib4/pull/19896 and https://github.com/leanprover-community/mathlib4/pull/19886

[Edward van de Meent]

unfortunately, due to the sheer number of PRs to mathlib, it takes a long time (weeks/months) to get PRs reviewed and merged. I suspect that with the holiday season right now, that is especially true. i think patience is the name of the game here.

[Yaël Dillies]

... although you should feel free to start a topic in #PR reviews for each (group of) PR(s)

[Yaël Dillies]

FYI you can write #19886 and Zulip will display it as #19886

[Edward van de Meent]

that will also make the github mathlib4 bot be able to find it, to mark it with emojis as status updates

[David Loeffler]

Volunteering to review others’ PRs is also an excellent way of persuading them to do likewise for your own!

[Violeta Hernández]

The PR queue is very big and stuff won't be reviewed instantly, but it shouldn't be taking 2+ weeks either.

[Violeta Hernández]

I think past that point is when you can ask in #PR reviews.

[Violeta Hernández]

There's a few exceptions of course. If a PR is big (300+ lines) then review will take longer. But you can often take such a PR and split it into various smaller self-contained PRs.

[Violeta Hernández]

A PR might also be in a very specialized topic, in which case it's probably best to directly ping someone who also knows about/has contributed to said topic.

[Violeta Hernández]

(e.g. me for anything set theory related :stuck_out_tongue:)

[Vasily Ilin]

Violeta Hernández said:

I think past that point is when you can ask in #PR reviews.

What do you mean by "ask in #PR reviews"?

[Junyan Xu]

I think she means opening a new topic in #PR reviews