Hacker News Reader

Comment by unexpectedtrap | Hacker News Reader

Unfortunately 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.

View on HN

Also, I dislike that they are using Github as the default package registery. But as this langage was created inside Microsoft, it makes senses.

Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.

>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.

> Lean is far off the most bloated one. Isabelle most likely takes that spot.

Among these three is the operative phrase here.

I hate to be pedantic, but we are talking about theorem provers here :)

That is a fair point, thank you for the correction there

Static linking wonders?

Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.

No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel, this part of a codebase has hardly changed since Lean 3). Almost all the space in the package (more than 2.5 GiB) is taken up by .olean/.ilean/.ir files, approximately 1 GiB of which is generated from the code of Lean’s frontend itself (i.e., parser, elaborator, core tactics, and so on) and the other 1 GiB from a standard library. As you might guess, these files are IR and essentially a compiled Lean’s environment (something like a Lisp image), so that Lean can load them straight up without recompiling and rechecking everything.

There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.

Thanks for the overview.

The name is amusingly ironic now.

was LeanB4

Reply on news.ycombinator.com