Shared libraries

Stream: lean4

[Tomas Skrivan]

How can I generate Lean's shared libraries? Lean's installation contains only static ones libInit.a libLean.a libleancpp.a libStd.a. Peeking into CMakeLists they are not generated because of some cross-compiling issues. I'm on linux and want to develop only for linux right now, so that should not be an issue for me. I have tried to un-comment that block, but I'm getting bunch of errors about recompiling with -fPIC.

Alternatively, how can I recompile those static libraries with fPIC such that I can use them when creating a plugin for some application.

[Sebastian Ullrich]

The nightlies come with libleanshared.so

[Sebastian Ullrich]

and all code compiled with fPIC

[Tomas Skrivan]

Thanks! I have missed that, I was using only stable.

[Tomas Skrivan]

Ok, managed to get it working! Successfully created a shared library with lean, loaded it and executed from external application. Took me a while. One thing I was confused about, why is void lean_initialize_runtime_module() not declared in lean.h? It seems to be defined in lean library and it has to be called before anything.