工程组织

lakefile 配置、模块与命名空间、依赖管理与缓存、CI 设置，以及大型形式化项目的组织经验。

lakefile

较新版本用 TOML：

name = "myproject"
version = "0.1.0"
defaultTargets = ["myproject"]

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "Myproject"

[[lean_exe]]
name = "myproject"
root = "Main"

旧格式是 lakefile.lean（用 Lean DSL 写）：

import Lake
open Lake DSL

package «myproject» where
  leanOptions := #[⟨`autoImplicit, false⟩]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

lean_lib «Myproject» where

@[default_target]
lean_exe «myproject» where
  root := `Main

两种都能用，TOML 更简洁，Lean 格式更灵活（可以写逻辑）。

常用 lake 命令

lake build              # 构建
lake build Myproject.Basic   # 只构建某个模块
lake exe myproject      # 运行
lake clean              # 清理
lake update             # 更新依赖（会改 lake-manifest.json）
lake exe cache get      # 下载 Mathlib 预编译缓存
lake env lean File.lean # 单文件检查

lake update 要谨慎——它会把依赖更新到最新，可能同时要求更换 Lean 版本，导致整个项目需要适配。

lake-manifest.json 记录了精确的依赖版本，应该提交进 git——它保证团队成员和 CI 用同样的依赖。

模块与命名空间

文件路径 = 模块名：

Myproject/
├── Basic.lean          → import Myproject.Basic
├── Advanced.lean       → import Myproject.Advanced
└── Data/
    └── Tree.lean       → import Myproject.Data.Tree

根模块 Myproject.lean 通常只做汇总：

-- Myproject.lean
import Myproject.Basic
import Myproject.Advanced
import Myproject.Data.Tree

命名空间独立于文件结构，但惯例上对应：

-- Myproject/Data/Tree.lean
namespace Myproject.Data

inductive Tree (α : Type) where
  | leaf
  | node : Tree α → α → Tree α → Tree α

def Tree.size : Tree α → Nat
  | .leaf => 0
  | .node l _ r => l.size + 1 + r.size

end Myproject.Data

Tree.size 定义在 Tree 命名空间下，就能用点记法 t.size——广义字段记法按类型名找函数。

这是 Lean 的重要惯例：给类型 T 的操作，定义成 T.操作名。

重要的 lean options

set_option autoImplicit false
set_option relaxedAutoImplicit false

autoImplicit 默认开启：用到未声明的小写标识符时，Lean 自动把它当隐式参数。

-- autoImplicit 开启时这能编译
def myFunc (xs : List α) : Nat := xs.length
--                    ^ α 未声明，被自动当作隐式参数

方便，但会掩盖拼写错误：

def bad (n : Nat) : Nat := m + 1     -- m 被当成隐式参数，而不是报错！

Mathlib 与多数严肃项目关闭它：

[leanOptions]
autoImplicit = false
relaxedAutoImplicit = false

关闭后必须显式声明：

universe u
variable {α : Type u}

def myFunc (xs : List α) : Nat := xs.length

其他常用选项：

选项	作用
`pp.unicode.fun`	用 `↦` 显示 lambda
`maxHeartbeats`	单个声明的计算预算
`maxRecDepth`	递归深度
`warningAsError`	警告当错误（CI 用）

依赖管理

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.32.0"          # 可以钉版本

或从 git：

[[require]]
name = "mylib"
git = "https://github.com/user/mylib"
rev = "main"

Reservoir 是 Lean 的包索引（reservoir.lean-lang.org），用 scope + name 就能引用已发布的包。

版本兼容的现实：依赖的 Lean 版本必须一致。Mathlib 要求 lean-toolchain 与它一致，所以引入 Mathlib 等于把项目的 Lean 版本钉死在 Mathlib 当前用的那个。

CI

GitHub Actions 的标准配置：

name: CI
on: [push, pull_request]

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install elan
        run: |
          curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Get Mathlib cache
        run: lake exe cache get

      - name: Build
        run: lake build

      - name: Check for sorry
        run: |
          ! grep -rn "sorry" --include="*.lean" Myproject/

三个要点：

lake exe cache get 必须有——否则 CI 要编译整个 Mathlib，超时。
检查 sorry——用 grep 或更严谨地用 #print axioms。
可以缓存 .lake 目录进一步加速。

更严谨的 sorry 检查：

-- Test/NoSorry.lean
import Myproject
open Lean in
run_cmd do
  let env ← getEnv
  for (name, info) in env.constants.toList do
    if info.value?.any (·.hasSorry) then
      logError m!"{name} uses sorry"

大型项目的组织经验

一、按主题分模块，不按「工具/类型/证明」分。

✅ Group/Basic.lean, Group/Quotient.lean, Ring/Basic.lean
❌ Definitions.lean, Lemmas.lean, Theorems.lean

后者会导致所有文件互相依赖，编译无法并行。

二、控制 import 深度。 每个模块只 import 真正需要的。Mathlib 有工具检查冗余 import：

lake exe shake

三、公开 API 与内部实现分开。

private theorem helper : ... := ...      -- 只在本文件可见

theorem main_result : ... := by
  exact helper ...

四、写文档字符串。

/-- 计算树的节点数。 -/
def Tree.size : Tree α → Nat := ...

/-- ... -/ 会进入生成的文档，也会在编辑器悬停时显示。

五、把长证明拆开。 见结构化证明。

编译性能

形式化项目的编译时间是真实问题。几个手段：

手段	效果
`lake exe cache get`	Mathlib 不用自己编译
减少 `import Mathlib`	只 import 需要的模块
`simp only` 代替 `simp`	减少搜索
拆分大文件	提高并行度
避免过深的 `decide`	内核计算很慢
`set_option maxHeartbeats` 定位	找出慢的声明

查看哪些声明慢：

set_option profiler true in
theorem slow : ... := by ...

发布

发到 Reservoir：

仓库根有合法的 lakefile.toml（含 name、version）。
打 git tag。
Reservoir 会自动索引 GitHub 上的 Lean 包。

添加 README.md 与 LICENSE——与其他生态一样。

一个推荐的项目骨架

myproject/
├── lakefile.toml
├── lean-toolchain
├── lake-manifest.json      ← 提交进 git
├── README.md
├── Myproject.lean          ← 汇总 import
├── Myproject/
│   ├── Basic.lean
│   ├── Core/
│   │   ├── Defs.lean       定义
│   │   └── Lemmas.lean     基础引理
│   └── Advanced/
│       └── MainTheorem.lean
├── Test/
│   └── NoSorry.lean
└── .github/workflows/ci.yml

下一篇：实战例子。

本页目录