Zulip Chat Archive

Stream: new members

Topic: Building static executables

Aditya Siram (Sep 24 2023 at 14:02):

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 (Sep 25 2023 at 07:23):

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 (Sep 25 2023 at 07:26):

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 (Sep 25 2023 at 14:29):

Thanks I'll try that.

Last updated: Dec 20 2023 at 11:08 UTC