vscode安装lean4

本教程演示在Windows系统下如何安装Lean 4正式版。Linux和MacOS版本请参考Lean Manual。

如果你身在中国，在运行安装程序前需要做如下准备： 在系统目录C:\Windows\System32\drivers\etc文件夹下找到hosts文件。对于其它系统用户也都是找到各自系统的hosts文件。 这个文件需要管理员权限来修改，有一个简便方法是，把它复制到别的地方修改，然后再粘贴回去，并选择使用管理员身份继续。 用记事本打开这个文件，在最后一行写入185.199.108.133 raw.githubusercontent.com 重启电脑，然后开启科学上网。（注意，你需要让终端也处在梯子的作用域中，例如你使用clash类梯子需要打开全局模式。） （经过这个步骤之后你也可以使用官网提供的方法来安装了。） 如果你遇到"SSL connect error", "Timeout was reached","Failed to connect to github.com port 443"...等错误，就是说明你的网络环境有问题。重启电脑或者检查你的梯子。

基本安装

所有受支持平台的发布版本都可以在Releases · leanprover/lean4 · GitHub中找到。

1. 使用Lean版本管理器elan代替下载文件和手动设置路径。 在elan的Github仓库中下载最新release（对于windows，请下载elan-x86_64-pc-windows-msvc.zip），解压运行elan-init.exe，按照指示安装。 默认安装位置是用户文件目录下的.elan文件夹，添加环境变量你的用户文件目录\.elan\bin。 可能出现以下报错无法加载文件……因为在此系统上禁止运行此脚本”。解决方案是 1.用管理员身份运行Powershell； 2.输入命令set-Executionpolicy Remotesigned，选择Y； 然后就可以正常使用了。考虑到系统安全性，建议安装完成后将该选项改回默认值N。 效果如下图

setuplean

1. 安装git。安装 VS Code，并安装lean4扩展。

installing the vscode-lean4 extension

1. 在终端中运行 elan self update # 以防你下载的不是最新版elan # 下载及应用最新的Lean4版本 (https://github.com/leanprover/lean4/releases) elan default leanprover/lean4:stable # 也可选择，只在当前目录下使用Lean4
2. 创建一个以 .lean 为扩展名的新文件，并写入以下代码： #eval Lean.versionString 你会看到语法高亮。当你把光标放在最后一行时，在右边有一个“Lean信息视图”，显示已经安装的Lean版本。

successful setup

创建新Lean项目

用VS code打开一个新文件夹，你可以用两种方式创建新工程。

1. 在终端中运行（<your_project_name>替换为你自己起的名字） lake init <your_project_name> 以创建一个名为your_project_name的空白新工程。如果你想把你的Lean程序编译成可执行文件，在终端中运行lake build命令。 如果你想在这个现有的工程中引用Mathlib4，你需要在lakefile.lean文件中加入 require mathlib from git "https://github.com/leanprover-community/mathlib4" 然后在终端中运行 curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
2. 如果你想直接创建一个引用Mathlib4的新工程，在终端中运行 lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math 以创建一个名为your_project_name的新工程。

使用Mathlib

更多内容请参考Mathlib Wiki

在你的项目文件夹下打开VS code，使用终端运行

lake update lake exe cache get

如果你看到终端中显示了类似如下的提示：

Decompressing 1234 file(s) unpacked in 12345 ms

同时你的项目文件夹中出现了lake-packages文件夹，那么证明你安装Mathlib成功了，重启系统即可使用。注意：你要在lake-packages所在的目录中运行VScode，才能让Lean使用Mathlib。

这里提供一个实例来测试你的安装：

import Mathlib.Data.Real.Basic example (a b : ℝ) : a * b = b * a := by rw [mul_comm a b]

如果你的Lean infoview没有任何报错，并且光标放在文件最后一行时会提示“No goals”，证明你的Mathlib已经正确安装了。

如果你想更新Mathlib，在终端中运行

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain lake update lake exe cache get

【参考文献】

1 https://subfish-zhou.github.io/theorem_proving_in_lean4_zh_CN/setup.html