Zulip Chat Archive

Stream: Lean Together 2026

Topic: Johan Commelin - The Mathlib Initiative


Jireh Loreaux (Jan 19 2026 at 14:19):

Discussion thread for the talk.

Snir Broshi (Jan 19 2026 at 14:29):

Do merge conflicts count as a review cycle? They cause PRs to leave the queue

Johan Commelin (Jan 19 2026 at 14:50):

Slides: LT26_Mathlib_Initiative.pdf

Johan Commelin (Jan 19 2026 at 14:51):

Snir Broshi said:

Do merge conflicts count as a review cycle? They cause PRs to leave the queue

Yes, everything that causes the PR to leave the queue counts.
Of course, you could argue that merge conflicts shouldn't cause a PR to leave the attention queue of reviewers. :smiley:


Last updated: Feb 28 2026 at 14:05 UTC