Building static executables

Stream: new members

[Aditya Siram]

Hi! I'm trying to build Lean from source on Linux with CMake and the resulting executables have a dependency on libleanshared.so, is there a CMake flag to that links statically?

[Sebastian Ullrich]

Hi! I don't think so. The reason for the shared library is that we produce multiple binaries that share a good amount of code

[Sebastian Ullrich]

It might or might not be sufficient to replace -lleanshared in https://github.com/leanprover/lean4/blob/63d2bdd4908b4df7db381537af754a7319e334e4/src/stdlib.make.in#L57 with -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group

[Aditya Siram]

Thanks I'll try that.