How effective is bot auto-assigning reviewers?

Stream: mathlib4

[Weiyi Wang]

I often see that who ended up actually reviewing my PRs were different from the one assigned by the bot, so I wonder how effective the bot is.

[Kim Morrison]

Would you be interested in doing an analysis, or suggesting improvements to the algorithm? Either would be great for someone with appropriate expertise.

[Weiyi Wang]

Oh, that sounds like a fun investigation. I can try soon

[Monica Omar]

I feel like one way to improve this is by seeing if the assigned reviewer hasn't interacted with the PR for longer than say, 3 weeks, then it should probably get reassigned?
Also, sometimes when people unassign themselves, the bot reassignes them back. So another improvement is that we could add a condition saying that the bot can't reassign the same person?

[Bryan Gin-ge Chen]

As of changes made ~2 weeks ago, the bot should no longer reassign a reviewer to a PR if they were manually unassigned from that PR. Let me know if you notice it happening still!

I'm also currently working on something to unassign reviewers if they haven't managed to get a PR off the queue after a configurable amount of time (the default will be 21 days). This will come after some Zulip integration to send notifications / allow reviewers to modify their assignment preferences.