Lean 安装与环境配置

Some content in this article was created with AI assistance. Please verify as needed.

Lean 是一个函数式编程语言和定理证明器，它的版本管理和环境配置可以分成两部分来看：

elan：负责 Lean 版本管理
lake：负责 Lean 项目构建和包管理

这套工具链的设计和 Rust 的 rustup + cargo 以及 Julia 的 juliaup + Pkg 非常相似，可以说是现代编程语言工具链的标配方案。

Lean 官网的安装教程为什么那么喜欢把 Lean 的安装和微软自家的 VSCode 生态绑定？

虽然 VSCode 的 Lean 插件提供的辅助操作很方便，但是显然手动安装才是 best practice，用户能知道这里到底发生了什么，即使是基于 Lean 插件的安装教程也不过是把 Lean 的安装放在了 VSCode 中执行。

除了官网教程，还可以参考 Lean Prover 中文文档。

Lean 工具链介绍

Lean 官方工具链（toolchain）包含程序开发所需的主要组件：

lean 可执行文件（编译器及 elaboration 前端）
随工具链提供的 Lean 库，包括 Init、Std 和 Lean
Lake 构建工具
leanc（bundled C 编译器，用于原生编译）
标准库源码、头文件及预编译 .olean 文件

狭义上的 Lean 运行时（runtime）指的是垃圾回收、对象表示、任务调度和 IO 支持等供生成程序执行的底层系统，它是工具链的一部分。

第三方包不属于工具链自带内容，它们存放在项目的 .lake/packages/ 目录中（项目依赖的本地工作副本），由 lake 按项目隔离管理。

elan 管理的 Lean 安装目录大致如下：

# Linux
~/.elan/
├── bin/
│   ├── elan
│   ├── lake
│   ├── lean
│   ├── leanc
│   ├── leanchecker
│   ├── leanmake
│   └── leanpkg
│
├── toolchains/
│   └── leanprover--lean4---v4.18.0/
│       ├── bin/
│       ├── include/
│       ├── lib/
│       ├── share/
│       └── src/
│
└── settings.toml

在 Windows 中，安装位置为 %USERPROFILE%\.elan\，内部结构相同。

说明：

目录	作用
`bin/`	`lean`、`lake` 等代理程序
`toolchains/`	各个版本的 Lean 工具链（真实二进制）
`lib/lean/`	Lean 核心库和标准库源码
`settings.toml`	elan 配置文件

elan 版本管理

elan 是一个版本管理器和启动器，可以理解为：

1	elan = Lean 版本下载 + 多版本切换 + 默认版本控制

~/.elan/bin 中的 lean、lake 等是 elan 提供的代理程序（proxy）。代理程序根据当前目录中的 lean-toolchain、目录 override 和默认工具链，调用 ~/.elan/toolchains/ 中对应版本的真实程序。

设计思路借鉴了 rustup 以及 juliaup。

安装与卸载

Linux：

1	curl https://elan.lean-lang.org/elan-init.sh -sSf \| sh

安装过程中 elan 会询问是否将 ~/.elan/bin 加入 PATH，选择 yes 即可。

Windows（PowerShell）：

1
2
3

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

安装完成后需要将 %USERPROFILE%\.elan\bin 添加到系统 PATH 环境变量中（安装脚本通常会询问是否自动添加）。

也可以从 GitHub Releases 手动下载安装包。

安装完成后，可以使用以下命令验证：

1
2
3

elan --version
lean --version
lake --version

如果不再需要 Lean，可以通过以下方式完全卸载。

elan 提供了卸载命令：

1	elan self uninstall

这个命令会自动清理 PATH 配置并删除整个 ~/.elan（或 %USERPROFILE%\.elan）目录。

也可以手动进行：

# Linux
rm -rf ~/.elan
# 然后编辑 ~/.bashrc / ~/.zshrc，删除 ~/.elan/bin 的 PATH 行

# Windows（PowerShell）
Remove-Item -Recurse -Force $env:USERPROFILE\.elan
# 然后在系统环境变量中移除 %USERPROFILE%\.elan\bin

基本使用

elan 使用工具链（toolchain）概念管理不同版本的 Lean：

stable：当前稳定版
nightly：每日构建版（包含最新改动）
v4.18.0：指定版本号

查看当前默认生效的工具链及相关信息：

elan show

输出例如

1 2	leanprover/lean4:v4.32.0 (resolved from default 'stable') Lean (version 4.32.0, x86_64-unknown-linux-gnu, commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35, Release)

查看已安装的工具链：

1	elan toolchain list

输出例如

1	leanprover/lean4:v4.32.0

安装指定版本：

1 2	elan toolchain install leanprover/lean4:stable elan toolchain install leanprover/lean4:v4.18.0

设置默认工具链：

1 2	elan default stable elan default leanprover/lean4:v4.18.0

更新工具链：

1	elan update

卸载某个工具链：

1	elan toolchain uninstall leanprover/lean4:v4.17.0

elan 自身的更新

1	elan self update

版本设置

在项目根目录创建文本文件 lean-toolchain，内容为版本标识，例如

1	leanprover/lean4:v4.18.0

进入该目录后，elan 会自动使用对应版本的 lean。如果该版本尚未安装，elan 会自动下载并安装相应工具链。

这个机制类似 Python 的 .python-version 或 Rust 的 rust-toolchain.toml。

elan 对版本的具体选择规则实际更复杂，支持从当前目录开始逐级向父目录查找 lean-toolchain，还支持对目录 override 版本设置，具体内容过于细节，这里略去。

Lean 基本使用

Lean 没有传统意义的独立 REPL。
#eval、#check、#print 等是 Lean 源文件中的顶层命令，可以在 .lean 文件中使用，用于在处理源文件时输出信息到控制台。

常用顶层命令：

命令	作用
`#eval <expr>`	求值表达式
`#check <expr>`	查看表达式类型
`#print <name>`	打印定义

例如在 test.lean 中写入（-- 开头代表注释）

#eval 1 + 1
-- 2

#eval String.append "Hello, " "World!"
-- "Hello, World!"

#eval List.range 10
-- [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

使用 lean 命令运行

1	lean test.lean

输出

1
2
3

2
"Hello, World!"
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

Lean 文件中还可以包括 main 函数，例如创建 hello.lean 并写入如下内容

def main : IO Unit :=
  IO.println "Hello, Lean!"

#eval 1 + 2 - 3

使用 lean 命令加上 --run 选项运行

1	lean --run hello.lean

输出

1 2	7 Hello, Lean!

lean 只会处理源文件，包括检查类型，输出 #eval 等顶层命令的内容。

lean 加上 --run 选项会在处理源文件之后，调用其中的 main。
因此 #eval 等顶层命令的输出顺序在 main 执行之前。

lake 项目管理和包依赖

lake（Lean Make）是 Lean 的构建工具和包管理器，功能上接近 Rust 的 cargo 或 Julia 的 Pkg：

1	lake = 项目初始化 + 构建管理 + 包依赖管理

每个 lake 项目围绕一个 lakefile.toml（或 lakefile.lean）组织。

创建新项目

lake 提供两个命令来初始化项目：

lake new <name> — 创建新目录并在其中初始化项目
lake init <name> — 在当前目录中初始化项目

创建新项目通常使用 lake new：

1	lake new MyProject

执行后生成以下结构：

MyProject/
├── .git/
├── .github/
├── MyProject/
│   └── Basic.lean
├── .gitignore
├── MyProject.lean
├── lakefile.toml
├── lean-toolchain
├── Main.lean
└── README.md

说明：

路径	作用
`lakefile.toml`	项目配置
`lake-manifest.json`	依赖锁定文件（首次 `lake build` / `lake update` 后生成）
`lean-toolchain`	指定 Lean 版本
`Main.lean`	主入口文件
`MyProject/`	包源码目录
`MyProject/Basic.lean`	示例模块

lakefile.toml 的一个简单示例（标准模板生成的配置大致如下）：

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

[[lean_lib]]
name = "MyProject"

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

如果更喜欢 Lean DSL 格式，可以手动改为 lakefile.lean：

import Lake
open Lake.DSL

package MyProject where
  -- 包元信息

lean_lib MyProject where
  -- 构建目标：库

@[default_target]
lean_exe myproject where
  root := `Main
  -- 构建目标：可执行文件

两种格式都可以表达常见的声明式项目配置。lakefile.lean 还允许使用 Lean 代码编写动态配置、自定义脚本和构建逻辑，因此比 lakefile.toml 更灵活；一般项目使用 TOML 即可。Lean 中，如果标识符包含连字符等特殊字符（例如包名 my-project），需要用 guillemet 引号 «» 包裹：«my-project»。如果包名是单个纯字母单词（如 MyProject、demo），则可以省略。本文示例均使用不含特殊字符的包名，因此不出现 «»。

构建和运行

在项目目录中：

# 构建项目
lake build

# 构建并运行可执行文件
lake exe myproject
# 输出 Hello, World!

清理构建产物：

1	lake clean

更新依赖：

1	lake update

添加依赖

下面是一个添加依赖的 demo 项目示例。

先在项目根目录初始化：

1 2	mkdir demo-project && cd demo-project lake init demo

编辑 lakefile.toml 以添加依赖（以 batteries 为例——Lean 的社区扩展库，提供更丰富的列表、字符串等操作）：

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

[[require]]
name = "batteries"
scope = "leanprover-community"
rev = "main"

[[lean_lib]]
name = "Demo"

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

lean init 会提供一个基础模板，只需要修改 [[require]] 部分添加依赖。

注意：Lean 工具链已自带 Std 标准库，import Std 即可使用，无需在 lakefile.toml 中添加依赖。batteries 是独立的社区扩展库（由原 std4 仓库迁移而来）。

更新依赖后下载并解析依赖

1	lake update

大致会执行以下操作：

从指定 Git 仓库下载依赖
将远程依赖的源码工作副本检出到 .lake/packages/ 目录
生成/更新 lake-manifest.json（锁定依赖的精确 commit）

lake-manifest.json 的内容大致如下（实际字段因 Lake 版本而异）：

{
  "version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages": [
    {
      "url": "https://github.com/leanprover-community/batteries",
      "type": "git",
      "subDir": null,
      "rev": "a1b2c3d4e5f6...",
      "name": "batteries",
      "manifestFile": "lake-manifest.json",
      "inputRev": "main"
    }
  ],
  "name": "demo",
  "lakeDir": ".lake",
  "fixedToolchain": false
}

这个文件相当于 Python 的 uv.lock 或 Rust 的 Cargo.lock，应该纳入版本管理。

然后构建项目即可

1	lake build

项目结构

一个实际使用依赖的项目结构大致如下

demo/
├── .lake/               -- Lake 工作目录，包含依赖源码副本和构建产物（不应提交到 git）
├── Demo/
│   └── Basic.lean      -- 库模块
├── Demo.lean            -- 库入口
├── Main.lean            -- 可执行文件入口
├── lakefile.toml
├── lake-manifest.json
└── lean-toolchain

在 Main.lean 中可以导入自己的库模块和外部依赖：

import Demo.Basic      -- 导入项目的库模块
import Batteries       -- 导入外部依赖

def main : IO Unit := do
  IO.println "Starting demo..."
  -- 使用 Batteries 或其他依赖的功能

编译并运行：

1 2	lake build lake exe demo

注意：

远程依赖的源码工作副本存放在项目的 .lake/packages/ 中，构建产物位于 .lake/build/ 中。
不同项目通常具有各自独立的依赖副本，与 Python 的虚拟环境（每个环境独立拷贝）和 Julia 的 depot（全局共享 ~/.julia）都不同。

mathlib

mathlib4 是 Lean 的数学库，类似 Coq 的 MathComp 或 Isabelle 的 AFP。它是 Lean 定理证明的核心生态组件。

目前绝大多数的数学形式化证明工作都需要依赖 mathlib，因此都需要使用项目模式而非简单的脚本模式运行。

创建 mathlib 项目

使用 mathlib 指定的工具链创建项目：

1 2	lake +leanprover-community/mathlib4:lean-toolchain new MyMathProject math cd MyMathProject

math 模板会生成已经配置好 mathlib 依赖的项目，并设置与该 mathlib 版本匹配的 lean-toolchain。初始化过程还会解析并下载依赖，生成 lake-manifest.json，并通过 mathlib 的更新钩子自动获取预编译构建产物。

因此，项目创建完成后通常可以直接构建：

1	lake build

mathlib 及其上游依赖的预编译产物已经在初始化阶段下载，lake build 通常只需构建当前项目自身的文件。

如果自动缓存下载被跳过、失败，或者需要重新下载缓存，可以手动执行：

1	lake exe cache get

也可以在现有项目的 lakefile.toml 中添加 mathlib 依赖

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "<compatible revision>"

为避免版本不匹配，尤其是在使用旧版 Lake 或固定 mathlib revision 时，推荐先将项目的 lean-toolchain 设置为该 mathlib revision 所要求的版本。

使用 mathlib 编写证明

使用 mathlib 编写证明的基本流程：

导入 mathlib——在文件顶部 import Mathlib（或按需导入具体模块）
写定义——定义函数、定理、引理
写证明——使用 by 块和 tactic 组合完成证明
构建检查——lake build 验证编译通过

示例如下：（MyMathProject/Basic.lean）

/-
Copyright (c) 2024 MyMathProject Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: MyMathProject Authors
-/
import Mathlib

/-!
Basic Lean examples and proofs.
-/

-- Prove 1 + 1 = 2
example : 1 + 1 = 2 := by
  rfl

-- Use a theorem from mathlib
example (a b : Nat) : a + b = b + a := by
  rw [add_comm]

-- A slightly more complex example
example (a b c : Nat) : (a + b) + c = a + (b + c) := by
  rw [add_assoc]

-- Define factorial
def factorial : Nat -> Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

-- Evaluate
#eval factorial 5   -- 120

-- Proposition and proof
theorem factorial_pos (n : Nat) : factorial n > 0 := by
  induction n with
  | zero =>
    simp [factorial]
  | succ k ih =>
    rw [factorial]
    exact Nat.mul_pos (by omega) ih

def hello := "world"

编译

1	lake build

构建通过表示文件已成功 elaboration，且所有已提供的证明项均通过内核检查。这不保证项目中不存在 sorry（默认仅产生警告）、未审查公理或以警告形式报告的问题。如需将警告视为错误，可使用 lake build --wfail。

Lean 编译模型

Lean 对源文件的处理包含两条相互关联但用途不同的路径：

将源文件转换为可供其他 Lean 模块导入、内核检查和编辑器分析的模块信息；
将其中需要在运行时执行的定义编译为原生代码。

这两条路径都以 Lean 的前端处理为基础，但最终生成的产物不同。

Lean 前端与模块产物

一个 .lean 源文件首先经过：

解析
  ↓
宏展开
  ↓
elaboration
  ↓
内核检查

其中，elaboration 会完成名称解析、隐式参数补全、类型推断、类型类合成、语法糖展开和证明项构造等工作；随后由 Lean 内核检查生成的声明和证明项是否满足类型规则。

处理结果可以保存为以下模块产物：

.olean：序列化后的 Lean 模块环境，供其他模块通过 import 导入；
.ilean：源代码引用和位置信息，主要供语言服务器、跳转定义和编辑器分析使用；
.c：Lean 后端生成的 C 源代码，用于后续原生编译。

其中，.olean 不是 C/C++ 中的 .o 目标文件。它保存的是经过 elaboration 和内核检查后的定义、类型、定理、实例以及其他环境信息，更接近编译器模块文件，而不是机器码文件。

原生代码生成

对于需要在运行时执行的定义，Lean 编译器会将其转换为内部中间表示，再由默认的 C 后端生成 C 代码。

生成的 C 代码由 Lean 工具链自带的 leanc 编译为原生目标文件。leanc 是对工具链内置 Clang 编译器的封装。目标文件随后可以根据构建目标：

归档为静态库；
链接为动态库；
链接为原生可执行文件。

整体流程可以概括为：

.lean 源文件
   │
   ▼
解析、宏展开、elaboration、kernel checking
   │
   ├──→ .olean    Lean 模块环境，供其他模块导入
   │
   ├──→ .ilean    源代码索引，供语言服务器使用
   │
   └──→ Lean IR
           │
           ▼
         C 代码（.c）
           │
           ▼
         leanc
           │
           ▼
      目标文件（.o）
           │
     ┌─────┼──────────┐
     ▼     ▼          ▼
  静态库  动态库    可执行文件
   .a   .so/.dll

因此，从 C/C++ 编译模型的角度，Lean 的原生代码路径可以粗略类比为：

1	Lean IR → .c → .o → library / executable

但 Lean 还具有一条没有直接对应于普通 C++ 目标文件的模块路径：

1	.lean → .olean

.olean 是 Lean 模块系统和定理检查过程中的核心产物，而 .o 才是包含原生机器码的目标文件。

通常情况下，Lean 项目不需要额外安装系统级的 GCC 或 Clang，因为官方工具链已经提供 leanc。只有在调用外部 C/C++ 库、编写 FFI、使用特殊平台或自定义原生构建流程时，才可能需要额外的系统编译环境。

使用 `lean` 处理单个文件

对于单个 .lean 文件，可以直接调用 lean。

假设 hello.lean 的内容为：

def main : IO Unit :=
  IO.println "Hello, Lean!"

#eval 1 + 2 - 3

直接执行：

1	lean hello.lean

会完成解析、elaboration 和内核检查，并执行 #eval 等顶层命令。未指定输出选项时，不会将 .olean、.ilean 或 .c 文件保存到磁盘。

常见命令如下：

# 处理源文件，并执行 #eval、#check 等顶层命令
lean hello.lean

# 处理源文件，并将运行时代码生成到指定的 C 文件
lean -c hello.c hello.lean

# 处理源文件并执行其中的 main
# 不在磁盘上生成独立的原生可执行文件
lean --run hello.lean

执行：

1	lean --run hello.lean

会先在处理源文件时执行 #eval，然后执行 main，因此输出为：

1 2	7 Hello, Lean!

需要注意，lean hello.lean 不只是传统意义上的类型检查。它还会执行宏展开、名称解析、类型推断、类型类合成、证明项构造和内核检查等 Lean 前端过程。

Lake 项目中的构建目标

对于包含多个模块和外部依赖的项目，通常由 Lake 组织模块处理、代码生成、原生编译和链接过程。

执行：

1	lake build

时，Lake 会根据命令中显式指定的目标，或者项目配置中的默认目标，增量构建相应产物。

不同类型的目标具有不同作用：

Lean 模块会生成 .olean、.ilean 和 C 代码等模块产物；
需要原生代码时，Lake 会调用 leanc 将 C 代码编译为 .o 目标文件；
lean_lib 定义 Lean 库目标，并可进一步构建相应的原生库产物；
lean_exe 定义原生可执行目标，最终链接所需目标文件和库，生成独立的可执行文件。

Lake 会记录构建输入及其依赖关系。源文件、依赖和配置没有变化时，已经是最新状态的目标不会被重新编译。

假设 lakefile.toml 中定义了：

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

[[lean_lib]]
name = "MyProject"

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

其中 Main.lean 包含：

1 2	def main : IO Unit := IO.println "Hello, Lean!"

可以显式构建可执行目标：

1	lake build myproject

生成的原生可执行文件通常位于：

1	.lake/build/bin/myproject

在 Windows 上通常为：

1	.lake/build/bin/myproject.exe

由于 myproject 已经列在：

1	defaultTargets = ["myproject"]

中，因此直接执行：

1	lake build

也会构建该可执行目标。

如果 defaultTargets 指定的是库目标，则裸命令 lake build 只构建相应的默认目标，不一定生成项目中的所有可执行文件。

使用 `lake exe` 构建并运行程序

Lake 提供：

1	lake exe <target> [arguments...]

用于运行项目中定义的 lean_exe 目标。例如：

1	lake exe myproject

其行为可以分为以下步骤：

在当前 Lake workspace 中查找名为 myproject 的可执行目标；
检查该目标及其依赖是否已经构建并处于最新状态；
如果目标缺失或已经过期，则增量构建该目标；
在 Lake 配置的运行环境中执行生成的原生二进制文件。

因此，概念上：

1	lake exe myproject

近似等价于：

1 2	lake build myproject .lake/build/bin/myproject

但二者并不完全相同。lake exe 会设置 Lake workspace 对应的环境变量、动态库搜索路径和其他运行环境，使程序能够正确使用工具链及依赖包中的原生库。

直接运行：

1	.lake/build/bin/myproject

则不会自动配置这些 Lake 环境变量。对于不依赖额外动态库的简单程序，两种运行方式可能表现相同；对于具有原生依赖的项目，通常应使用 lake exe。

程序参数可以写在可执行目标名称之后：

1	lake exe myproject input.txt 100

这些参数会传递给 Lean 程序。相应的入口函数可以定义为：

1
2
3

def main (args : List String) : IO UInt32 := do
  IO.println s!"arguments: {args}"
  return 0

lake exe 显式指定可执行目标，因此不要求该目标出现在 defaultTargets 中。相比之下：

1	lake build

在未指定目标时，只构建项目配置中的默认目标。

例如，mathlib 中的：

1	lake exe cache get

应理解为：

查找名为 cache 的可执行目标；
在需要时构建该目标；
运行生成的 cache 程序；
将 get 作为命令行参数传递给它。

因此，cache get 不是 Lake 内置的两级子命令。cache 是 mathlib 定义的可执行程序，get 是传递给该程序的参数。

`lean --run` 与 `lake exe` 的区别

lean --run 和 lake exe 都可以执行带有 main 的 Lean 程序，但二者的用途和执行路径不同。

命令	使用 Lake 项目配置	生成独立原生可执行文件	行为
`lean --run Main.lean`	否	否	直接处理源文件并执行 `main`
`lake build myproject`	是	是	构建 `lean_exe` 目标，但不运行
`lake exe myproject`	是	是	按需构建并运行原生可执行文件
`.lake/build/bin/myproject`	否	已经生成	直接运行已有二进制文件

因此，对于临时的单文件程序，可以使用：

1	lean --run Main.lean

对于包含多个模块、外部依赖和正式构建配置的项目，通常使用：

1	lake exe myproject

后者执行的是经过 Lean C 后端、leanc 编译和原生链接后得到的可执行文件，而不是直接处理 Lean 源文件。

Lake 构建目录

Lake 的构建产物默认存放在：

1	.lake/build/

其结构大致如下：

.lake/build/
├── ir/       # Lean 后端生成的 C 等中间代码
├── lib/      # .olean、.ilean、目标文件和库文件等
└── bin/      # lean_exe 生成的原生可执行文件

对于前面的 myproject 目标，整体构建和运行过程可以概括为：

Main.lean
   │
   ▼
解析、elaboration 与 kernel checking
   │
   ├──→ Main.olean
   ├──→ Main.ilean
   │
   └──→ Lean IR
           │
           ▼
         Main.c
           │
           ▼
         Main.o
           │
           ▼
  .lake/build/bin/myproject
           │
           ├──→ lake exe myproject
           │       在 Lake 环境中运行
           │
           └──→ 直接执行二进制文件
                   不自动配置 Lake 运行环境

Lean 工具链介绍

elan 版本管理

安装与卸载

基本使用

版本设置

Lean 基本使用

lake 项目管理和包依赖

创建新项目

构建和运行

添加依赖

项目结构

mathlib

创建 mathlib 项目

使用 mathlib 编写证明

Lean 编译模型

Lean 前端与模块产物

原生代码生成

使用 lean 处理单个文件

Lake 项目中的构建目标

使用 lake exe 构建并运行程序

lean --run 与 lake exe 的区别

Lake 构建目录

使用 `lean` 处理单个文件

使用 `lake exe` 构建并运行程序

`lean --run` 与 `lake exe` 的区别