Milestone

Stream: mathlib4

[Winston Yin (尹維晨)]

I believe mathlib4 recently exceeded the number of PRs that mathlib3 ever had! mathlib3#19245 was the largest mathlib3 PR I could find, but mathlib4 is already at #19359.

[Michael Rothgang]

To compare: for the same number of non-porting PRs (i.e., excluding approximately these), mathlib3 took about three years (July 2020 until June 2023), whereas mathlib4 did the same in 18 months. Exciting!

[Ruben Van de Velde]

As a reviewer: :scream:

[Riccardo Brasca]

This is great, but I think one big reason is that we have nowadays a lot of "maintenance" PRs (like splitting files, small refactors). I am not sure the actual mathematical growth of mathlib has increased.

[Shreyas Srinivas]

How many LoC is mathlib these days? I recall that there is a tool for getting these stats, but can't remember what it is called.

[Markus Himmel]

It's this webpage: https://leanprover-community.github.io/mathlib_stats.html

[Yaël Dillies]

Are we gaining 100k LoC every month? :flushed:

[Jireh Loreaux]

I think it's closer to 30-40k.

[Yaël Dillies]

I compute ~60k on the period 22/10-22/11