VSCode 中安装 Lean 4

VSCode中安装扩展：

跟随右侧导航走即可：

记得给 elan 设置一下环境变量，elan 一般在这个文件夹下（C:\User\<User Name>\.elan\bin\）：

编写一个测试文件：

点击右侧 $\forall$ 符号，选择 Toggle Infoview 可以看到一些预览信息（或快捷键 Ctrl+Shift+Enter：

Lean 4 项目的创建

我们使用 lake 进行项目的创建

注（引用自：Lean4 - Mathlib4 / 用于形式化数学的准备 (1) - 知乎，Lean4 安装教程 - Lean Prover 中文文档）：

lake：Lean 4 的包管理器，全称 Lean Make，已合并到 Lean 4 仓库，作为源码的一部分。它用于创建 Lean 项目，构建 Lean 包，配置 Mathlib 和编译 Lean 可执行文件。

elan：Lean 环境版本管理器。它的功能类似于 Rust 的 rustup 或 Node.js 的 nvm，用于安装、管理和切换不同版本的 Lean。

然后可以使用以下命令进行项目

lake new basic

这样就建立了一个名为 basic 的项目，它的结构是这样的：

basic
├─ Basic
│  └─ Basic.lean
├─ Basic.lean
├─ lake-manifest.json
├─ lakefile.toml
├─ lean-toolchain
├─ Main.lean
└─ README.md

或者你也可以选择在某个文件夹下直接运行 lake init 进行初始化。

接下来就可以使用 lake 来将 Lean 4 程序转换为可执行程序了：

lake build

你观察项目文件目录结构会发现恰好多了一个 ./lake 文件夹。接下来就是运行：

lake exec hello

总结 lake 常见用法如下所示：

# 构建新项目
lake new <project_name>
# 在当前文件夹初始化新项目
lake init
# 构建项目可执行文件
lake build
# 运行
lake exec <project_name>
# 清理构建文件
lake clean
# 更新依赖
lake update
# 运行 lakefile.lean 的脚本
lake run <script>

包的引用

注意到初始化好的项目中有一个文件 leanfile.toml ，这是一个配置文件，我们可以在其中进行引用的管理，格式如下：

# A Reservoir dependency
[[require]]
name = "<pkg-name>"
scope = "<scope>"
version = "<version>"
options = {<options>}

# A path dependency
[[require]]
name = "<pkg-name>"
path = "<path>"

# A Git dependency
[[require]]
name = "<pkg-name>"
git = "<url>"
rev = "<rev>"
subDir = "<subDir>"

其中比如我们想要引用 Mathlib，那么就可以如下编辑 leanfile.toml 文件：

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

[[lean_lib]]
name = "Basic"

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

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.11.0"

注意把 lean-toolchain 内容改为：

leanprover/lean4:v4.11.0

（等价于 curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain）

如果你是 leanfile.lean，则在文件中添加：require mathlib from git "https://github.com/leanprover-community/mathlib4" 即可。

当然你也可以选择在安装项目的时候使用指令：
lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math

这时运行 lake update ，额，它就会疯狂安装包。

下面这个命令可以下载预编译的文件：

这样build就很快：

Lean4-0 —— Lean4 的安装

VSCode 中安装 Lean 4

Lean 4 项目的创建

包的引用