深入 Lean 01：Lake 项目结构与依赖管理

Lake 是 Lean 4 的官方构建系统与包管理器，随 lean 工具链一同分发。形式化方法系列的第 07-08 篇已覆盖 elan 安装与 lake new 起手骨架；本篇从那个骨架向前推进，聚焦生产级项目需要的部分：toolchain 锁定、Mathlib4 依赖引入、lake-manifest.json 版本固定、多目标 lakefile 设计，以及可直接套用的 GitHub Actions CI 配置。

lean-toolchain：锁定工具链版本

项目根目录的 lean-toolchain 是一行纯文本文件，内容就是 toolchain 字符串：

leanprover/lean4:v4.12.0

elan 读取该文件，自动下载并激活对应版本的 lean 与 lake。项目目录内的所有 lake 命令都在该 toolchain 下执行，与机器全局版本无关。

版本字符串的两种合法格式：

格式	示例	说明
正式 release	leanprover/lean4:v4.12.0	推荐生产项目使用
nightly	leanprover/lean4:nightly-2025-01-15	追踪最新特性时使用，稳定性较低

Mathlib4 本身也带一个 lean-toolchain，声明它当前支持的 Lean 版本。引入 Mathlib 时，本项目的 lean-toolchain 必须与 Mathlib 的版本匹配，否则 lake build 会因 ABI 不兼容报错。确认方式：

# 查看 Mathlib 当前 lean-toolchain
curl -s https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain

lakefile.lean：项目定义 DSL

lakefile.lean 用 Lean 4 本身编写，Lake 提供一组 DSL 关键字。最小有意义的 lakefile：

import Lake
open Lake DSL

package «MyProject» where
  -- 包级配置（可选）

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

lean_lib «MyProject» where
  -- 库配置（可选）

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

• package «MyProject»：整个项目的顶层标识符，名称对应文件系统中的库目录。
• require mathlib from git ...：声明对 Mathlib4 的 Git 依赖；@ 后面是 tag 或 commit hash。
• lean_lib «MyProject»：声明一个 Lean 库目标，Lake 会按 MyProject/ 目录下的文件自动发现模块。
• lean_exe «myproject»：声明一个可执行目标，root 指向入口模块（Main.lean）。
• @[default_target]：标记默认构建目标，裸跑 lake build 时自动构建该目标。

多目标项目

一个 lakefile 可以包含多个库和可执行：

import Lake
open Lake DSL

package «MyProject» where

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

-- 核心库
lean_lib «MyProject» where

-- 工具库（可选，单独模块集合）
lean_lib «MyProjectUtils» where
  srcDir := "utils"

-- 主程序
@[default_target]
lean_exe «myproject» where
  root := `Main

-- 独立的验证脚本（不加 default_target，按需手动构建）
lean_exe «verify» where
  root := `Verify

lake build MyProject 只构建 MyProject 库；lake build 只构建带 @[default_target] 的目标。

目录结构：模块发现规则

Lake 的模块发现基于文件路径到模块名的直接映射：

MyProject/
  lakefile.lean          # 项目定义
  lean-toolchain         # toolchain 锁定
  lake-manifest.json     # 依赖锁文件（lake update 生成）
  Main.lean              # lean_exe 的入口模块
  MyProject.lean         # lean_lib 的根导入文件
  MyProject/
    Basic.lean           # 模块 MyProject.Basic
    Algebra/
      Group.lean         # 模块 MyProject.Algebra.Group
  utils/                 # 若 lean_lib 声明了 srcDir := "utils"
    Helper.lean          # 模块 MyProjectUtils.Helper
  .lake/
    build/               # 编译产物，不提交 git
    packages/            # 依赖包缓存

MyProject.lean 是库的根模块，通常只做集中 import：

-- MyProject.lean
import MyProject.Basic
import MyProject.Algebra.Group

其他项目 require 本项目时，import MyProject 会拉取这里列出的所有子模块。

lake-manifest.json：依赖锁文件

首次执行 lake update 后，Lake 生成 lake-manifest.json，记录所有依赖的精确 commit hash：

{
  "version": "0.1.2",
  "packagesDir": ".lake/packages",
  "packages": [
    {
      "type": "git",
      "name": "mathlib",
      "url": "https://github.com/leanprover-community/mathlib4.git",
      "rev": "v4.12.0",
      "inputRev": "v4.12.0"
    },
    {
      "type": "git",
      "name": "Qq",
      "url": "https://github.com/leanprover-community/quote4",
      "rev": "a0f8ade...",
      "inputRev": null
    }
  ]
}

rev 字段是 Git commit hash，而非浮动 tag。即使上游 v4.12.0 tag 被移动（这种情况罕见但存在），本项目重新 clone 后也会还原到完全相同的依赖快照。

lake-manifest.json 必须提交 git，语义与 yarn.lock / Cargo.lock 相同：它确保团队成员和 CI 得到完全一致的依赖树。

引入 Mathlib4：缓存优化

Mathlib4 包含约 16 万条定理，完整编译需要数小时。正确做法是下载预编译的 .olean 缓存：

# 1. 更新依赖，生成/更新 lake-manifest.json
lake update

# 2. 下载与当前 lean-toolchain + manifest commit 匹配的预编译缓存
lake exe cache get

# 3. 构建本项目（此时 Mathlib 模块直接读缓存，无需重编）
lake build

lake exe cache get 从 Mathlib 社区的 S3 存储桶拉取 .olean 文件，匹配规则是 lean-toolchain 版本 + Mathlib commit hash 的组合键。若缓存命中，整个 Mathlib 的"编译时间"降至几十秒（主要是网络传输）。

引入 Mathlib 后，可立即在 Lean 文件里验证：

-- MyProject/Basic.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

#check Nat.add_comm
-- Lean InfoView：Nat.add_comm : ∀ (n m : ℕ), n + m = m + n

example (n m : ℕ) : n + m = m + n := Nat.add_comm n m

#print axioms Nat.add_comm
-- Lean InfoView：'Nat.add_comm' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms 展示一个定理依赖的公理集合，是确认证明"真正封闭"的常用探针。Nat.add_comm 依赖 propext、Classical.choice、Quot.sound——这是 Lean 4 / Mathlib 的标准公理基，可接受。

将光标停在 example 内任意位置，InfoView 右栏显示当前目标：

⊢ n + m = m + n

exact Nat.add_comm n m 消解后 InfoView 显示 No goals，证明完成。

核心 Lake 命令

lake new MyProject          # 新建项目骨架（在新目录里）
lake init MyProject         # 在当前目录初始化项目

lake build                  # 构建 default_target
lake build MyProject        # 构建指定目标
lake build MyProject.Basic  # 构建单个模块

lake clean                  # 删除 .lake/build/（保留下载的依赖包）
lake clean -rfl             # 彻底清除，包括 .lake/packages/

lake update                 # 解析 lakefile 依赖，更新 lake-manifest.json
lake update mathlib         # 仅更新指定包

lake exe cache get          # 下载 Mathlib 预编译 olean
lake exe cache put          # （Mathlib 维护者用）上传缓存

lake run myproject          # 运行 lean_exe 目标
lake env lean --run Main.lean   # 在 lake 环境下执行单文件

lake clean 与 lake clean -rfl 的区别：前者只删构建产物，依赖包缓存保留（下次 build 不需重新下载）；后者全部清除，适合排查缓存污染问题。

GitHub Actions CI 配置

# .github/workflows/ci.yml
name: CI

on:
  push:
    branches: [main]
  pull_request:
    branches: [main]

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

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
            -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Set toolchain from lean-toolchain
        run: elan toolchain install "$(cat lean-toolchain)"

      - name: Cache Lake packages
        uses: actions/cache@v4
        with:
          path: .lake/packages
          key: lake-${{ hashFiles('lake-manifest.json') }}
          restore-keys: lake-

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

      - name: Build
        run: lake build

• --default-toolchain none 防止 elan 在 CI 里装一份多余的默认 toolchain；实际版本由 lean-toolchain 文件驱动。
• actions/cache 的 key 绑定 lake-manifest.json 的 hash，确保依赖锁变更时缓存自动失效。
• lake exe cache get 在本地构建目录不含 Mathlib olean 时下载预编译版本，与本地工作流一致。

若项目不依赖 Mathlib，删去 lake exe cache get 一行即可，CI 时间通常在 1-3 分钟内。

汇总

文件 / 命令	职责
lean-toolchain	锁定 Lean + Lake 版本，elan 自动读取
lakefile.lean	声明包、依赖、库、可执行
lake-manifest.json	依赖 commit hash 快照，必须提交 git
lake update	解析依赖，更新 manifest
lake exe cache get	下载 Mathlib 预编译缓存，避免本地重编
lake build	构建 default_target
lake clean	删除构建产物，保留依赖包
CI actions/cache	用 manifest hash 做 key，跨 CI 复用依赖包

给读者的练习

1. 从零创建一个 ProofSandbox 项目，lean-toolchain 锁定到 leanprover/lean4:v4.12.0，在 lakefile 里 require mathlib，执行 lake update 与 lake exe cache get，最后 lake build 零错误。记录整个过程的耗时，对比有无 lake exe cache get 的差异。

2. 在已引入 Mathlib 的项目里，新建 MyProject/Explore.lean，写下面两行并观察 InfoView 输出：

   #check @List.map
   #print axioms List.length_map

   解释 List.length_map 的公理依赖与 Nat.add_comm 相比多了什么（如果有的话）。

3. 修改 lakefile，在同一个项目里同时声明 lean_lib «MyProject» 和一个不带 @[default_target] 的 lean_exe «verify»（入口为 Verify.lean，内容只写 #eval "verify ok"）。确认 lake build 只构建库，lake build verify 构建可执行并打印 "verify ok"。

参考资料

• Lake 文档：https://github.com/leanprover/lake
• Mathlib4 贡献指南：https://leanprover-community.github.io/contribute/index.html
• Mathlib4 文档：https://leanprover-community.github.io/mathlib4_docs/
• Theorem Proving in Lean 4：https://leanprover.github.io/theorem_proving_in_lean4/
• elan GitHub：https://github.com/leanprover/elan
• 本系列前置篇：形式化方法 07-08——准备 Lean 4 实验环境、在 Lean 4 中证明经典命题