LeanDojo | 为 Lean 定理证明器搭建桥梁

发表于 更新于 分类于 阅读次数： 字数： 1.2k 时间 ≈ 5 分钟
Lean 定理证明器的 Python 交互库，支持 Lean 3 和 Lean 4。

简介

LeanDojo 是一个为 Lean 定理证明器设计的 Python 库，支持 Lean 3 和 Lean 4 版本。其主要提供以下两大功能：

  • 数据提取：从 Lean 存储库中提取证明状态、策略、前提等关键信息。
  • 环境交互：允许用户以编程方式与 Lean 环境进行交互。

LeanDojo 功能图示

LeanDojo 在解析 Lean 文件及与环境交互方面有很高的实用性。但项目只支持处理 GitHub 上的仓库，且这一问题一直没有修复。

最近给 LeanDojo 提交了一个更新 PR，增加对本地及非 GitHub 仓库的支持，借此机会写个简易教程。

项目浅析

LeanDojo 按照 仓库=>文件=>定理 的结构来解析文件，操作围绕 LeanGitRepo 类来进行：

LeanGitRepo 类操作示意图

该类基于 PyGithub 实现，因此频繁调用 GitHub API。

当前处理这个问题的 PR ：Add Support for Local and Remote Repositories #179。使用 gitpython 作为补充，并对一些函数方法进行了重写。

相关链接

基本示例

准备工作

安装依赖，测试用 Python 3.10 版本：

1
pip install lean-dojo

使用官方示例仓库：yangky11/lean4-example。这是一个简洁的 Lean 包，文件结构如下：

1
2
3
4
5
6
7
lean4-example/
├── lakefile.lean
├── lake-manifest.json
├── Lean4Example.lean
├── lean-toolchain
├── LICENSE
└── README.md

其中，Lean4Example.lean 文件的内容：

1
2
3
4
5
6
7
open Nat (add_assoc add_comm)

theorem hello_world (a b c : Nat)
  : a + b + c = a + c + b := by
  rw [add_assoc, add_comm b, ←add_assoc]

theorem foo (a : Nat) : a + 1 = Nat.succ a := by rfl

从 Nat 命名空间导入了 add_assoc 和 add_comm 两个引理，然后定义了两个定理。

设置环境变量

环境变量只在首次 import lean_dojo 时生效，因此先设置：

1
2
3
4
5
6
7
8
9
10
import os

# 设置 GitHub token 以避免请求频率限制
os.environ['GITHUB_ACCESS_TOKEN'] = 'gho_xxx'
# 配置线程数以加快 `trace` 的运行速度
os.environ['NUM_PROCS'] = '64'
# 设置临时目录以便观察 `trace` 阶段生成的文件
os.environ['TMP_DIR'] = 'temp_dir'
# 取消远程缓存下载，在本地进行构建
os.environ['DISABLE_REMOTE_CACHE'] = 'true'

仓库对象

环境交互和数据提取都是围绕 LeanGitRepo 对象展开的。

首先导入 LeanGitRepo 类

1
from lean_dojo import LeanGitRepo

初始化仓库对象，可使用 commit hash 或 main 分支：

1
repo = LeanGitRepo("https://github.com/PatrickMassot/GlimpseOfLean", "8d73d32d90ec2315616ad8e720754eeacfb96af6")

查看仓库对象的基本属性：

1
2
3
4
5
print("repo.url", repo.url)
print("repo.commit", repo.commit)
print("repo.repo", repo.repo)
print("repo.lean_version", repo.lean_version)
print(repo.get_config("lean-toolchain"))

输出结果：

1
2
3
4
5
repo.url https://github.com/PatrickMassot/GlimpseOfLean
repo.commit 8d73d32d90ec2315616ad8e720754eeacfb96af6
repo.repo Repository(full_name="PatrickMassot/GlimpseOfLean")
repo.lean_version 873ef2d894af80d8fc672e35f7e28bae314a1f6f
{'content': 'leanprover/lean4:v4.8.0-rc2\n'}

这里 lean_version 是一个 commit hash，而不是直观的版本字符串。

Trace 操作

对仓库进行 trace 操作：

1
2
3
4
from lean_dojo import trace

repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "04e29174a45eefaccb49b835a372aa762321194e")
trace(repo, dst_dir="traced_lean4-example")

trace 主要执行以下步骤：

  1. 克隆仓库到 TMP_DIR 目录，并执行 lake build 进行构建。
  2. 获取仓库的 Lean4 版本，将对应版本的 Lean4 文件复制到 .lake/packages 目录。
  3. 数据提取：将 ExtractData.lean 脚本拷贝到仓库，执行 lake env lean --run ExtractData.lean 命令，提取 AST 树、状态和定理等信息，随后删除 ExtractData.lean 文件。
  4. 环境交互：将 Lean4Repl.lean 脚本拷贝到仓库，并更新 lakefile 以包含依赖信息，执行 lake build Lean4Repl 命令进行构建。
  5. 获取仓库信息，并更新 .cache/leandojo 目录下的缓存。

此外，ExtractData.lean 和 Lean4Repl.lean 文件是整个项目的核心。如果只关心环境交互问题，可以重点关注 Lean4Repl.lean 文件。

数据提取

提取的文件位于 .lake/build 目录：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
.lake
├── build
│   ├── ir
│   │   ├── Lean4Example.ast.json
│   │   ├── Lean4Example.c
│   │   ├── Lean4Example.c.hash
│   │   ├── Lean4Example.dep_paths
│   │   └── Lean4Example.trace.xml
│   └── lib
│       ├── Lean4Example.ilean
│       ├── Lean4Example.ilean.hash
│       ├── Lean4Example.olean
│       ├── Lean4Example.olean.hash
│       └── Lean4Example.trace
├── lakefile.olean
├── lakefile.olean.trace
└── packages
    └── lean4
        ├── bin
        ├── include
        ├── lib
        ├── LICENSE
        ├── LICENSES
        ├── share
        └── src

这里有两类比较重要的文件：

  • .ast.json：包含带有语义信息的注释，例如策略状态和名称。
  • .trace.xml：结构化处理后的句法和语义信息。

项目按 仓库 => 文件 => 定理 的层次结构生成文件。示例中的例子比较简单，仅包含一个文件。

环境交互

示例仓库中包含两个定理。以下以 hello_world 定理为例，展示如何使用 Dojo 类进行环境交互。

1
2
3
theorem hello_world (a b c : Nat)
  : a + b + c = a + c + b := by
  rw [add_assoc, add_comm b, ←add_assoc]

首先导入 Dojo 类和 Theorem 类：

1
from lean_dojo import Theorem, Dojo

获取定理对象，从 Lean4Example.lean 文件中提取 hello_world 定理：

1
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")

获取初始状态：

1
2
3
4
5
6
dojo, state_0 = Dojo(theorem).__enter__()
print(state_0)
# TacticState(pp='a b c : Nat\n⊢ a + b + c = a + c + b', id=0, message=None)
print(state_0.pp)
# a b c : Nat
# ⊢ a + b + c = a + c + b

对初始状态 state_0 执行策略，并获取更新后的状态：

1
2
3
4
state_1 = dojo.run_tac(state_0, "rw [add_assoc]")
print(state_1.pp)
# a b c : Nat
# ⊢ a + (b + c) = a + c + b

继续对状态 state_1 执行策略，并获取最终状态：

1
2
3
4
print(dojo.run_tac(state_1, "sorry"))
# ProofGivenUp()
dojo.run_tac(state_1, "rw [add_comm b, ←add_assoc]")
# ProofFinished(tactic_state_id=4, message='')

小结

以上，我们演示了用 LeanDojo 进行数据提取和环境交互。

如果对 LeanDojo 的关键实现细节感兴趣，可以进一步阅读两个核心文件：