building shared library depending on another project

Stream: lean4

[Tomas Skrivan]

edit: For anyone from the future, working example project can be found at https://github.com/lecopivo/ReverseFFIwithMathlib

---

How do I build shared library that is depending on another project like std or mathlib? The issue I'm having is that the symbols from dependencies are not included in the created shared library.

Here is an example:

lakefile.lean

import Lake
open Lake DSL

package «SharedLibTest» where

lean_lib «SharedLibTest» where

@[default_target]
lean_lib «sharedlibtest» where
  roots := #[`SharedLibTest]
  defaultFacets := #[`shared]

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

Main file SharedLibTest.lean

import Std.Data.RBMap.Basic

def minNumber (x y z : USize) : USize :=
  let map : Std.RBSet USize compare := Std.RBSet.ofList [x,y,z] _
  map.toList.head!

running

lake build && nm .lake/build/lib/libsharedlibtest.so

produces

output

                 w __cxa_finalize
                 w __deregister_frame_info
0000000000001e40 t __do_fini
00000000000077b0 b __do_fini.__finalized
0000000000001df0 t __do_init
0000000000007768 b __do_init.__initialized
0000000000007770 b __do_init.__object
00000000000076d8 d __dso_handle
00000000000064f0 d _DYNAMIC
0000000000000b08 r __EH_FRAME_LIST__
0000000000000b08 r __EH_FRAME_LIST_END__
00000000000064e8 d __fini
00000000000053d4 t _fini
00000000000077c0 b _G_initialized
00000000000076e0 d _GLOBAL_OFFSET_TABLE_
                 w __gmon_start__
00000000000064e0 d __init
00000000000053b8 t _init
                 U initialize_Init
00000000000052d0 T initialize_SharedLibTest
                 U initialize_Std_Data_RBMap_Basic
                 U lean_alloc_small
0000000000004e10 t lean_ctor_release
0000000000001fd0 t lean_dec
                 U lean_dec_ref_cold
                 U lean_free_object
0000000000001ff0 t lean_inc
                 U lean_inc_ref_cold
                 U lean_mark_persistent
                 U l_instInhabitedUSize
0000000000001eb0 T l_List_foldl___at_minNumber___spec__1
0000000000004ea0 T l_List_foldl___at_minNumber___spec__1___at_minNumber___spec__2
                 U l_List_head_x21___rarg
0000000000005010 T l_minNumber
0000000000005230 T l_minNumber___boxed
00000000000077b8 B l_minNumber___boxed__const__1
0000000000002010 T l_Std_RBNode_ins___at_minNumber___spec__4
0000000000005170 T l_Std_RBNode_ins___at_minNumber___spec__4___boxed
0000000000004e50 T l_Std_RBNode_insert___at_minNumber___spec__3
00000000000051b0 T l_Std_RBNode_insert___at_minNumber___spec__3___boxed
                 U l_Std_RBNode_insert___rarg
                 U l_Std_RBNode_setBlack___rarg
                 U l_Std_RBNode_toList___rarg
                 w __register_frame_info

See the last lines

                 U l_Std_RBNode_insert___rarg
                 U l_Std_RBNode_setBlack___rarg
                 U l_Std_RBNode_toList___rarg

indicates that functions Std.RBNode.insert, Std.RBNode.setBlack and Std.RBNode.toList are not included in the shared library.

How do I make sure that all the functions from dependencies are included in the generated library? (I'm expecting this question is just for @Mac Malone)

[Mac Malone]

@Tomas Skrivan The shared libraries Lake builds for a Lean library only include the symbols of the library itself. Unfortunately, there is no way to build a "fat" shared library with Lake yet. You instead must also link the shared libraries of the dependencies as well as the library itself to whatever itt consuming this shared library.

[Tomas Skrivan]

So in my project I should do lake build Std:shared Mathlib:shared ..., then hunt those libraries down somewhere in .lake/... and link it against the main shared library I want to use?

[Tomas Skrivan]

This is of course unfortunate as I'm forced to build everything, not only the stuff I'm actually using.

[Eric Wieser]

I think you can build just +YourModule:dynlib and it will build all the intermediate libraries?

[Tomas Skrivan]

Eric Wieser said:

I think you can build just +YourModule:dynlib and it will build all the intermediate libraries?

I do not understand, do you mean lake build +sharedlibtest:dynlib? That does not work.

[Eric Wieser]

I assume you had it as SharedLibTest not lowercase?

[Tomas Skrivan]

Ohh lake build +SharedLibTest:dynlib is doing something, let me investigate.

[Tomas Skrivan]

Running lake build +SharedLibTest:dynlib && nm .lake/build/lib/libSharedLibTest-1.so produces

output

                 w __cxa_finalize
                 w __deregister_frame_info
00000000000021b0 t __do_fini
0000000000007d70 b __do_fini.__finalized
0000000000002160 t __do_init
0000000000007d28 b __do_init.__initialized
0000000000007d30 b __do_init.__object
0000000000007c98 d __dso_handle
00000000000068c0 d _DYNAMIC
0000000000000e70 r __EH_FRAME_LIST__
0000000000000e70 r __EH_FRAME_LIST_END__
00000000000068b8 d __fini
00000000000057a4 t _fini
0000000000007d80 b _G_initialized
0000000000007ca0 d _GLOBAL_OFFSET_TABLE_
                 w __gmon_start__
00000000000068b0 d __init
0000000000005788 t _init
                 U initialize_Init
00000000000056a0 T initialize_SharedLibTest
                 U initialize_Std_Data_RBMap_Basic
                 U lean_alloc_small
0000000000005180 t lean_ctor_release
0000000000002340 t lean_dec
                 U lean_dec_ref_cold
                 U lean_free_object
0000000000002360 t lean_inc
                 U lean_inc_ref_cold
                 U lean_mark_persistent
                 U l_instInhabitedUSize
0000000000002220 T l_List_foldl___at_minNumber___spec__1
0000000000005210 T l_List_foldl___at_minNumber___spec__1___at_minNumber___spec__2
                 U l_List_head_x21___rarg
00000000000055e0 T l_minNumber___boxed
0000000000007d78 B l_minNumber___boxed__const__1
0000000000002380 T l_Std_RBNode_ins___at_minNumber___spec__4
0000000000005520 T l_Std_RBNode_ins___at_minNumber___spec__4___boxed
00000000000051c0 T l_Std_RBNode_insert___at_minNumber___spec__3
0000000000005560 T l_Std_RBNode_insert___at_minNumber___spec__3___boxed
                 U l_Std_RBNode_insert___rarg
                 U l_Std_RBNode_setBlack___rarg
                 U l_Std_RBNode_toList___rarg
0000000000005380 T min_number
                 w __register_frame_info

In particular, the Std.RBNode... functions are not included

                 U l_Std_RBNode_insert___rarg
                 U l_Std_RBNode_setBlack___rarg
                 U l_Std_RBNode_toList___rarg

[Tomas Skrivan]

Ok I got it working when working with std. Now I'm struggling to get it working with mathlib. When compiling test c++ file using generated shared library I'm getting this error:

/usr/bin/ld: ~/ReverseFFIWithMathlib/.lake/packages/importGraph/.lake/build/lib//libImportGraph.so: undefined reference to `initialize_Lake_Load_Manifest'
/usr/bin/ld: ~/ReverseFFIWithMathlib/.lake/packages/importGraph/.lake/build/lib//libImportGraph.so: undefined reference to `l_Lake_Manifest_load_x3f'

where do I find initialize_Lake_Load_Manifest and l_Lake_Manifest_load_x3f?

[Eric Wieser]

Yes, you still have to link all the transitive .so files

[Tomas Skrivan]

And I created example repo for any unfortunate soul doing this in the future
https://github.com/lecopivo/ReverseFFIwithMathlib

[Tomas Skrivan]

Oh those functions are in libLake.a

[Tomas Skrivan]

And adding -lLake flag in lakefile fixes this!

[Tomas Skrivan]

It would be nice to have shared version of libLake.a as my shared library has 23kB but because I have to link statically against libLake.a it balloons to 1.3MB.