安装 lean4

随笔1个月前发布 蔡蔡
40 0 0

安装教程推荐

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 命令,具体如下

安装 lean4

原因是因为找不到对应路径,解决方法如下:

ctrl+,打开 vscode 设置,搜索 terminal.integrated.env.windows,在 settings.json 中编辑,添加

  "terminal.integrated.env.windows": {
      "PATH":"C:/Users/Username/.elan/bin;${env:PATH}"
  },

注意,不要漏掉 ${env:PATH} 否则会导致丢失系统变量

© 版权声明

相关文章

暂无评论

您必须登录才能参与评论!
立即登录
暂无评论...