Using foreign functions with --plugin

Stream: lean4

[Owen W]

Hello, I have been messing around with the extern command. Using resources such as https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign, I have been able to use c++ objects in a lean project by compiling it to an executable. I would now like to use c++ objects (foreign functions) in lean programs without needing to compile them. In other words, I would like to be able to use lean --run or the interactive vscode theorem prover with foreign function. I found a possible method of doing this here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Using.20result.20from.20foreign.20function.20in.20a.20tactic. I created the shared object by running leanc -shared -x none test.cpp -o build/bin/plugin.so. In this instance, test.cpp is the file containing the c++ objects that I want to use, and the file is compiled to build/bin/plugin.so. This step executes successfully as far as I can tell, but upon passing the file to lean using lean --run --plugin=./build/bin/plugin.so main.lean I get an error:
terminate called after throwing an instance of 'lean::exception' what(): error, plugin /home/owenr/Documents/LEAN/testing/build/bin/plugin.so does not seem to contain a module 'plugin.Default' Aborted (core dumped)
In the resource that I linked above (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Using.20result.20from.20foreign.20function.20in.20a.20tactic), it appears that @Ramon Fernandez Mir seemed experienced the same problem, though I'm not really sure how it was resolved.
What would be the best way to resolve it?

[Mac]

@Owen W A couple notes:

1. That post is rather out of date, a lot has changed since then. You should load a shared library containing foreign functions through --load-dynlib not --plugin.
2. To use a foreign function interactively in Lean, the shared library needs to have both the foreign implementation of function extern function and the compiled Lean module with the extern definition.

[Mac]

For example, if you have lean_object* foo(lean_object*) in a C file and @[extern "foo"] constant foo : IO Unit" in a Lean file. The resulting foo.so you pass to --load-dynlib` needs to include the compiled versions of both.

[Mac]

A step-by-step process would look something like:

1. Compile the external C file: cc -c -o ext_foo.o ext_foo.c
2. Compile the Lean file into a C file: lean -c foo.c Foo.lean
3. Compile the Lean C file: leanc -c -o foo.c foo.o
4. Link them together into a shared library: leanc -shared -o foo.so foo.o ext_foo.o
5. Load the shared library when interpreting a Lean file using the extern definition: lean --load-dynlib=foo.so test.lean

[Ramon Fernandez Mir]

@Owen W the main difference I see with my code is that you're not using the -L option in leanc to add a directory to the library search path but I might be wrong. I suggest taking a look at the makefiles in: https://github.com/cpehle/lean4-plugin-example

[Owen W]

I managed to get my foreign functions working using --load-dynlib thanks @Mac 's instructions. Thanks all for helping to clear up this process.