lakefile can't find a .so file it generated

Stream: lean4

[Chase Norman]

I have the following command in my lakefile.lean:

extern_lib libffi := do inputBinFile "generated-rust-lib/libffi.a"

This creates a .dylib file on MacOS and .so file on Linux. However, on Linux, the .so file subsequently cannot be found:

error loading library, libffi.so: cannot open shared object file: No such file or directory

I have tried moving the .so file out of the generated-rust-lib directory. Any ideas?

[Arthur Paulino]

Why is it generating a .so file? Do you have precompileModules := true?

[Chase Norman]

Yes

[Chase Norman]

As far as I can tell this is necessary for executing the code via FFI in VSCode

[Arthur Paulino]

I'd try moving generated-rust-lib/libffi.a to .lake/build/lib/libffi.a and setting the extern_lib to point to that path instead, just to see if Lake does a better job at finding the .so file

[Arthur Paulino]

Ah, actually you didn't set the relative path to your lib properly.

Add a pkg argument to your extern lib and use pkg.dir to teach Lake to point to your lib correctly when your project is being used as a dependency

extern_lib libffi pkg :=
  inputBinFile $ pkg.dir / "generated-rust-lib" / "libffi.a"