How to use std::string (C++ standard library) in Lean 4 FFI?

Stream: lean4

[T L]

I am trying to write a string processing function in c++ via lean 4 FFI. But I got link errors when using lake. I asked a question in PA.SE, and was referred to here. Below are the main parts of my question, and any help is appreciated.

I wanted to use the C++ std::string and its supporting functions in the C++ standard library (C++1x or C++20) in it.

I re-used the ffi example in the Lean documentation, and added a (empty) reverseString/c_reverse_string function.

lib/FFI/Add.lean:

@[extern "my_add"]
opaque myAdd : UInt32 → UInt32 → UInt32

@[extern "c_reverse_string"]
opaque reverseString (s : @& String) : IO String

lib/c/ffi.cpp:

#include <lean/lean.h>
#include <string>

extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
    return a + b;
}

extern "C" LEAN_EXPORT lean_obj_res c_reverse_string(lean_obj_arg s) {
    std::string ss = "hi";
    lean_obj_res result = lean_mk_string(ss.c_str());
    return lean_io_result_mk_ok(result);
}
//...

Note that I used std::string trivially in the c++ function. But the use of std::string here seems to cause link errors when building the project:

$ lake -d lib build -v
...
ℹ [17/18] Built Main:c.o (with exports)
trace: .> /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang -c -o lib/./.lake/build/ir/Main.c.o.export lib/./.lake/build/ir/Main.c -I /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/include -fstack-clash-protection -fwrapv -fPIC -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /home/.../.elan/toolchains/leanprover--lean4---v4.16.0 -nostdinc -isystem /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
✖ [18/18] Building test
trace: .> /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang -o lib/./.lake/build/bin/test lib/./.lake/build/ir/Main.c.o.export lib/./.lake/build/ir/FFI/Fn.c.o.export lib/./.lake/build/ir/FFI/Add.c.o.export lib/./.lake/build/ir/FFI.c.o.export lib/./.lake/build/lib/libleanffi.a --sysroot /home/.../.elan/toolchains/leanprover--lean4---v4.16.0 -L /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/lib -L /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc/libc_nonshared.a /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -L /home/.../.elan/toolchains/leanprover--lean4---v4.16.0/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread
info: stderr:
ld.lld: error: undefined symbol: std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::c_str() const
>>> referenced by ffi.cpp
>>>               ffi.o:(c_reverse_string) in archive lib/./.lake/build/lib/libleanffi.a

ld.lld: error: undefined symbol: std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::~basic_string()
>>> referenced by ffi.cpp
...

The lakefile.lean is:

import Lake
open System Lake DSL

package ffi where
  srcDir := "lean"

lean_lib FFI where
  precompileModules := true

@[default_target]
lean_exe test where
  root := `Main

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

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

My questions are:

How can I properly link C++ standard library (e.g. std::string) in a lakefile by fixing either example above?

Also, I am new to writing lakefile.lean, and I was wondering how to add a second .cpp source file (in addition to ffi.cpp), so that I can put my new functions in separate files.

(This is under Ubuntu 24.04, lean 4 v4.16.0)

[Daniil Kisel]

You can try specifying LEAN_CC env var to gcc/clang/g++/clang++ (when running lake build). You can also try adding -lstdc++ or -lc++ to moreLinkArgs instead. I think both worked for me in different projects.

See also:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20FFI.20to.20C.2B.2B.3A.20GiNaC

[T L]

Thanks! I tried using

lean_lib FFI where
  moreLinkArgs := #["-lstdc++", "-lc++"]

in lib/lean/lakefile.lean. Then I got a different error when running ./test.sh:

✖ [14/19] Building FFI
trace: .> LEAN_PATH=app/././../lib/.lake/build/lib:app/./.lake/build/lib LD_LIBRARY_PATH=app/././../lib/.lake/build/lib:app/././../lib/.lake/build/lib /home/.../.elan/toolchains/leanprover--lean4---v4.17.0/bin/lean app/././../lib/lean/./FFI.lean -R app/././../lib/lean/. -o app/././../lib/.lake/build/lib/FFI.olean -i app/././../lib/.lake/build/lib/FFI.ilean -c app/././../lib/.lake/build/ir/FFI.c --load-dynlib=app/././../lib/.lake/build/lib/libleanffi.so --load-dynlib=app/././../lib/.lake/build/lib/libFFI-Fn-1.so --load-dynlib=app/././../lib/.lake/build/lib/libFFI-Add-1.so --json
info: stderr:
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

It seems I can manually fix the output command by inserting --load-dynlib=${HOME}/.elan/toolchains/leanprover--lean4---v4.17.0/lib/libc++.so.1 before the first --load-dynlib=.... But I am not sure how to specific the location of libc++.so.1 in one of the two lakefile.lean. Any suggestion on how to let lean find the .so for the c++ standard library?

[Tomas Skrivan]

That should be simple as

  moreLinkArgs := #["-L/path/to/lib/dir","-lstdc++",...]

You just need to find the right directory on your system.

[T L]

no, that does not seem to address the problem.
I added moreLinkArgs := #["-L/home/.../.elan/toolchains/leanprover--lean4---v4.17.0/lib/libc++.so.1", "-lstdc++", "-lc++"] to both the lib/ and app/ lakefile.lean, and got the same error.

[T L]

For completeness, here is the slightly adapted ffi test from the lean v4.17.0 source:

ffi_lean4-reverse_string.tgz

The only addition is the reverseString function and its C++ backend using std::string. Any help on fixing the two lakefile.lean is appreciated.