Issue with linking shared libraries

Stream: lean4

[Abdalrhman M Mohamed]

I am facing issues loading shared libraries with dependencies. Here is a MWE: I have a simple lakefile.lean that imports the standard library:

import Lake
open Lake DSL

package lib

@[default_target]
lean_lib Lib

require std from git "https://github.com/leanprover/std4" @ "main"

Lib.lean contains a simple import and definition

import Std.Data.Rat

def hello : Rat := 1/2

I have one more file, Test.lean, that imports import Lib.lean:

import Lib

#eval hello

I get the following error if I try to build a shared version of the target library Lib and load it before elaborating Test.lean:

$ lake build Lib:shared
Linking libLib.so
$ lake env lean --load-dynlib=libLib.so Test.lean
/home/user/.elan/toolchains/leanprover--lean4---nightly-2023-03-07/bin/lean: symbol lookup error: ./build/lib/libLib.so: undefined symbol: initialize_Std_Data_Rat

Interestingly, @Wojciech Nawrocki noticed that if I build the shared version of module Lib, it gets loaded correctly:

$ lake build +Lib:dynlib
Linking Lib
$ lake env lean --load-dynlib=libLib.so Test.lean
(1 : Rat)/2

@Mac, do you have an idea of what's going on? Is this expected behavior?

[Sebastian Ullrich]

The module shared lib might not be declaring its dependencies correctly (what does ldd say?). Lake passes the entire closure of modules via --load-dynlib, which is necessary on Windows but ideally should not be on Unix

[Wojciech Nawrocki]

@Sebastian Ullrich when I tried this on a non-MWE, ldd libLib.so was not importing any Lean module whatsoever.

[Sebastian Ullrich]

Yeah, I thought so. It's not necessary, but it would be nicer if Lake passed the dependencies to the linker

[Mac Malone]

@Sebastian Ullrich Lib in this case is the shared library for the whole Lean library of the package. It doesn't depend on any specific other libraries (e.g., it could work with either individual module libraries or shared libraries of other modules or even static libraries).

[Abdalrhman M Mohamed]

Sebastian Ullrich said:

The module shared lib might not be declaring its dependencies correctly (what does ldd say?). Lake passes the entire closure of modules via --load-dynlib, which is necessary on Windows but ideally should not be on Unix

Here is what I get from ldd when I run lake build Lib:shared:

$ lake env ldd build/lib/libLib.so
        linux-vdso.so.1 (0x00007fff6abf4000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fd55516d000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fd555168000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fd555163000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fd554e00000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fd55526c000)

[Abdalrhman M Mohamed]

Oh! I see. So this is expected behavior and we should just load libStd.so?

[Sebastian Ullrich]

@Mac Well, there are two libLibs here. So what's the difference?

[Mac Malone]

@Sebastian Ullrich Yeah, that's a naming confusion I forgot to fix. The first one Lib:shared is the shared library of lean_lib Lib (e.g., a normal shared library for library distribution purposes). The second one +Lib:dynlib is the shared library of the module Lib for use with precompiled modules.

[Mac Malone]

The second one should have some special prefix or suffix to differentiate it. I haven't come up with a good one yet. That is, one that would not cause confusion if a library or module happens to be named in a particular way. For instance, if it was suffixed with M (for module), it might clash with modules defining a monad (which also use the suffix M).

[Sebastian Ullrich]

I see, I assumed it was the other way around. But for a "proper" shared library in contrast to the implementation detail of precompiled dynlibs it's even more wrong not to declare its dependencies. Indeed it should probably be linked with -no-undefined.

[Sebastian Ullrich]

Precisely because precompiled libraries are an implementation detail, I would simply drop the lib prefix, then there is no confusion (edit: though the prefix might be necessary to use with -l on macOS...)

[Mac Malone]

Sebastian Ullrich said:

(edit: though the prefix might be necessary to use with -l on macOS...)

Yeah, MacOS requires it (learned that the hard way).

[Mac Malone]

Sebastian Ullrich said:

t's even more wrong not to declare its dependencies.

How so? It still works without them and doesn't cause the numerous problems dependencies cause across OSes (since they all have different lookup procedures). Furthermore, it gives more flexibility on how the dependencies symbols are stored (i.e., you can link them all into one library per package or per module or per root).

[Wojciech Nawrocki]

How so? It still works without them

I am confused by this point. Without knowing the dependencies' initializers we can't run the initializers for Lib, which is what Abdal is experiencing.

[Mac Malone]

@Wojciech Nawrocki what I meant by works is that you can get it to work by loading the dependencies as well e.g. do --load-dynlib=libStd.so --load-dynlib=libLib.so etc.

[Sebastian Ullrich]

But using them with --load-dynlib is not what the target dynlibs were made for, or how Lake itself uses them, no? I assume :shared is intended primarily for uses outside of Lean, in which case it should try to generate shared libraries that follow the conventions of the platform, and in particular should not contain undefined symbols on either Linux or macOS.