2 million

Stream: mathlib4

[Floris van Doorn]

Mathlib has reached 2 million lines of code as of October 28. Thanks to everyone that contributed to Mathlib during the roughly 8 years of Mathlib's existence!

[Kevin Buzzard]

I heard that over 300k of those lines were blank ;-)

[Julian Berman]

Without checking who's correcterer (if either are even any good at counting Lean), cloc and tokei seem to roughly agree:

⊙  cloc Mathlib Archive Counterexamples                                                                                                                                                                                                                                          julian@Mac
    7222 text files.
    7221 unique files.
       1 file ignored.

github.com/AlDanial/cloc v 2.06  T=3.24 s (2227.9 files/s, 594792.5 lines/s)
-------------------------------------------------------------------------------
Language                     files          blank        comment           code
-------------------------------------------------------------------------------
Lean                          7208         377629         296057        1253919
Markdown                        13             53              0            152
-------------------------------------------------------------------------------
SUM:                          7221         377682         296057        1254071
-------------------------------------------------------------------------------

~/Development/Mathlib4 is a git repository on master
⊙  tokei Mathlib Archive Counterexamples                                                                                                                                                                                                                                         julian@Mac
===============================================================================
 Language            Files        Lines         Code     Comments       Blanks
===============================================================================
 Lean                 7209      1927608      1252077       335980       339551
 Markdown               13          205            0          152           53
===============================================================================
 Total                7222      1927813      1252077       336132       339604
===============================================================================

[Aaron Liu]

does that mean we only have 1.9M lines?

[Julian Berman]

Obviously the site is counting lines some different way (or including more than the 3 dirs I included), let's see how...

[Julian Berman]

Looks like it includes all files in the repo probably, it's the code around here: https://github.com/leanprover-community/mathlib_stats/blob/df5630f7b98ecbdbee7e48463d8835bb9aaa3071/gitstats.py#L550

[Bryan Gin-ge Chen]

As you can see from some of the comments around there, I was thinking of modifying that code to let us show graphs for various top-level directories at some point. I probably won't be able to get to it for a while, but I'd be happy to review PRs from anyone who wants to modify the calculation.

[Snir Broshi]

and π * 10⁴ PRs/issues :upside_down::tada: