Linking a C library

Stream: lean4

[Sofia Rodrigues]

I'm trying to link a C library called libuv in my application using this code to build:

@[default_target]
lean_exe «melp» {
  root := `Main,
  moreLinkArgs := #["-luv"]
}

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

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

And i'm getting a bunch of these errors:

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_rwlock_trywrlock@GLIBC_2.34
>>> referenced by /usr/lib64/gcc/x86_64-pc-linux-gnu/13.1.1/../../../../lib64/libuv.so

I tried to add -lpthread but it does not works :\ how should I proceed?

[Sebastian Ullrich]

It seems the library requires a newer version of glibc than Lean targets. When you interface with system libs, it is safer to compile under LEAN_CC=cc in order to use the system C compiler.

[Joe Hendrix]

@Felipe GS Did you resolve your issue? I am starting bindings to libuv and was curious about what you are working on.

[Utensil Song]

Joe Hendrix said:

Felipe GS Did you resolve your issue? I am starting bindings to libuv and was curious about what you are working on.

According to this post, melp settled on lean4-socket, so libuv still has no Lean 4 binding yet I guess. Looking forward to your work!