Reducing binary size

Stream: lean4

[Number Eighteen]

My hello_world binary with no imports compiles at around 5MB in Linux; is there a way to reduce the size of the binary by some build flags or other method?

[Henrik Böving]

First thing you can do is strip it, that can usually cut some slack out. Apart from that there is not too much. The runtime is statically linked into the binary as to avoid a dependency on shared objects and that is causing most of the size you are seeing.

[Number Eighteen]

Thank you.