# 工程组织

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

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/lake-projects
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## lakefile

较新版本用 TOML：

```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 写）：

```lean
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 命令

```bash
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 # 单文件检查
```

<Callout type="warn">
  **`lake update` 要谨慎**——它会把依赖更新到最新，可能同时要求更换 Lean 版本，导致整个项目需要适配。

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

## 模块与命名空间

**文件路径 = 模块名**：

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

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

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

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

```lean
-- 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
```

<Callout type="info">
  **`Tree.size` 定义在 `Tree` 命名空间下，就能用点记法 `t.size`**——[广义字段记法](https://daiw.org/manual/lean4/functions)按类型名找函数。

  这是 Lean 的重要惯例：**给类型 `T` 的操作，定义成 `T.操作名`**。
</Callout>

## 重要的 lean options

```lean
set_option autoImplicit false
set_option relaxedAutoImplicit false
```

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

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

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

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

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

```toml
[leanOptions]
autoImplicit = false
relaxedAutoImplicit = false
```

关闭后必须显式声明：

```lean
universe u
variable {α : Type u}

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

其他常用选项：

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

## 依赖管理

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

或从 git：

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

**Reservoir** 是 Lean 的包索引（[reservoir.lean-lang.org](https://reservoir.lean-lang.org/)），用 `scope` + `name` 就能引用已发布的包。

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

## CI

GitHub Actions 的标准配置：

```yaml
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/
```

三个要点：

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

更严谨的 sorry 检查：

```lean
-- 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"
```

## 大型项目的组织经验

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

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

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

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

```bash
lake exe shake
```

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

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

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

**四、写文档字符串。**

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

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

**五、把长证明拆开。** 见[结构化证明](https://daiw.org/manual/lean4/structured-proofs)。

## 编译性能

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

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

查看哪些声明慢：

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

## 发布

发到 Reservoir：

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

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

## 一个推荐的项目骨架

```text
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
```

下一篇：[实战例子](https://daiw.org/manual/lean4/worked-example)。