search

tydeu / lean4-alloy

Write C shims from within Lean code.
Apache License 2.0
41 stars 11 forks source link

Link Library #8

Open drcicero opened 1 month ago

drcicero commented 1 month ago

Hi, alloy sounds nice!

I wonder, how does one link a library -- in particular, with gcc for example, I would add the flag -lsqlite3 to link the library and make its symbols available. How would I add a -l flag using alloy?

For example sudo apt install sqlite3-dev

import Alloy.C
open scoped Alloy.C

alloy c include <lean/lean.h> <sqlite3.h> <stdio.h>

alloy c extern
def sqliteversion : BaseIO UInt32 :=
  printf("%s\n", sqlite3_libversion())
  return lean_io_result_mk_ok(lean_box(0))
$ lake build
...
error: stderr:
ld.lld: error: undefined symbol: sqlite3_libversion
>>> referenced by Sqlite.alloy.c:6 (./.lake/build/ir/Sqlite.alloy.c:6)
>>>               ./.lake/build/ir/Sqlite.alloy.c.o:(_alloy_c_l_sqliteversion)
...
/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/lean: symbol lookup error: ./.lake/build/lib/libSqlite-1.so: undefined symbol: sqlite3_libversion
drcicero commented 1 month ago

I tried this

import Alloy.C
open scoped Alloy.C

#eval Alloy.C.modifyLocalServerConfig (·.addFlag "-lsqlite3")

alloy c include <lean/lean.h> <sqlite3.h> <stdio.h>

alloy c extern
def sqliteversion : BaseIO UInt32 :=
  printf("%s\n", sqlite3_libversion())
  return lean_io_result_mk_ok(lean_box(0))

But then lake gets stuck at [92/104] Building Sqlite and doesn't do anything at all anymore...

drcicero commented 1 month ago

I tried compiling without alloy and there the same error appears. I found this other library that also needs to link https://github.com/arthurpaulino/LeanMySQL/blob/master/lakefile.lean . They added moreLinkArgs to the package in lake-file, which seems necessary for the final linking (?) . I suppose now i can try, whether this will also help when using alloy.

package sqlite where
  moreLinkArgs := #["-L", "/usr/lib/x86_64-linux-gnu/", "-lsqlite3"]
tydeu commented 1 month ago

@drcicero Hello! To link to a shared library, specifying the linking flags via moreLinkArgs in the Lake configuration file is the currently recommended way. Alloy delegates the management of linking libraries and executables to Lake, and linking is not part of C/C++ language server (hence why using modifyLocalServerFlags did not succeed).

For link arguments, hard-coding the location of the library (e.g., -L/usr/lib/x86_64-linux-gnu) is not recommended. I t will prevent other packages which depend on yours from successfully linking to the library if it is located elsewhere (e.g., other OSes). Ideally, you should either:

  1. Use just -lsqlite3 and rely on the SQL lite library being installed on the user's system and part of the appropriate library path (e.g., LD_LIBRARY_PATH on Linux)
  2. Ship a copy of the relevant shared library with your Lean package.

Unfortunately, path (2) is complicated to accomplish at present, so it might not be wise to peruse. (However, if you are curious, LeanCopilot's lakefile.lean is one such sophisticated example of downloading libraries as part of the build.) If you take the more straightforward approach of (1), I would mentioning in the documentation of your package that the user is expected to have installed sqlite3 as a system library and have it available in the path.

drcicero commented 1 month ago

Thanks for the response! I got surprisingly far without alloy for now, but I'm intrigued by your comment on avoiding platform-specificity. Option two sounds like more work, I will ignore that for now. Option one was:

Use just -lsqlite3 and rely on the SQL lite library being installed on the user's system and part of the appropriate library path (e.g., LD_LIBRARY_PATH on Linux)

Do you mean LIBRARY_PATH (compile-time) or LD_LIBRARY_PATH (run-time)? I just tried removing the platform-specific -L option, replacing it by invoking LD_LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ lake exe test (or any combination of the two environment variables), but it just leads to different errors.

Do you have an example for how this could work?

EDIT: For example when using just moreLinkArgs := #["-lsqlite3"] then

$ lake clean sqlite; lake exe test
...
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
...

$ lake clean sqlite; LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ lake exe test
...
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
...

$ lake clean sqlite; LD_LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ lake exe test
...
error: > ~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar rcs ./.lake/build/lib/liblean4sqlite3.a ./.lake/build/c/lean4sqlite3.o
error: stderr:
~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar: symbol lookup error: ~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar: undefined symbol: _ZN4llvm3sys16getProcessTripleEv, version LLVM_15

$ lake clean sqlite; LD_LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/ lake exe test
...
error: > ~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar rcs ./.lake/build/lib/liblean4sqlite3.a ./.lake/build/c/lean4sqlite3.o
error: stderr:
~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar: symbol lookup error: ~/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar: undefined symbol: _ZN4llvm3sys16getProcessTripleEv, version LLVM_15
error: external command `/home/dr/.elan/toolchains/leanprover--lean4---4.6.0/bin/llvm-ar` exited with code 127

Maybe I'm doing something stupid :)

tydeu commented 1 month ago

@drcicero

For example when using just moreLinkArgs := #["-lsqlite3"]

There is mixed of news here. The good news is that is does seem to be successfully linking to a version sqlite3 installed in your systems library path. The neutral news is that it appears that version of sqlite3 needs pthread, and the potentially bad news, is that it possibly needs a different pthread than the one used by Lean? I am not confident I can provide you good advice on what exactly is needed here without trying this myself on a Linux system. I'll see if I can find some time to do so, but, unfortunately, I am not sure I promise I will. In general, though, you are on the write track, you just need to find the right set of arguments to get your executable to link without errors. You can also run with -v to see the full invocations of the compiler/linker used by Lake/Lean..

drcicero commented 1 month ago

Thanks for the input.

I'll see if I can find some time to do so, but, unfortunately, I am not sure I promise I will

Of course you don't need to do anything, I'm just randomly asking someone on the internet :)

In any case, I found this and this. Sebastian Ullrich wrote in both cases:

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.

But that didnt work for me. I detailed my endeavor here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Linking.20a.20C.20library/near/429369692 . Maybe someone has an idea.

You can also run with -v

-v to what?

tydeu commented 1 month ago

-v to what?

Sorry, lake build (e.g., lake build -v).