20.3.1. The Lean ABI

The Lean Application Binary Interface (ABI) describes how the signature of a Lean declaration is encoded in the platform-native calling convention. It is based on the standard C ABI and calling convention of the target platform. Lean declarations can be marked for interaction with foreign functions using either the attribute extern "sym", which causes compiled code to use the C declaration sym as the implementation, or the attribute export sym, which makes the declaration available as sym to C.

In both cases, the C declaration's type is derived from the Lean type of the declaration with the attribute. Let α₁ → ... → αₙ → β be the declaration's normalized type. If n is 0, the corresponding C declaration is

extern s sym;

where s is the C translation of β as specified in the next section. In the case of a definition marked extern, the symbol's value is only guaranteed to be initialized after calling the Lean module's initializer or that of an importing module. The section on initialization describes initializers in greater detail.

If n is greater than 0, the corresponding C declaration is

s sym(t₁, ..., tₙ);

where the parameter types tᵢ are the C translations of the types αᵢ. In the case of extern, all irrelevant types are removed first.

term ::= ...
    | Indicates that an argument to a function marked `@[extern]` is borrowed.

Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked `@[extern]`.

When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.

Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.
@& term

20.3.2. Initialization🔗

When including Lean code in a larger program, modules must be initialized before accessing any of their declarations. Module initialization entails:

• initialization of all “constant definitions” (nullary functions), including closed terms lifted out of other functions,

• execution of all code marked with the init attribute, and

• execution of all code marked with the builtin_init attribute, if the builtin parameter of the module initializer has been set.

The module initializer is automatically run with the builtin flag for executables compiled from Lean code and for “plugins” loaded with lean --plugin. For all other modules imported by lean, the initializer is run without builtin. In other words, init functions are run if and only if their module is imported, regardless of whether they have native code available, while builtin_init functions are only run for native executable or plugins, regardless of whether their module is imported. The Lean compiler uses built-in initializers for purposes such as registering basic parsers that should be available even without importing their module, which is necessary for bootstrapping.

The initializer for module A.B is called initialize_A_B and will automatically initialize any imported modules. Module initializers are idempotent when run with the same builtin flag, but not thread-safe. Together with initialization of the Lean runtime, code like the following should be run exactly once before accessing any Lean declarations:

void lean_initialize_runtime_module();
void lean_initialize();
lean_object * initialize_A_B(uint8_t builtin, lean_object *);
lean_object * initialize_C(uint8_t builtin, lean_object *);
...

lean_initialize_runtime_module();
// Necessary (and replaces `lean_initialize_runtime_module`) for code that
// (indirectly) accesses the `Lean` package:
//lean_initialize();

lean_object * res;
// use same default as for Lean executables
uint8_t builtin = 1;
res = initialize_A_B(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
    lean_dec_ref(res);
} else {
    lean_io_result_show_error(res);
    lean_dec(res);
    // do not access Lean declarations if initialization failed
    return ...;
}
res = initialize_C(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
...

// Necessary for code that (indirectly) uses `Task`
//lean_init_task_manager();
lean_io_mark_end_initialization();

In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling

void lean_initialize_thread();

and should be finalized in order to free all thread-local resources by calling

void lean_finalize_thread();

20.3.3. @[extern] in the Interpreter

The Lean interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes declarations that are marked extern. To run this code (e.g. with Lean.Parser.Command.eval : command`#eval e` evaluates the expression `e` by compiling and evaluating it. * The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result. * If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m` to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`. Users can define `MonadEval` instances to extend the list of supported monads. The `#eval` command gracefully degrades in capability depending on what is imported. Importing the `Lean.Elab.Command` module provides full capabilities. Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly, since the presence of `sorry` can lead to runtime instability and crashes. This check can be overridden with the `#eval! e` command. Options: * If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances. * If `eval.type` is true (default: false) then pretty prints the type of the evaluated value. * If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance when there is no other way to print the result. See also: `#reduce e` for evaluation by term reduction. #eval), the following steps are necessary:

1. The module containing the declaration and its dependencies must be compiled into a shared library

2. This shared library to should be provided to lean --load-dynlib= to run code that imports the module.

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. The Lean source repository contains an example of this usage in tests/compiler/foreign.