[unexpectedtrap]

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.

[ebonnafoux]

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

[c0balt]

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

[senko]

>> 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 :)

[c0balt]

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

[pjmlp]

Static linking wonders?

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

[unexpectedtrap]

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.

[pjmlp]

Thanks for the overview.

[jandrese]

The name is amusingly ironic now.

[redrobein]

was LeanB4