ffi without alloy

Stream: lean4

[Joachim Breitner]

I have a working ffi setup using @Mac Malone’s alloy library, including linking against a system-provided library (libseccomp). But my C code is very trivial, so I’d like to use the FFI directly, but I can’t get it to work.

Like before, I use this fragment to make lake pick up the system-provided libseccomp.so:

extern_lib libseccomp pkg := do
   let name := nameToStaticLib "seccomp"
   let dst := pkg.nativeLibDir / name
   let libdir ← captureProc { cmd := "pkg-config", args := #[ "--variable=libdir", "libseccomp"] }
   logStep s!"Copying {name} from {libdir}"
   proc { cmd := "mkdir", args := #[ "-p", pkg.nativeLibDir.toString] }
   proc { cmd := "cp", args := #[ "-f", s!"{libdir}/{name}", dst.toString] }
   pure $ BuildJob.pure dst

Further Cargo-culting the example from the lean repo, I now have this:

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

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

lean_lib Seccomp where
   roots := #[`Seccomp]
   precompileModules := true

It builds a .so file from my shim (loogle_seccomp.so), and passes it to lean when building the Seccomp lean module, but it has missing symbols:

~/projekte/programming/loogle $ lake build
[0/4] Copying libseccomp.a from /nix/store/3hdrczj786rpbprb7h92g75j5cx9j48l-libseccomp-static-x86_64-unknown-linux-musl-2.5.4-lib/lib
[2/16] Building Seccomp
error: > LEAN_PATH=./lake-packages/proofwidgets/build/lib:./build/lib:./lake-packages/Cli/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/etc/sane-libs:./build/lib:./build/lib:./build/lib /home/jojo/.elan/toolchains/leanprover--lean4---nightly-2023-08-15/bin/lean ./././Seccomp.lean -R ././. -o ./build/lib/Seccomp.olean -i ./build/lib/Seccomp.ilean -c ./build/ir/Seccomp.c --load-dynlib=./build/lib/libloogle_seccomp.so --load-dynlib=./build/lib/libseccomp.so
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./build/lib/libloogle_seccomp.so: undefined symbol: seccomp_init
error: external command `/home/jojo/.elan/toolchains/leanprover--lean4---nightly-2023-08-15/bin/lean` exited with code 134

This command line actually works when I reverse the order of the last two flags, but probably the real solution is to somehow pass -lseccomp when ./build/lib/libloogle_seccomp.so is built. Can I achieve this somehow?

(Full code at <https://github.com/nomeata/loogle/tree/no-alloy>)

[Henrik Böving]

@Joachim Breitner you can set the option moreLinkArgs and moreLeancArgs on your lean_lib/lean_exe

[Joachim Breitner]

I’ll try. Did Alloy somehow take care of that for me implicitly?

[Joachim Breitner]

Hmm, I’m still a bit lost. Wouldn’t I have to set the flag somewhere for the extern_lib libloogle_seccomp target, as that is the C shim that uses the system library?

[Joachim Breitner]

Ah, setting it for the package seems to help… And it seems I don’t even need extern_lib libseccomp then

[Joachim Breitner]

How does lake know which extern_lib’s are needed in which lean_lib or lean_exe's? Does it assume that within one project, all extern_libs are needed all the other targets?

[Mac Malone]

Joachim Breitner said:

How does lake know which extern_lib’s are needed in which lean_lib or lean_exe's? Does it assume that within one project, all extern_libs are needed all the other targets?

Currently, Yes.