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!

[Sofia Rodrigues]

Joe Hendrix said:

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

It's an old message so I guess the issue is solved by now lol

[David Richter]

Hi, I am trying to wrap sqlite https://github.com/drcicero/sqlite.lean

However, when building i get a lot of errors of style undefined reference due to --no-allow-shlib-undefined

$ lake clean; lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
error: > /home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc -o ./.lake/build/bin/test ./.lake/build/ir/Test.c.o ./.lake/build/ir/Sqlite.c.o ./.lake/build/lib/libleansqlite3.a -lsqlite3
error: stderr:
ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_join@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlerror@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_destroy@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: exp@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_create@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: log@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: stat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_init@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: fstat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlopen@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: fcntl64@GLIBC_2.28
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: lstat64@GLIBC_2.33
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutexattr_settype@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlsym@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pthread_mutex_trylock@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: pow@GLIBC_2.29
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so

ld.lld: error: undefined reference due to --no-allow-shlib-undefined: dlclose@GLIBC_2.34
>>> referenced by /lib/x86_64-linux-gnu/libsqlite3.so
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc` exited with code 1

I found another library https://github.com/arthurpaulino/LeanMySQL/blob/master/lakefile.lean which simply adds "-L/usr/lib/x86_64-linux-gnu/" to the moreLinkArgs. If I do that it works for me and I can run some simple queries:

$ lake clean; lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
3.37.2
> SELECT SQLITE_VERSION()
  [(SQLITE_VERSION(), 3)]
  [3.37.2]
  DONE 101
> DROP TABLE IF EXISTS Cars
  []
  DONE 101
> CREATE TABLE Cars(Id INT, Name TEXT, Price INT)
  []
  DONE 101
> INSERT INTO Cars VALUES (1, 'Audi', 52642), (2, 'Mercedes', 57127), (3, 'Skoda', 9000)
  []
  DONE 101
> INSERT INTO Cars VALUES (4, 'Volvo', 29000), (5, 'Bentley', 350000), (6, 'Citroen', 21000)
  []
  DONE 101
> INSERT INTO Cars VALUES (7, 'Hummer', 41400), (8, 'Volkswagen', 21600)
  []
  DONE 101
> SELECT * FROM sqlite_master
  [(type, 3), (name, 3), (tbl_name, 3), (rootpage, 1), (sql, 3)]
  [table, Cars, Cars, 2, CREATE TABLE Cars(Id INT, Name TEXT, Price INT)]
  DONE 101
> SELECT * FROM Cars
  [(Id, 1), (Name, 3), (Price, 1)]
  [1, Audi, 52642]
  [2, Mercedes, 57127]
  [3, Skoda, 9000]
  [4, Volvo, 29000]
  [5, Bentley, 350000]
  [6, Citroen, 21000]
  [7, Hummer, 41400]
  [8, Volkswagen, 21600]
  DONE 101
> SELECT * FROM Cars WHERE Price > 29000
  [(Id, 1), (Name, 3), (Price, 1)]
  [1, Audi, 52642]
  [2, Mercedes, 57127]
  [5, Bentley, 350000]
  [7, Hummer, 41400]
  DONE 101
> SELECT Name FROM Cars WHERE Price > 29000
  [(Name, 3)]
  [Audi]
  [Mercedes]
  [Bentley]
  [Hummer]
  DONE 101

However, I suppose that would make the library platform-dependent, which is unsatisfying? I'm wondering whether there is a better way.

A similar error was posted twice in the past, and @Sebastian Ullrich responded with:

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.

However, that doesn't work for me either:

$ lake clean; LEAN_CC=cc lake exe test
info: [0/4] Compiling leansqlite3.c
info: [0/4] Creating libleansqlite3.a
info: [0/4] Linking libleansqlite3.so
info: [0/4] Building Sqlite
info: [1/4] Compiling Sqlite
info: [1/4] Building Test
info: stdout:
./././Test.lean:14:46: warning: unused variable `nmtp` [linter.unusedVariables]
info: [3/4] Compiling Test
info: [4/4] Linking test
error: > /home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc -o ./.lake/build/bin/test ./.lake/build/ir/Test.c.o ./.lake/build/ir/Sqlite.c.o ./.lake/build/lib/libleansqlite3.a -L/usr/lib/x86_64-linux-gnu/ -lsqlite3
error: stderr:
/usr/bin/ld: cannot find -lc++: No such file or directory
/usr/bin/ld: cannot find -lc++abi: No such file or directory
collect2: error: ld returned 1 exit status
error: external command `/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/leanc` exited with code 1

Any ideas?