企业官网建设流程全解析

Lean 4 Reverse FFI 实战：用 Lake 构建共享库并从 C 程序调用

【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4

Lean 4 的 FFI（外部函数接口）通常指在 Lean 中调用 C 函数，而tests/lake/examples/reverse-ffi示例演示了与之相反的"反向 FFI"：将一个 Lean 库编译为动态共享库（.so/.dylib/.dll），再从 C 语言程序加载并调用其中用@[export]导出的 Lean 函数。读完本文，你将掌握@[export]导出机制、Lake 的sharedFacet共享库构建、Lean 运行时初始化流程，以及通过Makefile链接与运行 C + Lean 混合程序的完整实战方案。

示例总体结构与角色划分

本示例位于 tests/lake/examples/reverse-ffi，整个目录刻意保持最小化，仅包含三类角色：

这个结构对应了 README 所概括的核心理念：一个 Lake 库（lib/）可以被任意外部语言与构建系统（main.c+Makefile）使用。Lean 侧只负责"产出共享库"，调用方是谁、用什么构建系统，完全解耦。

第一步：用@[export]把 Lean 函数导出为 C 符号

lib/RFFI.lean 全文只有几行，却是整个反向 FFI 的基石：

@[export my_length] def myLength (s : String) : UInt64 := s.length.toUInt64

关键点拆解：

• @[export my_length]属性指示 Lean 编译器在生成 C 代码时，把函数myLength的符号名改为my_length，从而暴露为可供外部 C 程序直接链接/调用的 C 函数；
• 导出的函数签名必须满足可编译为 C 的类型约束：String在运行时对应lean_object*，UInt64对应uint64_t。这正是 main.c 中extern uint64_t my_length(lean_obj_arg);声明能够匹配的原因；
• 函数体的s.length.toUInt64演示了在 Lean 侧完成真实计算（求字符串长度），把"业务逻辑留在 Lean、外部只做壳"的反向 FFI 典型形态。

导出背后的机制

从源码结构看，@[export]的处理位于编译器的代码生成链路中：src/Lean/Compiler/下的导出（export）逻辑会把指定的 Lean 声明以给定名字写入生成的 C 声明，供外部链接。这类导出同时服务于正向 FFI（Lean 侧用@[extern]声明外部函数）与反向 FFI（本示例的@[export]），两者共同构成 doc/dev/ffi.md 所描述的 Lean FFI 全貌。

第二步：用 LakesharedFacet构建共享库

lib/lakefile.lean 是 Lake 侧的全部配置：

import Lake open System Lake DSL package rffi @[default_target] lean_lib RFFI where defaultFacets := #[LeanLib.sharedFacet]

逐项说明：

• package rffi：声明包名为rffi；
• lean_lib RFFI：声明一个名为RFFI的 Lean 库，对应本目录下的RFFI.lean；
• defaultFacets := #[LeanLib.sharedFacet]：把默认构建目标从普通的静态 olean 库改为共享库（shared library）facet。构建产物即动态库librffi_RFFI.so（Linux）/.dylib（macOS）/rffi_RFFI.dll（Windows），位于lib/.lake/build/lib/。

这里用到的LeanLib.sharedFacet是 Lake 的内置 facet 之一，其sharedFacetConfig定义于 src/lake/Lake/Build/Library.lean。facet 机制是 Lake 的核心抽象：构建系统通过sharedFacet将.olean/.c等中间产物进一步加工为动态链接库，开发者只需声明目标，Lake 负责推导完整构建图。ExternLib.sharedFacet（见 src/lake/Lake/Build/ExternLib.lean）则用于将第三方外部 C 库同样暴露为共享库，二者在 src/lake/Lake/Build/Infos.lean 中统一纳入 facet 构建流程。

构建命令（由 Makefile 的lake目标触发）：

lake --dir=lib build

执行后生成的共享库即为外部程序的链接对象。

第三步：在 C 程序中初始化 Lean 运行时并调用

main.c 展示了外部调用方的完整流程，分为"初始化"与"业务调用"两个阶段：

#include <stdio.h> #include <lean/lean.h> extern uint64_t my_length(lean_obj_arg); extern void lean_io_mark_end_initialization(); extern lean_object * initialize_rffi_RFFI(uint8_t builtin); int main() { lean_object * res; uint8_t builtin = 1; // 与 Lean 可执行文件使用相同的默认值 res = initialize_rffi_RFFI(builtin); if (lean_io_result_is_ok(res)) { lean_dec_ref(res); } else { lean_io_result_show_error(res); lean_dec(res); return 1; // 初始化失败时禁止访问 Lean 声明 } lean_io_mark_end_initialization(); // 实际业务 lean_object * s = lean_mk_string("hello!"); uint64_t l = my_length(s); printf("output: %ld\n", l); }

这段代码蕴含了反向 FFI 最关键的运行时约束：

1. 必须调用初始化函数：Lean 库中的顶层声明（包括@[export]的函数）在运行前需要初始化。Lake 会为每个包生成形如initialize_rffi_RFFI的初始化入口（命名规则为initialize_<包名>_<模块名>），返回lean_object*形式的IO结果；
2. 必须检查初始化结果：通过lean_io_result_is_ok判断成败，失败时用lean_io_result_show_error打印错误并退出，且注释明确指出"初始化失败时禁止访问 Lean 声明"，否则可能访问未就绪的对象；
3. 必须标记初始化结束：调用lean_io_mark_end_initialization()通知运行时初始化阶段已结束（源码注释给出的参考文档指向 Lean 手册的ffi-initialization小节），该机制用于回收/固化初始化期使用的资源；
4. 参数与返回值遵守 ABI：lean_obj_arg表示被借用（不递增引用计数）的 Lean 对象参数，lean_mk_string构造字符串对象，uint64_t为返回值；外部代码需自行保证引用计数正确（示例中初始化结果对象通过lean_dec_ref/lean_dec释放）。

第四步：Makefile 编译、链接与运行

Makerfile 提供了两种运行方式，覆盖了最常见的部署场景。

方式一：run—— 通过 rpath 指定动态库搜索路径

LEAN_SYSROOT ?= $(shell lean --print-prefix) LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean $(OUT_DIR)/main: main.c lake | $(OUT_DIR) cc -o $@ $< -I $(LEAN_SYSROOT)/include \ -L $(LEAN_LIBDIR) -L lib/.lake/build/lib \ -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS)

链接命令的要点：

• -I $(LEAN_SYSROOT)/include：找到lean/lean.h（Lean 运行时头文件，实际位于 src/include/lean 下，安装后位于 sysroot 的 include 目录）；
• -L $(LEAN_LIBDIR) -L lib/.lake/build/lib：同时加入 Lean 自身运行时库目录与 Lake 构建出的共享库目录；
• -l$(LIB_NAME)（即-lrffi_RFFI）链接本示例的 Lean 共享库；-lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared链接 Lean 标准库与运行时（分层共享库命名）；
• 非 Windows 平台通过-Wl,-rpath,...把LEAN_LIBDIR与lib/.lake/build/lib写入可执行文件，保证运行期动态加载器能找到依赖；Windows 下则改用env PATH=...在运行前动态注入库路径；
• $(OUT_DIR)/main依赖lake目标，确保先执行lake --dir=lib build再编译。

方式二：run-local—— 复制依赖得到可移植可执行文件

如果不想配置搜索路径，可以"把所有共享库依赖复制到当前目录"，得到更便携的产物：

ifeq ($(shell uname -s),Darwin) LINK_FLAGS_LOCAL := -Wl,-rpath,@executable_path SHLIB_EXT := dylib else LINK_FLAGS_LOCAL := -Wl,-rpath,'$${ORIGIN}' SHLIB_EXT := so endif $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR) cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)$(LIB_NAME).$(SHLIB_EXT) $(OUT_DIR) cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) \ -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL)

• 将 Lean 运行时的全部共享库与librffi_RFFI.so一并cp到out/，随后仅-L $(OUT_DIR)即可完成链接；
• 运行期路径交给$ORIGIN（Linux）或@executable_path（macOS）解析，即"以可执行文件自身所在目录为基准"，Windows 默认即当前目录，无需额外设置；
• 注意平台差异的封装：SHLIB_PREFIX/SHLIB_EXT/LEAN_SHLIB_ROOT按 Windows / macOS / Linux 分支取值，$(OS)与uname -s配合判断。

两个目标的关系

.PHONY: all run run-local lake all: run run-local

make all（默认目标）会依次构建并运行run与run-local两种方式，预期输出均为output: 6（"hello!"长度为 6）。

第五步：一键验证与清理

test.sh 提供端到端验证：

set -ex LAKE=${LAKE:-../../.lake/build/bin/lake} ./clean.sh LAKE=$LAKE make run LAKE=$LAKE make run-local

• LAKE环境变量默认指向仓库内构建出的 Lake 可执行文件（../../.lake/build/bin/lake），也可通过环境变量覆盖为系统安装的lake；
• 先clean.sh清理上次产物（rm -rf out lib/.lake lib/lake-manifest.json），再分别验证两种运行方式，set -ex保证任何一步失败即中止并回显命令；
• 该脚本同时作为 Lake 测试套件的一部分（tests/lake 目录中的示例均可由 CI 直接驱动），印证了示例的正确性。

反向 FFI 的适用场景与注意事项

综合整个示例，可以总结出反向 FFI 在工程实践中的定位：

• 适用场景：把 Lean 实现的算法/逻辑以共享库形式嵌入 C/C++ 宿主程序（如已有的大型 C 代码库）、其他语言通过 C ABI 间接调用 Lean、或分发不含完整 Lean 可执行文件的二进制组件；
• 必须做的三件事：@[export]导出符号、lean_lib+sharedFacet产出共享库、调用方完成运行时初始化与lean_io_mark_end_initialization；
• 需要小心的地方：引用计数（lean_obj_arg借用语义与lean_dec_ref释放）、初始化失败保护、跨平台动态库路径（rpath / PATH /$ORIGIN）、以及导出函数签名的 ABI 兼容性（仅限可编译为 C 的类型，如String↔lean_object*、UInt64↔uint64_t）。

这个最小示例从零展示了 Lean 4 反向 FFI 的完整链路，lib/（Lake 库）与main.c+Makefile（外部语言与构建系统）的分离设计，恰好印证了 README 的核心观点：Lean 库是"可被外部复用的构件"，而非只能通过lake build生成可执行文件的封闭单元。将其中的模式迁移到自己的项目时，只需替换导出函数、包名与链接库名即可。

【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4