leanprover/lean4checker

# ⚠️ 废弃：lean4checker 现已内置至 Lean **此仓库已弃用，即将归档。** `lean4checker` 已合并至 Lean 4 仓库本体，并以 `leanchecker` 形式随每个 Lean 工具链分发（自 v4.28.0 起）。您不再需要 此独立仓库。 ## 使用内置的 `leanchecker` 要使用内置检查器检查项目的 `.olean` 文件，请运行： ``` lake env leanchecker ``` 或检查单个模块： ``` lake env leanchecker Mathlib.Data.Nat.Basic ``` 或重新播放所有常量到一个全新环境： ``` lake env leanchecker --fresh Mathlib ``` 由于 `leanchecker` 是工具链的一部分，`lake env` 会自动找到它—— 无需构建或指向独立二进制文件。 ## 原始 README 使用 Lean 内核重新检查编译后的 Lean `olean` 文件。 `lake exe lean4checker ` 会重新播放 `` 中的环境， 从其导入提供的环境开始， 确保内核接受所有声明。 不带参数的 `lake exe lean4checker` 会并行对搜索路径上的每个 `.olean` 文件运行 `lean4checker`（注意这包括 Lean 4 和您项目的所有依赖项）。 您还可以使用 `lake exe lean4checker --fresh Mathlib.Data.Nat.Basic` 将所有常量 （包括导入和该文件中定义的）重新播放到一个全新环境中。 这是单线程的，速度可能慢得多。 这并非外部验证器，因为它使用的是 Lean 内核本身。 然而，它作为检测"环境篡改"的工具非常有用， 即使用元编程功能构建不一致的 Lean 环境。

标签：Lean 4, .olean 文件, TLS抓取, 一致性检测, 云安全监控, 元编程, 内核验证, 声明检查, 工具链, 形式化验证, 环境重放, 类型系统, 编程语言, 编译器, 软件安全, 静态分析