3 ms·

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

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 6mo ago
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 6mo ago
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 6mo ago
  >> 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 6mo ago
    That is a fair point, thank you for the correction there
pjmlp 6mo ago
Static linking wonders? Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
- unexpectedtrap 6mo ago
  No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel 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 6mo ago
    Thanks for the overview.
jandrese 6mo ago
The name is amusingly ironic now.
- redrobein 6mo ago
  was LeanB4

ebonnafoux 6mo ago

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 6mo ago

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 6mo ago
>> 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 6mo ago
  That is a fair point, thank you for the correction there

pjmlp 6mo ago

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

unexpectedtrap 6mo ago
No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel 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 6mo ago
  Thanks for the overview.

jandrese 6mo ago

The name is amusingly ironic now.

redrobein 6mo ago
was LeanB4