lake : creating libraries that links with a shared object.

Stream: lean4

[PolyB]

Hi !

I am trying to make a lean4 library that links against a linux shared object but I can't find how to make everything work.

I'm based on the ffi example in lake repository https://github.com/leanprover/lake/tree/master/examples/ffi

Right now, I'm having 2 issues:

• I don't know how to say to lake that applications that requires this package needs to be linked with my library.
  I tried to add moreLinkArgs := #["-lz"] in ffi lake package or lean_lib definition, but it doesn't propagate the args to the application that require the library.
  It works if I add a moreLinkArgs := #["-lz"] in either the application package or in lean_exe, but I feel like it's not application role to know what the library needs.

• The shared objects built in order to be --load-dynlib are not linked to the shared library, so the lean compiler doesn't load zlib when loading the shared object.
  By looking at lake source code, Looks like there is no way to define custom linker arguments when building the shared object https://github.com/leanprover/lake/blob/master/Lake/Build/Targets.lean#L84-L92

[Mac]

Sadly, shared external libraries for dependencies are not currently supported by Lake. It is on my TODOs list, though. Two reasons I had not prioritized this thus far is that:

1. In general, linking against a system library is not portable (users of your library will have to, out of band of Lean/Lake, acquire the library). For instance, note that Windows does not come with zlib.
2. Linking a shared library makes it impossible for dependent packages to then build a self-contained native executable / shared library (i.e., they will need to always ship the required shared library with it)

Number (2) is particularly important for your example because it highlights that even if the ability existed to tell Lake that dependents upon your library should link zlib, the end-user would still need to know that and figure out how to acquire and/or distribute zlib with their application. So, the principle you elucidated that "it's not the application's role to know what the library needs" would still be violated.

Does that make sense / seem reasonable?

To solve your immediate problem in the short term, I would suggest either using extern_lib to build a static copy of zlib or stick with adding -lz to the moreLinkArgs of your library / application.

[PolyB]

Thank you for your response !

Yes that make sense, thank you for the explanation !

Even if adding -lz fixes my first bullet point, the second one still won't work because my lib won't be loaded at runtime.

As you suggested I'm working around the issue by using a static build of the library. By doing that I ran into few new issues:
For reference this is my current state : https://github.com/PolyB/LeanPythonRaw/blob/try_improve_lake/lakefile.lean

• What is the correct "lean4" way to fetch and build external dependencies ?
  Currently I'm fetching a tarball with wget and building it in __package.buildDir, As there is no helper to do that in Lake I feel like this is hacky.

• This creates an other issue as the fetched tarball has 2 Targets : the static library, and the directory containing the C headers. This makes fetching the archive a dependency to two things : the extern_lib producing the static library, and the extern_lib that requires the C headers to build my ffi code. How do I make so that the archive is only fetched only once ?

• The --load-dynlib is still not working , in the console, lake prints :
  LEAN_PATH=[...] LD_LIBRARY_PATH=[...] [...]/lean ./lean/./Python/Raw/Ffi.lean -R ./lean/. -o ./build/lib/Python/Raw/Ffi.olean -i ./build/lib/Python/Raw/Ffi.ilean -c ./build/ir/Python/Raw/Ffi.c --load-dynlib=libpythonffi.so --load-dynlib=libpython3.10.so

  But as libpythonffi.so references symbols defined in libpython3.10.so, it crashes when loading libpythonffi.so.

  If I manually swap the 2 --load-dynlib by doing
  [...] --load-dynlib=libpythonffi.so --load-dynlib=libpython3.10.so
  instead of
  [...] --load-dynlib=libpython3.10.so --load-dynlib=libpythonffi.so
  it works, but I'm not sure on how to explain Lake that he needs to do that.

• One issue I ran across is that I can't define a directory as a FileTarget. As a hack I referenced a file in the directory and used .getParent on the file path, how can I do that properly ?

[Mac]

Wow! Thanks for the detailed walkthrough of your use case. This will really help me in a having a complex example to support as I improve Lake. Unfortunately, almost everything you hit is an issue with the current target API. Good news this that these things are my next big goal. Bad news is they are not done yet. However, for stop-gap solutions. here is some advice:

What is the correct "lean4" way to fetch and build external dependencies ?

Currently, exactly the way you are doing so.

This creates an other issue as the fetched tarball has 2 Targets :

Sadly, there is not yet a way to fetch one target from another in extern_lib (though the feature does currently exist within Lake, it is just not currently exposed through the target API). One way to solve this for now is to just build a single static library composed of both the third-party code and your ffi. See this StackOverflow post on how to combine static libraries.

The --load-dynlib is still not working , in the console, lake prints

The above single library solution should solve this.

One issue I ran across is that I can't define a directory as a FileTarget.

This is leanprover/lake#90. Your hack is reasonable enough for now.

[Locria Cyber]

still can't link with libX11

[Mac Malone]

@Locria Cyber what seems to be the issue?

[Locria Cyber]

figured it out already

have to pass cflags to clang