Large binary sizes

Stream: lean4

[Aiken Cairncross]

I noticed the executables produced by lean are pretty big (~60MB) even for simple programs if I use any of std4. They contain lots of symbols/functions that I wouldn't have thought my programs are using. Is there any way to ask the compiler to produce smaller binaries?

[Henrik Böving]

You can reduce binary size substantially with strip but not to a really satisfying degree

[Henrik Böving]

One issue seems to be that we link in a large part of the lean compiler statically into std4? At least according to the output of nm on a binary with symbols. I think that should be avoidable

[Aiken Cairncross]

Yeah, strip brings it down from ~60MB to ~50MB, so significant but not drastic

[Scott Morrison]

My understanding is that the new module system (see the roadmap) may help with this.

The fundamental problem at the moment is that you use definitions or lemmas from Std that do not require import Lean (or importing any files from Lean), but they use tactics in their proofs which require an import Lean.X.Y.Z.

Today, we have no way of saying "this import is only going to be used while running a tactic at compile time", and hence have no way of knowing that those symbols don't need to be in the binary.

However this is definitely not my expertise, so @Sebastian Ullrich may be able to give a better answer!