remove unused library in compiled file

Stream: general

[Locria Cyber]

Someone mentioned that

import Lean.Data.Json.Parser

def main := IO.println "Hello, world!"

This code compiles to 135M.

Compiled with lake build.

Is there anything i can do to make the executable file size smaller? This should be a task done by the compiler, I think.

[Henrik Böving]

The easiest thing for you would be to call strip on the binary. In general importing anything from Lean calls into action a lot of code that we can't easily get rid of but we could still do a better job yes.

[Anthony Wang]

There's an open issue about this bug: https://github.com/leanprover/lean4/issues/5274