Lean 4 同时承担定理证明器与通用程序设计语言两种角色。前十六篇聚焦逻辑与证明工程；本篇转向可执行端：从 #eval 求值，到 lake build 编译本地二进制，再到通过 FFI 调用 C/Rust 代码，最后讨论影响运行期性能的属性与编译选项。

Lean 4 作为编程语言：#eval 与 IO

Lean 4 的类型论本身不区分"证明代码"与"程序代码"——两者都是项（term）。运行 Lean 代码最轻量的方式是 #eval，它在编译时对表达式求值并在 InfoView 中显示结果。

1
2
3
#eval 1 + 1          -- InfoView 输出：2
#eval "hello".length -- InfoView 输出：5
#eval List.range 5   -- InfoView 输出：[0, 1, 2, 3, 4]

涉及副作用（文件读写、网络、标准输入输出）时，表达式类型变为 IO α：

1
2
#eval IO.println "hello from Lean"
-- 输出：hello from Lean

IO 是 Lean 4 对副作用的封装，与 Haskell 的 IO monad 语义相近，但在实现层与 C 运行时直接对接。在 InfoView 中，#eval 对 IO α 执行求值并显示 α 的结果（若有）；这一过程在编辑器语言服务器进程内发生，无需独立编译步骤。

main 入口函数的类型是 IO Unit：

1
2
def main : IO Unit := do
  IO.println "Hello, world!"

lake build 编译此定义后，生成的二进制执行 main，打印字符串并退出。

编译流水线：Lean → C → 二进制

lake build 调用的不是直接的机器码生成器，而是先将 Lean 代码翻译为 C，再由系统 C 编译器（通常是 cc 或 clang）编译成目标二进制。流水线分三个阶段：

1
.lean  →  lean c-backend  →  .c  →  cc/clang  →  .o  →  ld  →  binary

build/ 目录的典型内容：

1
2
3
4
5
6
.lake/build/
  lib/
    MyProject.olean     -- 已检查的类型信息缓存
    MyProject.c         -- C 后端输出
  bin/
    myproject           -- 最终可执行文件

.olean 文件是 Lean 的"已编译模块"格式，存储类型检查结果与元数据；.c 文件包含所有定义展开后的 C 实现，可直接阅读（虽然冗长）。

调试编译输出时，lake build --verbose 会打印每一步命令，包括 cc 的调用参数。

@[extern]：从 Lean 调用 C

当 Lean 定义带有 @[extern "c_function_name"] 属性时，编译器在遇到该定义的调用点时，改为生成对指定 C 函数的调用，而不展开 Lean 侧的实现（如果有的话）。

典型写法——声明一个 Lean 函数，其实体由 C 实现：

1
2
3
-- MyProject/FFI.lean
@[extern "lean_myproject_add"]
opaque myAdd (x y : UInt32) : UInt32

opaque 声明告诉 Lean 类型检查器：该函数存在、类型确定，但没有可见的项定义。编译器生成调用 lean_myproject_add 的 C 代码，链接器负责将名称解析到提供该函数的目标文件或库。

对应的 C 实现（c/myproject.c）：

1
2
3
4
5
#include <lean/lean.h>

LEAN_EXPORT uint32_t lean_myproject_add(uint32_t x, uint32_t y) {
    return x + y;
}

UInt32、UInt64、Float 等标量类型在 FFI 边界按值传递，不需要装箱。

@[export]：将 Lean 函数暴露给 C

反方向——把 Lean 函数导出为 C 可见符号——使用 @[export "lean_function_name"]：

1
2
3
4
5
@[export "lean_fib"]
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

编译后，链接到该库的 C 代码可以通过 lean_fib(n) 调用此函数。注意 Nat 不是标量，其 C 类型是 lean_object *，需要按 Lean 运行时约定处理（见下节）。

运行时表示：lean_object 与引用计数

Lean 4 运行时对所有堆上对象使用统一的 lean_object 结构。每个对象头部存储：

  • 引用计数（rc）：有符号 32 位整数
  • 类型标签（tag）：用于区分构造子、数组、字符串等
  • 析构函数指针（del_fn）：rc 降到 0 时调用

标量（UInt32、Bool 等固定大小的基本类型）在编译器确认时不装箱，直接按值传递；Nat 在小值时用"tagged integer"编码（低位为 1），大值时升级为堆上的多精度整数对象。

引用计数相关宏：

1
2
3
lean_inc(o)    // 增加引用计数
lean_dec(o)    // 减少引用计数，若降为 0 则析构
lean_inc_n(o, n)  // 批量增加 n

lean_dec 是递归的：析构一个构造子时，会对其每个字段递归调用 lean_dec。

编写 C shim：字符串与内存管理

字符串在运行时是 lean_object *，由 lean_mk_string 创建：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
#include <lean/lean.h>

LEAN_EXPORT lean_obj_res lean_myproject_greet(lean_obj_arg name) {
    // name 是 Lean String，转为 C const char *
    const char *cname = lean_string_cstr(name);

    char buf[256];
    snprintf(buf, sizeof(buf), "Hello, %s!", cname);

    // 归还入参的引用（调用者已转移所有权）
    lean_dec(name);

    // 构造返回的 Lean String
    return lean_mk_string(buf);
}

几个关键约定：

  • lean_obj_arg 表示该参数的所有权被"转移"给被调函数：函数内部负责最终 lean_dec。
  • lean_obj_res 表示返回值将所有权转移给调用方。
  • 如果函数需要"借用"而非拥有参数，使用 b_lean_obj_arg，此时不应调用 lean_dec。

对应的 Lean 声明：

1
2
@[extern "lean_myproject_greet"]
opaque greet (name : String) : String

IO monad 与 FFI 边界

涉及副作用（文件、网络、全局状态）的 C 函数，在 Lean 侧应包裹在 IO：

1
2
@[extern "lean_myproject_read_file"]
opaque readFileFfi (path : String) : IO String

C 侧原型变为：

1
2
3
4
5
6
7
8
9
10
11
// IO α 对应 lean_obj_res (*)(lean_obj_arg world)
// world 是 RealWorld token，约定必须原样传回
LEAN_EXPORT lean_obj_res lean_myproject_read_file(lean_obj_arg path,
                                                   lean_obj_arg world) {
    const char *cpath = lean_string_cstr(path);
    lean_dec(path);
    // ... 读取文件 ...
    lean_obj_res result = lean_mk_string(contents);
    lean_dec(world);
    return lean_io_result_mk_ok(result);
}

lean_io_result_mk_ok 将结果包装为 IO.Result.ok；发生错误时用 lean_io_result_mk_error。

需要绕过 IO 约束执行"不安全"操作时，Lean 提供 unsafePerformIO（位于 Init.System.IO），与 Haskell 的 unsafePerformIO 语义相同，只在明确知道无竞态且无可见副作用时使用。

lakefile.lean：链接外部 C/C++ 代码

Post 01 介绍了 lakefile.lean 的基本结构。链接外部 C 代码需要在 executable 或 library 目标中添加两类选项：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
-- lakefile.lean
import Lake
open Lake DSL

package myProject where
  name := "myProject"

lean_lib MyProject

-- 链接外部 C 目标文件
extern_lib leanMyprojectFfi := do
  let name := nameToStaticLib "leanmyproject_ffi"
  let ffiO ← compileCFile (Lake.srcDir / "c" / "myproject.c") {}
  buildStaticLib (Lake.libDir / name) #[ffiO]

lean_exe myproject where
  root := `Main
  -- 额外链接参数（如系统库）
  moreLinkArgs := #["-lm"]
  -- 额外 Lean 编译器参数（如头文件路径）
  moreLeancArgs := #["-I", "c/include"]

extern_lib 声明告诉 Lake 如何构建外部静态库，并将其纳入依赖图。compileCFile 调用系统 C 编译器；buildStaticLib 产生 .a 文件，链接阶段自动包含。

多个 C 文件时，compileCFile 的调用可以并行：

1
2
3
4
extern_lib leanFfi := do
  let srcs := #["c/a.c", "c/b.c"]
  let objs ← srcs.mapM (fun s => compileCFile (Lake.srcDir / s) {})
  buildStaticLib (Lake.libDir / nameToStaticLib "leanffi") objs

与 Rust 互操作

Rust 提供 C ABI 兼容的 FFI，因此 Lean ↔ Rust 的桥接路径与 Lean ↔ C 相同：在 Rust 侧用 #[no_mangle] 与 extern "C" 导出函数，Lean 侧用 @[extern] 声明，lakefile.lean 链接 .a 文件。

Rust 侧示例（rust/src/lib.rs）：

1
2
3
4
5
6
7
8
9
10
11
use std::ffi::CStr;

#[no_mangle]
pub extern "C" fn lean_myproject_rust_hello(name_ptr: *const u8) -> *mut u8 {
    // 注意：真实场景需要配合 lean_object* 的内存管理约定
    // 这里仅展示概念；完整实现须使用 lean4-sys 或手工管理
    let name = unsafe { CStr::from_ptr(name_ptr as *const i8) };
    let result = format!("Hello from Rust, {}!", name.to_string_lossy());
    // 必须通过 lean_mk_string 分配，或直接操作 lean_object*
    Box::into_raw(result.into_bytes().into_boxed_slice()) as *mut u8
}

社区项目 lean4-sys（crates.io）提供了 lean_object、lean_mk_string 等的 Rust 绑定，使上述代码不需要裸 unsafe 指针操作。lakefile.lean 里可用 buildRustLib（非官方 Lake 扩展）或手工调用 cargo build --release 后链接 target/release/libmyproject.a。

性能属性：@[inline]、@[specialize]、@[implementedBy]

Lean 4 的 C 后端支持三个与运行时性能密切相关的属性：

@[inline]：请求编译器将函数展开到调用点，减少函数调用开销，适合短小的组合子。

1
2
@[inline]
def square (x : Int) : Int := x * x

@[specialize]：对多态函数生成按具体类型参数特化的版本，避免通过类型类字典间接调用。

1
2
3
@[specialize]
def sumList [Add α] [OfNat α 0] (xs : List α) : α :=
  xs.foldl (· + ·) 0

@[implementedBy]：用于将一个函数的逻辑规范与高效的运行时实现分离。规范版本用于证明，@[implementedBy] 指向的版本用于执行：

1
2
3
4
5
6
7
8
9
10
-- 逻辑规范（用于证明）
def mySort (xs : List Nat) : List Nat :=
  xs.mergeSort

-- 高效实现（仅运行时使用）
@[extern "lean_myproject_sort_ffi"]
opaque mySortFast (xs : List Nat) : List Nat

-- 将执行路径重定向到 mySortFast
attribute [implementedBy mySortFast] mySort

#print axioms mySort 此时会显示 implementedBy 公理被引入：

1
2
3
#print axioms mySort
-- mySort depends on axioms:
--   propext, Classical.choice, Quot.sound, implementedBy

implementedBy 公理表明：逻辑上使用的是规范定义，但运行时替换为指定实现。这不影响证明的可信度，但代码的运行结果依赖外部实现的正确性。

证明与 @[extern] 共存：term-mode 与 tactic-mode 对比

一个带有 @[extern] 的 opaque 函数本身无法在 Lean 内部展开，因此不能用 simp 或 rfl 证明关于它的等式命题。此时需要引入公理或依赖外部证明。

对于有完整 Lean 实现且同时带有 @[extern] 的函数（extern 仅替换执行路径），可以对规范定义本身做证明。以一个带有外部实现的加法函数为例：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
-- 规范定义（可证明性质）
def myAdd' (x y : Nat) : Nat := x + y

-- 为规范定义提供外部实现
@[extern "lean_myproject_add"]
opaque myAdd (x y : Nat) : Nat

attribute [implementedBy myAdd] myAdd'

-- tactic-mode 证明规范定义的性质
theorem myAdd'_comm (x y : Nat) : myAdd' x y = myAdd' y x := by
  simp [myAdd', Nat.add_comm]

-- term-mode 等价写法
theorem myAdd'_comm' (x y : Nat) : myAdd' x y = myAdd' y x :=
  Nat.add_comm x y

tactic-mode 在引入假设或处理多步等式链时更易读；term-mode 在等式由单个引理直接覆盖时更简洁。两者可混用，by exact Nat.add_comm x y 是常见的桥接写法。

对于完全 opaque 的外部函数，若要建立其数学性质，需要以 axiom 形式在 Lean 侧声明该性质并接受其为公理——这会被 #print axioms 显示，使信任代价显式化。

形式化项目交付时，通常需要确认核心定理不依赖非预期的公理。#print axioms 展示传递依赖：

1
2
3
4
5
6
7
8
theorem my_theorem : ... := ...

#print axioms my_theorem
-- 若干净：
-- 'my_theorem' does not depend on any axioms
-- 若引入了 extern/implementedBy：
-- my_theorem depends on axioms:
--   propext, Classical.choice, Quot.sound, implementedBy

在含有 FFI 的项目中，保持核心逻辑部分（证明树）与执行部分（带 @[implementedBy] 或 opaque extern 的路径）的明确分层，是控制可信基（trusted base）的标准做法。

练习

练习一：编写一个 C 函数 lean_clz32，接收 uint32_t，返回前导零计数（count leading zeros）。在 lakefile.lean 中完成构建配置，使 #eval clz32 0x00FF0000 输出 8。

练习二：为练习一中的 clz32 写一个 Lean 规范版本 clz32Spec（用递归或 BitVec 库实现），再用 @[implementedBy] 将执行路径指向 C 实现。运行 #print axioms clz32Spec，观察 implementedBy 公理的出现位置。

练习三：用 @[export "lean_compute"] 导出一个接受 Nat 返回 Nat 的 Lean 函数，编写一段 C 的 main.c（不依赖 Lean main），通过 lean_initialize 初始化运行时后调用该函数并打印结果。参考 Lean 源码中 src/include/lean/lean.h 的 lean_initialize、lean_finalize 文档注释。

参考资料

  • Lean 4 官方文档：Compiler and FFI
  • lean/lean.h：Lean 运行时 C API 头文件，随 Lean 工具链分发
  • Lake 文档：lakefile.lean DSL
  • lean4-sys（crates.io）：Lean 运行时的 Rust 绑定
  • 本系列 Post 01：Lake 项目结构与依赖管理（构建系统基础、lean-toolchain 锁定、lakefile.lean 多目标配置）
  • 本系列 Post 02：Term-mode 与 Tactic-mode 切换心法（by exact 与纯项写法的等价关系）