Why are olean files so big?

Stream: new members

[Mr Proof]

As some context, I come from a game development, where one of the number one priorities is to be very efficient with memory.

So I was kind of confused when I downloaded Mathlib which was 65Mb which seems about right for a bunch of text files.
But when building a new project using: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency the Mathlib folder was about 3.6GB (55x bigger). Considering I thought the olean files are the compiled version my expectation was they would be smaller.

e.g. all the olean files in MyLeanProject\.lake\packages\mathlib\.lake\build\lib\Mathlib\Algebra\Algebra

I had a plan of bundling Lean/Mathlib in with a type of CAS I was making. But at 3-5GB that's not really an option.

Can anyone satisfy my curiosity as for the need for such a big build size? I imagine there is a lot of duplication.

And secondly, are there any plans to optimise this a bit more?

Thirdly, is there any way to run lean without building things into olean files? I tried to import Mathlib without building it and it complained there was no Mathlib.olean file. Can it run in interpreted mode?

[Eric Wieser]

One interpretation of "run lean" is "transpile to C, and build a binary"; but this only helps you run lean programs, not lean itself

[Eric Wieser]

Mr Proof said:

I had a plan of bundling Lean/Mathlib in with a type of CAS I was making. But at 3-5GB that's not really an option.

If your CAS doesn't need all of mathlib, then you can omit many of the Olean files by using import Mathlib.JustTheBitYouNeed

[Utensil Song]

You might also want to check out https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/reverse.20FFI.3A.20building.20a.20.22fat.22.20static.20library.3F