PSA: queue crisis

Stream: general

[Johan Commelin]

Dear mathlib community, you may have noticed that the PR #queue has sky-rocketed over the last few weeks. This is a sign that activity is booming, and we are very happy about that! But it is also causing a lot of unnecessary stress among the community because of neglected PRs, PRs blocking progress, etc...
As maintainers we are aware of this "minor crisis", and we want to come with a scalable long-term solution. Please bear with us for a few more days while we develop a proposal, and stay tuned! -- The maintainer team

[Damiano Testa]

While the process might not be as quick as desired by the author of a PR, the end result is that I'm usually much happier with the merged PR than the original proposal!

So, maintainers, thank you very much for all your hard work and know that I am incredibly grateful about the whole process: I'd rather it be slow and thorough than quick and sloppy!