alt Hacker NewsUnfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Replies
Static linking wonders?
Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
The name is amusingly ironic now.
Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.
Also, I dislike that they are using Github as the default package registery. But as this langage was created inside Microsoft, it makes senses.