using c++ std with ffi

Stream: lean4

[Tomas Skrivan]

I'm having issues using c++ standard library with ffi. I'm getting errors like undefined symbol: _ZSt4cout

I'm following the ffi example, but it does not work as expected.

The issue seems to be that linking is done with leanc, I tried to replace it with clang++ with appropriate flags and then it works.

Main.lean

@[extern "print_integer"]
opaque printInt (n : USize) : USize

def main : IO Unit :=
  IO.println s!"Hello, {printInt 42}!"

c/ffi.cpp

#include <iostream>

extern "C" size_t print_integer(size_t n){
    std::cout << "input integer is" << n << std::endl;
    return n;
}

lakefile.lean

import Lake
open Lake DSL

package «fFI» {}

@[default_target]
lean_exe «fFI» {
  root := `Main
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
  let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
  buildO "ffi.cpp" oFile srcJob flags "c++"

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  buildStaticLib (pkg.buildDir / name) #[ffiO]

[Sebastian Ullrich]

Yes, leanc is not a C++ compiler, it won't implicitly link in a C++ stdlib

[Tomas Skrivan]

How can I create a lean package that has external library written in C++?

[Mario Carneiro]

btw, cc: @Mac Malone on the unusual casing of package «fFI» {}. I'm guessing this project was created using lake new FFI

[Mac Malone]

@Mario Carneiro I believe that has since been fixed and it is due to using an old Lake version.

[Mac Malone]

Tomas Skrivan said:

How can I create a lean package that has external library written in C++?

You need to explicitly link libstdc++ to it (e.g., via moreLinkArgs := #["-lstdc++"]).

[Tomas Skrivan]

Mac Malone said:

Mario Carneiro I believe that has since been fixed and it is due to using an old Lake version.

I just realized that I created the project on an ancient version of lean

[Tomas Skrivan]

Where do I add moreLinkArgs := #["-lstdc++"] ?

Adding it in:

@[default_target]
lean_exe «fFI» {
  root := `Main
  moreLinkArgs := #["-lstdc++"]
}

does nothing and still leads to the same error

libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./build/libleanffi.so: undefined symbol: _ZSt4cout

Adding it to

package «fFI» {
  moreLinkArgs := #["-lstdc++"]
}

produces a new error

libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libc++.so.1: cannot open shared object file: No such file or directory

[James Gallicchio]

Not sure if this will help, but there's some documentation of what worked for me here https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/C.20FFI.20usage/near/307471978

[Mac Malone]

@Tomas Skrivan Do you have your WIP code in a repo somewhere? It is hard to debug linking errors without seeing the full configuration.

[Tomas Skrivan]

I will set it up in a moment.

[Tomas Skrivan]

Mac Malone said:

Tomas Skrivan Do you have your WIP code in a repo somewhere? It is hard to debug linking errors without seeing the full configuration.

Here is the repo: https://github.com/lecopivo/lean-cpp-ffi

[Tomas Skrivan]

Was the yesterday patch supposed to fix this issue? Because it still does not work :( It is still unclear how am I supposed to link c++ standard library.

[Siddharth Bhat]

@Tomas Skrivan I can haz backtrace? :)

[Tomas Skrivan]

Backtrace of what? How do I get it?

[Siddharth Bhat]

I was wondering what the precise error was when you ran lake build.

[Tomas Skrivan]

The output is

lean-cpp-ffi$ lake build
[0/2] Building Main
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=./build/lib:./build/lib /home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2023-08-24/bin/lean ./././Main.lean -R ././. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c --load-dynlib=./build/lib/libleanffi.so
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./build/lib/libleanffi.so: undefined symbol: _ZSt4cout
error: external command `/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2023-08-24/bin/lean` exited with code 134

[Mac Malone]

@Tomas Skrivan Did you add -lstdc++ (or -lc++ on MacOS) to moreLinkArgs?

[Tomas Skrivan]

Mac Malone said:

Tomas Skrivan Did you add -lstdc++ (or -lc++ on MacOS) to moreLinkArgs?

Yes I did

[Mac Malone]

Oh wait, I confused myself. No, that patch was not mean to fix this. That patch was mean to fix compilation of precompiled dynlibs (which is the step before this). This is an issue with using C++ symbols in interactive mode. To fix this you need to add --load-dynlib=stdc++ or --load-dynlib=path/to/stdc++.so to your moreLeanArgs.

[Mac Malone]

That is, your problem here is that lean itself does not have access to the symbol.

[Siddharth Bhat]

@Mac Malone can you explain what the intended behaviour of the lakefile below is supposed to be?

import Lake
open Lake DSL

package «FFI» {
}

@[default_target]
lean_exe «FFI» {
  root := `Main
  moreLinkArgs := #["-lc++abi", "-lstdc++"]
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
  let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
  buildO "ffi.cpp" oFile srcJob flags "c++"

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]

Am I right in assuming that this is supposed to build a libleanffi and link this into the executable FFI?

[Siddharth Bhat]

Mac Malone said:

Oh wait, I confused myself. No, that patch was not mean to fix this. That patch was mean to fix compilation of precompiled dynlibs. This is an issue with using C++ symbols in interactive mode. To fix this you need to add --load-dynlib=stdc++ or --load-dynlib=path/to/stdc++.so to your moreLeanArgs.

Yes, this is what I don't understand. Why does the above lakefile cause

[0/2] Building Main
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=./build/lib:./build/lib /home/t-sibhat/.elan/toolchains/leanprover--lean4---nightly-2023-08-23/bin/lean ./././Main.lean -R ././. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c --load-dynlib=./build/lib/libleanffi.so

to be executed, where _lean_ (the compiler) tries to load libleanffi.so dynamically?

[Siddharth Bhat]

I find the fact that lake adds the argument --load-dynlib=./build/lib/libleanffi.so confusing.

[Mac Malone]

@Siddharth Bhat Because Lake tries to load external libraries into Lean's environment so that you can use the symbols interactively.

[Mac Malone]

i.e., so that end-users calling #eval someDefThatUsesAnExternSomewhereWithin works and doesn't cause the server to crash.

[Siddharth Bhat]

@Mac Malone Shouldn't the principled solution be to add the used definitions from stdc++ and c++abi into the static library (libleanffi.a)?

[Mac Malone]

@Siddharth Bhat Yes, that would be most ideal. However, statically linking the C++ stdlib is not always easy.

[Tomas Skrivan]

Mac Malone said:

Oh wait, I confused myself. No, that patch was not mean to fix this. That patch was mean to fix compilation of precompiled dynlibs (which is the step before this). This is an issue with using C++ symbols in interactive mode. To fix this you need to add --load-dynlib=stdc++ or --load-dynlib=path/to/stdc++.so to your moreLeanArgs.

The --load-dynlib=stdc++ does not work. This is probably because
.elan/toolchains/leanprover--lean4---nightly-2023-08-23/lib/libc++.so.1 does not have the symbol _ZSt4cout

The only library on my machine that has _ZSt4cout is /usr/lib/gcc/x86_64-linux-gnu/9/libstdc++.a which is not a shared library.

[Mac Malone]

@Tomas Skrivan In that case, you can hopefully do what @Siddharth Bhat suggested and build a static library from your FFI and your static standard library.

[Tomas Skrivan]

What is the lake idiomatic way to organize such a thing?

[Tomas Skrivan]

Do I use the command extern_lib and inside do whatever needed to build my static library and output its name?

[Mac Malone]

@Tomas Skrivan Sadly, I have not tested Lake before with the C++ standard library. So, it might be best for me to try to get your example working and then come back with a solution. Alternatively, I could give you suggestions and debug failures, but that seems inefficient for both of us.

[Mac Malone]

@Tomas Skrivan For reference, what OS are you on?

[Tomas Skrivan]

I'm happy to wait and I would really appreciate you looking into this!

My ultimate goal is to create bindings for linear algebra library Eigen, I have this repo https://github.com/lecopivo/EigenLean but lake build sparse which builds example file for sparse matrices ends up with bunch of linker errors.

I'm on Linux, Ubuntu 20.04 to be precise, but I would really like the Eigen bindings to work on all platforms

[Mac Malone]

@Tomas Skrivan / @Siddharth Bhat I see two potential solutions here:

1. Extend the extern_lib syntax to support additional linking arguments when building the shared library from the static one. At this stage, with some additional options (e.g., -static -lstdc++) we could statically link the system libraries with the FFI code to make a self-contained shared library.
2. Locate the static library version of the system library and build a fat self-contained static library containing both the FFI code and static system library.

[Mac Malone]

(2) is a possible stop-gap solution until a Lake change. (1) has the advantage of avoiding system-dependent lookup of shared libraries in Lean but does require a breaking Lake change.

[Tomas Skrivan]

This is all black magic to me and I don't think I understand the trade off between (1) vs (2) properly, so what ever is easier for you :)

[Mac Malone]

@Tomas Skrivan Here is a dumb implementation of (2) that should work in the meantime (if you want to start debugging something):

import Lake
open Lake DSL

package «FFI»

@[default_target]
lean_exe «FFI» {
  root := `Main
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
  let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
  buildO "ffi.cpp" oFile srcJob flags "c++"

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  let stdlib ← inputFile <| "/path/to/lib/libstdc++.a"
  buildStaticLib (pkg.nativeLibDir / name) #[ffiO, stdlib]

[Siddharth Bhat]

➜  lean-cpp-ffi git:(master) ✗ cat lakefile.lean
import Lake
open Lake DSL

package «FFI» {
}

@[default_target]
lean_exe «FFI» {
  root := `Main
  -- moreLinkArgs := #["-L/usr/lib/gcc/x86_64-linux-gnu/11/", "-lstdc++"]
  -- moreLeanArgs := #["--load-dynlib=/usr/lib/gcc/x86_64-linux-gnu/11/libstdc++.so"]
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
  let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
  buildO "ffi.cpp" oFile srcJob flags "c++"

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  let stdlib ← inputFile <| "/usr/lib/gcc/x86_64-linux-gnu/11/libstdc++.a"
  buildStaticLib (pkg.nativeLibDir / name) #[ffiO, stdlib]

error:

➜  lean-cpp-ffi git:(master) ✗ lake build
[0/2] Creating libleanffi.a
[0/2] Linking libleanffi.so
error: > /home/t-sibhat/.elan/toolchains/leanprover--lean4---nightly-2023-08-23/bin/leanc -shared -o ./build/lib/libleanffi.so -Wl,--whole-archive ./build/lib/libleanffi.a -Wl,--no-whole-archive
error: stderr:
ld.lld: error: ./build/lib/libleanffi.a(libstdc++.a): not an ELF file
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/t-sibhat/.elan/toolchains/leanprover--lean4---nightly-2023-08-23/bin/leanc` exited with code 1

[Tomas Skrivan]

I'm getting the same error :/

[Siddharth Bhat]

@Mac Malone , I don't think it likes us having an archive containing an archive:

c++  -shared -o ./build/lib/libleanffi.so -Wl,--whole-archive ./build/lib/libleanffi.a -Wl,--no-whole-archive
/bin/ld: ./build/lib/libleanffi.a: member ./build/lib/libleanffi.a(libstdc++.a) in archive is not an object
collect2: error: ld returned 1 exit status

[Mac Malone]

@Tomas Skrivan / @Siddharth Bhat Sorry, yeah, my code is buggy. I realized only after I posted that that it was not doing what it was supposed to.

[Siddharth Bhat]

@Mac Malone Thanks for helping with this!

[Siddharth Bhat]

As per https://stackoverflow.com/questions/3821916/how-to-merge-two-ar-static-libraries-into-one, it seems like maybe we can teach lake to generate an MRI script on the fly and feed that into ar?

[Siddharth Bhat]

https://github.com/google/shaderc/issues/473#issuecomment-409754031

Jeez, so an MRI script does not like to have +s in it, so no linking to stdc++ :P

[Mac Malone]

@Tomas Skrivan / @Siddharth Bhat Here is an extremely hacky, but now working, Linux solution:

import Lake
open Lake DSL

package «FFI»

@[default_target]
lean_exe ffi {
  root := `Main
  moreLeanArgs := #["--load-dynlib=./build/lib/libstdcpp.so"]
  moreLinkArgs := #["-Lbuild/lib", "-lstdc++"]
}

target ffi.o pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / "ffi.o"
  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
  let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
  buildO "ffi.cpp" oFile srcJob flags "c++"

-- Path to system static lib
def staticStdlib := "/usr/lib/gcc/x86_64-linux-gnu/9/libstdc++.a"

extern_lib libstdcpp pkg := do
  let libFile := pkg.nativeLibDir / nameToStaticLib "stdcpp"
  let contents ← IO.FS.readBinFile staticStdlib
  createParentDirs libFile
  IO.FS.writeBinFile libFile contents
  inputFile libFile

extern_lib libleanffi pkg := do
  let name := nameToStaticLib "leanffi"
  let ffiO ← fetch <| pkg.target ``ffi.o
  buildStaticLib (pkg.nativeLibDir / name) #[ffiO]

[Mac Malone]

Attempting to construct a working example revealed a number of bugs and missing features in Lake, which I hope to fix soon.