Project statistics

Stream: condensed mathematics

[David Michael Roberts]

I thought it might be interesting to keep track of how the LTE is going as far as length of code produced. I appreciate it may not be easy with material going into mathlib, so maybe even just tracking the main self-contained parts is reasonable. Is there any automatic way to do this? Or are the parts all moving too fast at present?

[Johan Commelin]

@David Michael Roberts Does https://github.com/leanprover-community/lean-liquid/pulse give you some of the stats you want?

[Johan Commelin]

You can also run git ls-files | xargs wc to get very rough line-count statistics

[David Michael Roberts]

I'd checked that, but it only goes back so far. I found this online tool that seems to a reasonable job, giving a current snapshot only: https://codetabs.com/count-loc/count-loc-online.html (so no historical added/removed)

[Johan Commelin]

I'm giving a talk about LTE later today, so I decided to gather a bit more statistics.

• Scholze's proof: $\approx 12p \quad (+ 3p \quad\text{BD resolutions})$
• Blueprint: $\approx (2\,000l, 12\,000w, 87\,000c) \approx 21p$
• Lean code: $\approx (20\,000l, 120\,000w, 1\,060\,000c)$
• strip-lean.tar.gz $= 512\,798b \quad$ (nofor_mathlib/)
• strip-blue.tar.gz $= 23\,846b$
• De Bruijn factor $= \frac{512\,898b}{23\,846b} \approx 21.5$

[Scott Morrison]

Which you interpret to mean ...? :-)

[Johan Commelin]

I don't really interpret. That's the job of my audience...

[Johan Commelin]

It seems that the blueprint compresses better than the lean code. So I guess there's more redundancy in the blueprint? :stuck_out_tongue_wink:

[Johan Commelin]

(Edit: I forgot to count 8.17 and 8.19, so the proof in Analytic.pdf is more like 12p.)

[Riccardo Brasca]

Is the talk public?

[Johan Commelin]

http://individual.utoronto.ca/groechenig/K.html

[Scott Morrison]

Johan is on at 2021-05-27T02:00:00+10:00 . Too late for me. :-)

[Johan Commelin]

Sorry :shrug: I'm also not sure it's recorded. But ey, you guys won't here anything new anyways.

[Sebastien Gouezel]

How come the Lean text only compresses by a factor of two? It's just text, right, with a lot of words coming back, so it should be much better. Or has it something to do with unicode? I guess a more efficient compression engine would give different results.

[Johan Commelin]

I'm not a compression expert...

[Johan Commelin]

-rw-rw-r-- 1 jmc jmc  21764 May 26 08:08 strip-blue.tar.xz
-rw-rw-r-- 1 jmc jmc 468512 May 26 08:08 strip-lean.tar.xz

[Johan Commelin]

lz4 only makes things worse

-rw-rw-r-- 1 jmc jmc  37870 May 26 08:12 strip-blue.tar.lz4
-rw-rw-r-- 1 jmc jmc 619758 May 26 08:12 strip-lean.tar.lz4