安装教程推荐
Windows 下 Lean4 安装教程: 安装 – Lean定理证明 (subfish-zhou.github.io)
英文版:Extended Setup Notes – Lean Manual (lean-lang.org)
推荐:Lean4入门:安装配置篇_哔哩哔哩_bilibili
Lean4 参考教材地址:leanprover-community/mathematics_in_lean: The user home repository for the Mathematics in Lean tutorial. (github.com)
安装流程
配套软件安装顺序: glean
(避免被墙) → o→ elan
→ o→ 确定项目依赖 → o→ 对应版本的 lean 4
到对应镜像地址下载 glean
elan
; glean
下载后所需要的是其中的可执行文件 glean.exe
,执行安装 elan
压缩包里的安装文件 elan-init.exe
完成 elan
的安装,安装完后可以在用户目录下找到 .elan
文件夹,C:UsersUsername.elanin
也应该被自动添加进环境变量(若没有可以手动添加一下);最后将 glean.exe
移动至 C:UsersUsername.elanin
文件夹里.
下载对应的项目文件,如 mathematics_in_lean,直接 git clone https://mirror.sjtu.edu.cn/git/lean4-packages/mathematics_in_lean
,如果不想使用镜像,可以到到对应的 github 仓库下载 .
到项目文件夹下的 lean-toolchain
查看所需 lean 4
的版本例如 leanprover/lean4:v4.xx.xx
,使用 elan install leanprover/lean4:v4.xx.xx
;如果不想FQ,可以使用 glean -install lean --version 4.xx.xx
进行安装.
接下来进行编译,编译非常耗时,如果想节省时间且能FQ的话可以先在项目文件夹下执行 lake exe cache get
拉取 cache,再执行 lake build
; 如果不行,则只好花点时间直接在项目文件夹下执行 lake build
,具体时间由 cpu 性能决定,一般 1h 内就可以编译好.
在 vscode 中安装 lean4
插件,即可完成基本项目环境的配置.
可能存在的问题:
使用 lake
相关指令后报错 error: could not detect the configuration of the Lake installation
.
原因 : 路径中含有中文名,具体解决方案可以从参考这篇文章.
vscode 的 powershell 无法识别 elan 命令,具体如下
原因是因为找不到对应路径,解决方法如下:
ctrl
+,
打开 vscode 设置,搜索 terminal.integrated.env.windows
,在 settings.json
中编辑,添加
"terminal.integrated.env.windows": {
"PATH":"C:/Users/Username/.elan/bin;${env:PATH}"
},
注意,不要漏掉 ${env:PATH}
否则会导致丢失系统变量