Zulip Chat Archive

Stream: lean4

Topic: Package with native (foreign) dependencies


Christian Pehle (Jun 09 2021 at 12:16):

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 (Jun 09 2021 at 14:02):

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 (Jun 09 2021 at 15:29):

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 (Jun 09 2021 at 15:32):

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 (Jun 09 2021 at 15:42):

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 (Jun 09 2021 at 15:53):

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.


Last updated: Dec 20 2023 at 11:08 UTC