编辑“︁Lean命令行界面”︁

= Lean命令行界面 =

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

Lean CLI的主要功能包括：
* 初始化和管理Lean项目
* 编译和检查代码语法
* 运行测试和验证证明
* 安装和管理第三方工具链（如`mathlib`）

== 安装与配置 ==
=== 基础安装 ===
通过[Elan](https://github.com/leanprover/elan)（Lean版本管理器）安装CLI工具链：
<syntaxhighlight lang="bash">
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
</syntaxhighlight>

验证安装：
<syntaxhighlight lang="bash">
lean --version
# 输出示例：Lean (version 4.2.0)
</syntaxhighlight>

=== 项目结构 ===
典型的Lean项目目录结构如下：
<mermaid>
graph TD
    A[Project Root] --> B[Lean.toml]
    A --> C[Main.lean]
    A --> D[Lakefile.lean]
    A --> E[build/]
</mermaid>

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

== 核心命令 ==
=== 项目初始化 ===
创建新项目：
<syntaxhighlight lang="bash">
lake new my_project
</syntaxhighlight>

=== 编译与运行 ===
编译单个文件：
<syntaxhighlight lang="bash">
lean Main.lean
</syntaxhighlight>

使用Lake构建系统（推荐）：
<syntaxhighlight lang="bash">
lake build
</syntaxhighlight>

=== 交互模式 ===
启动交互式REPL环境：
<syntaxhighlight lang="bash">
lean --repl
</syntaxhighlight>

示例会话：
<syntaxhighlight lang="lean">
# 输入：
#eval 1 + 1
# 输出：
2
</syntaxhighlight>

== 高级用法 ==
=== 定理证明辅助 ===
调用自动化证明器：
<syntaxhighlight lang="bash">
lean --run Proof.lean
</syntaxhighlight>

文件内容示例：
<syntaxhighlight lang="lean">
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a
  · simp
  · simp [*]
</syntaxhighlight>

=== 性能分析 ===
生成时间统计报告：
<syntaxhighlight lang="bash">
lean --profile Main.lean
</syntaxhighlight>

输出示例：
<pre>
Processing time: 1.23s
Memory usage: 45MB
</pre>

== 实际案例 ==
=== 数学库开发 ===
1. 初始化项目：
   <syntaxhighlight lang="bash">
   lake init math_lib
   </syntaxhighlight>

2. 添加`mathlib`依赖：
   修改`Lakefile.lean`：
   <syntaxhighlight lang="lean">
   require mathlib from git "https://github.com/leanprover-community/mathlib4"
   </syntaxhighlight>

3. 构建项目：
   <syntaxhighlight lang="bash">
   lake update
   lake build
   </syntaxhighlight>

=== CI集成示例 ===
GitHub Actions配置片段：
<syntaxhighlight lang="yaml">
jobs:
  build:
    steps:
      - uses: actions/checkout@v3
      - run: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
      - run: lake build
</syntaxhighlight>

== 故障排除 ==
常见问题解决方案：
{| class="wikitable"
! 错误 !! 解决方法
|-
| `unknown package 'mathlib'` | 运行 `lake update`
|-
| `maximum recursion depth` | 增加栈空间：`lean --stack-size=8192`
|}

== 数学公式支持 ==
Lean CLI可以处理包含数学公式的文档，例如：
<math>
\forall (n : \mathbb{N}), \exists m > n
</math>

对应Lean代码：
<syntaxhighlight lang="lean">
example : ∀ n : Nat, ∃ m, m > n := by
  intro n
  exists n + 1
  simp
</syntaxhighlight>

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean基础]]