exporting a dynamic library

Stream: new members

[JJ]

I'm trying to get Lean to output a dynamic library .so file suitable for linking against. I've managed to get lake to output .so files, with lake build Main:dynlib (for a file named Main) but these all include a bunch of undefined symbols for standard library functions, which is causing issues when I try to open the .so in a different languages's FFI.

After learning a little bit about linking (I knew nothing beginning of today) and inspecting the .so with nm -D the other language's FFI seems correct in yelling at me as a bunch of standard library functions are undefind... but I can't seem to figure out, how can I get a standalone dynamic library? The structure of my project is, I have one Main.lean file containing several functions. My lakefile looks like the following:

name = "Main"
version = "0.1.0"

[[lean_lib]]
name = "Main"

How might I build a self-contained dynamic library with the standard library included?

[Derek Rhodes]

Hi, I have not done any FFI programming with Lean, however I did get this example to build an .so on linux.

https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi

check in main.c, to see the goal, which was to use an exported lean function to compute the length of a string:

  //... preamble
  // actual program

  lean_object * s = lean_mk_string("hello!");
  uint64_t l = my_length(s);
  printf("output: %ld\n", l);

However, I had to remove mentions of -lleanshared_1 in the Makefile to get it to build. (also, I have no idea how much of the stdlib is available from C)

[Sebastian Ullrich]

How might I build a self-contained dynamic library with the standard library included?

This kind of "fat" dynamic library is not supported yet (as it does not compose if you mix dynlibs from multiple Lean libraries). It would be great if you could open a small RFC with your use case. Pending that, copying over the dynlibs from the toolchain directory should work.

[JJ]

Thanks! I've found the symbols I was missing in libleanshared.so there.

[JJ]

I'm doing something very stupid (calling Lean from Racket for no real reason)... I think having the symbols in a separate library will probably work for my use case, though I haven't gotten it to work yet. Not supporting this outright makes sense from how you're describing it.

[JJ]

Update: I have gotten it working. Many thanks!

[JJ]

(also @Sebastian Ullrich are you at POPL?)

[Sebastian Ullrich]

(I am, always happy to talk about anything Lean-related and even other things!)

[Sparsa Roychowdhury]

Hi, Sorry for opening this 1 year old thread. I am trying something with dynamic library. I created a simple lean module from which I am trying to create a dynamic library so that I can load it from a Python program. I was able to generate the *.so file, but there are some missing definitions. I have linked libLean.a, libStd.a, libInit.a during the compilation. But, when I try to load the library from python it complains that "lean_dec_ref_cold" is not defined. I tried to look under all the libraries under $LEAN_LIB/lib/lean folder using "nm" command but still couldn't find the library where "lean_def_rec_cold" is defined. If I can get some help that would be amazing.
Thank you.

[Sparsa Roychowdhury]

Sparsa Roychowdhury said:

Hi, Sorry for opening this 1 year old thread. I am trying something with dynamic library. I created a simple lean module from which I am trying to create a dynamic library so that I can load it from a Python program. I was able to generate the *.so file, but there are some missing definitions. I have linked libLean.a, libStd.a, libInit.a during the compilation. But, when I try to load the library from python it complains that "lean_dec_ref_cold" is not defined. I tried to look under all the libraries under $LEAN_LIB/lib/lean folder using "nm" command but still couldn't find the library where "lean_def_rec_cold" is defined. If I can get some help that would be amazing.
Thank you.

I have found "lean_dec_ref_cold" in libleanrt.a library. But still not able to complete the process. Will update.

[Sparsa Roychowdhury]

all were declared under libleanshared.so.
able to figure out.