From b2f331f502975ccf2bd0dc16404fd386c47adc2a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 29 Oct 2021 19:11:17 +0200 Subject: [PATCH] doc: --load-dynlib --- doc/dev/ffi.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md index c19e780767..545402ae66 100644 --- a/doc/dev/ffi.md +++ b/doc/dev/ffi.md @@ -95,3 +95,15 @@ if (lean_io_result_is_ok(res)) { //lean_init_task_manager(); // necessary if you (indirectly) use `Task` lean_io_mark_end_initialization(); ``` + +## `@[extern]` in the Interpreter + +The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations. +Thus to e.g. run `#eval` on such a declaration, you need to +1. compile (at least) the module containing the declaration and its dependencies into a shared library, and then +1. pass this library to `lean --load-dynlib=` to run code `import`ing this module. + +Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration. +Thus it is not possible to interpret an `@[extern]` declaration in the same file. + +See `tests/compiler/foreign` for an example.