12.4.1. Lean ABI🔗

Lean 应用程序二进制接口 (ABI) 描述如何在平台本机调用约定中对 Lean 声明的签名进行编码。 它基于标准C ABI和目标平台的调用约定。 可以使用属性 Lean 标记 Lean 声明以与外部函数交互，这会导致编译代码使用 C 声明 sym 作为实现，也可以使用属性 export sym 进行标记，这使得声明可作为 sym 提供给 C。

在这两种情况下，C 声明的类型均派生自具有属性的声明的 Lean 类型。 令 α₁ → ... → αₙ → β 为声明的 规范化 类型。 如果 n 为 0，则对应的 C 声明为

extern s sym;

其中 s 是 β 的 C 翻译，如 下一节中指定。 对于标记为 extern 的定义，仅保证在调用 Lean 模块的初始化程序或导入模块的初始化程序后初始化符号的值。 关于 初始化 的部分更详细地描述了初始化器。

如果 n 大于 0，则相应的 C 声明为

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

其中参数类型 tᵢ 是类型 αᵢ 的 C 翻译。 对于 extern，首先删除所有 不相关 类型。

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/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.
@& term

12.4.2. 初始化🔗

当在较大的程序中包含 Lean 代码时，模块在访问其任何声明之前必须是 initialized。 模块初始化需要：

• 所有“常量定义”（空函数）的初始化，包括从其他函数中取出的封闭术语，

• 执行标有 init 属性的所有代码，以及

• 如果已设置模块初始值设定项的 builtin 参数，则执行标有 builtin_init 属性的所有代码。

对于从 Lean 代码编译的可执行文件以及使用 lean --plugin 加载的“插件”，模块初始化程序会使用 builtin 标志自动运行。 对于 lean 导入的所有其他模块，初始化程序在没有 builtin 的情况下运行。 换句话说，init 函数当且仅当其模块被导入时才会运行，无论它们是否具有可用的本机代码，而 builtin_init 函数仅针对本机可执行文件或插件运行，无论其模块是否已导入。 Lean 编译器使用内置初始化程序来实现诸如注册基本解析器之类的目的，这些解析器即使在不导入其模块的情况下也应该可用，这是引导所必需的。

包 foo 中模块 A.B 的初始化程序称为 initialize_foo_A_B。 对于 Lean内核中的模块（例如 Init.Prelude），初始化程序称为 initialize_Init_Prelude。 模块初始化程序将自动初始化任何导入的模块。 它们也是幂等的（当使用相同的 builtin 标志运行时），但不是线程安全的。

对于与流程相关的功能很重要：使用 libuv 中的流程相关功能（例如 Std.IO.Process.getProcessTitle 和 Std.IO.Process.setProcessTitle）的应用程序必须调用 lean_setup_args(argc, argv)（它返回可能已修改的 argv，必须用来代替原始的）在调用 lean_initialize() 或lean_initialize_runtime_module()。 这可以正确设置进程处理功能，这对于 Lean 运行时可能依赖的某些系统级操作至关重要。

与 Lean 运行时的初始化一起，在访问任何 Lean 声明之前，应运行如下代码一次：

void lean_initialize_runtime_module();
void lean_initialize();
char ** lean_setup_args(int argc, char ** argv);

lean_object * initialize_A_B(uint8_t builtin);
lean_object * initialize_C(uint8_t builtin);
...

argv = lean_setup_args(argc, argv); // if using process-related functionality
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_foo_A_B(builtin);
if (lean_io_result_is_ok(res)) {
    lean_dec_ref(res);
} else {
    lean_io_result_show_error(res);
    lean_dec(res);
    return ...;  // do not access Lean declarations if initialization failed
}
res = initialize_bar_C(builtin);
if (lean_io_result_is_ok(res)) {
...

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

此外，任何其他不是由 Lean 运行时本身生成的线程都必须通过调用来初始化以供 Lean 使用

void lean_initialize_thread();

并且应该通过调用来最终确定以释放所有线程本地资源

void lean_finalize_thread();

12.4.3. 解释器中的 @[extern]🔗

Lean 解释器可以运行 Lean 声明，这些声明的符号在加载的共享库中可用，其中包括标记为 extern 的声明。 要运行此代码（例如使用 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），需要执行以下步骤：

1. 包含声明及其依赖项的模块必须编译成共享库

2. 应将此共享库提供给 lean --load-dynlib= 以运行导入模块的代码。

加载包含外部符号的外部库是不够的，因为解释器依赖于为每个 extern 声明发出的代码。 因此，无法解释同一文件中的 extern 声明。 Lean 源存储库在 tests/compiler/foreign 中包含此用法的示例。