Lean命令行界面[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean命令行界面（CLI）是Lean定理证明器的核心交互工具，允许用户通过终端直接执行Lean代码、管理项目依赖、编译文件以及调用自动化证明工具。CLI为开发者提供了不依赖图形界面的高效工作流，尤其适合集成到自动化构建系统或持续集成（CI）环境中。

Lean CLI的主要功能包括：

初始化和管理Lean项目
编译和检查代码语法
运行测试和验证证明
安装和管理第三方工具链（如`mathlib`）

安装与配置[编辑 | 编辑源代码]

基础安装[编辑 | 编辑源代码]

通过[Elan](https://github.com/leanprover/elan)（Lean版本管理器）安装CLI工具链：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

验证安装：

lean --version
# 输出示例：Lean (version 4.2.0)

项目结构[编辑 | 编辑源代码]

典型的Lean项目目录结构如下：

关键文件说明：

`Lean.toml`：项目配置文件
`Lakefile.lean`：构建脚本（类似Makefile）
`build/`：编译输出目录

核心命令[编辑 | 编辑源代码]

项目初始化[编辑 | 编辑源代码]

创建新项目：

lake new my_project

编译与运行[编辑 | 编辑源代码]

编译单个文件：

lean Main.lean

使用Lake构建系统（推荐）：

lake build

交互模式[编辑 | 编辑源代码]

启动交互式REPL环境：

lean --repl

示例会话：

# 输入：
#eval 1 + 1
# 输出：
2

高级用法[编辑 | 编辑源代码]

定理证明辅助[编辑 | 编辑源代码]

调用自动化证明器：

lean --run Proof.lean

文件内容示例：

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a
  · simp
  · simp [*]

性能分析[编辑 | 编辑源代码]

生成时间统计报告：

lean --profile Main.lean

输出示例：

Processing time: 1.23s
Memory usage: 45MB

实际案例[编辑 | 编辑源代码]

数学库开发[编辑 | 编辑源代码]

1. 初始化项目：

   lake init math_lib

2. 添加`mathlib`依赖：

  修改`Lakefile.lean`：

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

3. 构建项目：

   lake update
   lake build

CI集成示例[编辑 | 编辑源代码]

GitHub Actions配置片段：

jobs:
  build:
    steps:
      - uses: actions/checkout@v3
      - run: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
      - run: lake build

故障排除[编辑 | 编辑源代码]

常见问题解决方案：

错误	解决方法
运行 `lake update`
增加栈空间：`lean --stack-size=8192`

数学公式支持[编辑 | 编辑源代码]

Lean CLI可以处理包含数学公式的文档，例如： $\forall (n : ℕ), \exists m > n$

对应Lean代码：

example : ∀ n : Nat, ∃ m, m > n := by
  intro n
  exists n + 1
  simp

扩展阅读[编辑 | 编辑源代码]

Lean 4官方文档中的[命令行工具章节]
《定理证明与编程实践》第3章