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!)