Lean Theorem Prover 安装手记

我主要是遵循 https://leanprover-community.github.io/install/debian_details.html 来安装。

在虚拟机中安装 debian11，配置 4G 内存与 4G 交换空间。创建标准用户。以标准用户身份登陆，然后在终端依次执行以下命令（感觉直接以 root 身份登陆执行更恰当）：

wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
sudo apt install -y git curl python3 python3-pip python3-venv
sudo apt install ./code.deb
rm code.deb

前往 https://github.com/leanprover/elan/blob/master/elan-init.sh 复制 elan-init.sh 的内容到 ~/elan-init.sh 中（也可以用 git clone --depth=1 https://github.com/leanprover/elan.git 把仓库克隆最新版本下来再把文件找出来），然后继续在终端依次执行以下命令（要用标准用户，别用 root 用户）：

bash elan-init.sh -y
code --install-extension jroesch.lean
python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

最后打开 ~/.bashrc ，把 ~/.elan/bin 添加到路径中。

退出登陆，然后依然以标准用户身份重新登陆。在终端依次执行以下命令：

leanproject get tutorials
code tutorials

现在 VS Code 运行起来了。有可能会提示安装 Lean 的插件、然后要重配置 leanpkg，照着做就好。

如果发现运行起来吃内存太多（超过4G），那么可能是 mathlib 没有现成的 olean 文件。此时，在项目根目录中（例如 tutorials 目录中）运行 leanproject get-mathlib-cache 从网上下载现成的 olean 文件。完成之后，内存占用就会变得可以接受啦。

最后修改于 2021-06-26