Package with native (foreign) dependencies

Stream: lean4

[Christian Pehle]

Is there some example that shows how to create a library with native (C++) dependencies? I have been able to create a working binary using the foreign function interface as in (https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign), but I am unsure how to create a library / package instead that one could import. I've found --plugin, but that seems to be meant for compiler plugins.

[Sebastian Ullrich]

It's not clear to me what you are asking for. You can pass additional libraries to link to using leanpkg build bin/lib LINK_OPTS=....

[Christian Pehle]

Ok that makes sense, so one just creates a C++ library and then leanpkg will link against it resolving the @[extern ...] declarations. Thanks!

[Sebastian Ullrich]

Ideally you could specify link options in leanpkg.toml and they would be appropriately inherited by dependent packages. The Nix setup has something like this, and there Nix also takes care of the problem of fetching/compiling those libraries in the first place.

[Christian Pehle]

Ok I guess I will check out the nix setup as well then. My primary motivation is to be able to interactively use the package in VSCode, this is easy if you are just writing Lean code, but it wasn't obvious to me how to accomplish it, if you have native code involved.

[Sebastian Ullrich]

Hmm, interactive use is a bit of a different matter. You need to get Lean to load the foreign code at runtime. If you statically link it into your Lean library, you can indeed use --plugin for that.