Lean 4 安装教程及环境管理

在这里插入图片描述

唠唠闲话

Lean 是一个交互式定理证明器（Interactive Theorem Prover, ITP），也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。用于定理证明的编程语言还有很多，比如 Coq，isabelle，HOL Light 等。很多数学家选择使用 Lean 的标准库 mathlib 作为基础，这个仓库也被称为未来的数学图书馆。

Lean 4 的官方文档(Get started)提供了不同平台的安装方式，包括 Windows、MacOS 和 Ubuntu 系统，且都提供了一行脚本运行的方式。但在国内因为网络问题，通常要借助镜像站或手动安装。

当前教程针对 Ubuntu 系统，Windows 可以参考子鱼的博客，Mac 系统可以按官网教程，使用 homebrew 来快速配置。

安装教程

如果没有网络问题，用一行命令安装：

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

该命令执行了一个脚本：install_debian.sh，脚本安装了 VsCode，LEAN 插件，以及 elan。

如果下载不了 GitHub 资源，在安装了 VsCode 和 LEAN 4 拓展后，脚本里只有 elan 是需要手动安装的。

安装 elan

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

在 GitHub release 页面根据系统版本下载新版 elan，比如 linux-x86_64 系统的 elan 安装器地址为：

https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz

如果不确定系统架构，执行 uname -s 和 uname -m 查看：

❯ uname -s
Linux
❯ uname -m
x86_64

下载文件并解压：

# 如果网络不行就本地下载再上传
curl https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
tar xf elan.tar.gz

解压得到 elan-init 文件，赋予可执行权限并执行：

chmod +x elan-init
./elan-init

完成后，在 .bashrc 或 .zshrc 中修改环境变量：

export PATH="$HOME/.elan/bin:$PATH"

重启终端，检查 elan 版本和默认安装的 Lean 版本：

❯ elan -V
elan 3.1.1 (71ddc6633 2024-02-22)
❯ elan show
stable (default)
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)

elan 的管理目录为 $HOME/.elan，内容形如

❯ tree .elan -L 2
.elan
├── bin
│   ├── elan
│   ├── lake
│   ├── lean
│   ├── leanc
│   ├── leanchecker
│   ├── leanmake
│   └── leanpkg
├── env
├── settings.toml
├── tmp
├── toolchains
│   └── stable
└── update-hashes└── stable

下载的 LEAN 版本在 toolchains 目录下，settings.toml 是 elan 的配置文件。

elan 的二进制文件中，lake 经常会用到。

Lake 管理器

lake 全称 Lean Make，是 LEAN4 的包管理器，已合并到 LEAN4 仓库，作为源码的一部分。

下边用一个简单的例子演示 lake 的基本用法。

创建项目，目录为 hello

# 创建包
lake new hello
## 或者
mkdir hello && cd hello && lake init hello
# 构建包
lake build
# 运行
lake exec hello # Hello, world!
# 清理构建文件
lake clean
# 更新依赖
lake update
# 运行 lakefile.lean 的脚本
lake run <script>