elan
glean
: Lean 4 镜像适配工具
使用上海交通大学的 https://mirror.sjtu.edu.cn 镜像服务,软件源镜像托管在 elan
和 git/lean4-packages
下。
请自行修改命令中的版本号,可用版本参见: http://mirror.sjtu.edu.cn/elan/?mirror_intel_list
也可以通过这个链接下载 glean。
安装 Elan
Elan 是 Lean 的版本管理工具,在 Lake 调用时根据项目 lean-toolchain
文件下载安装 Lean 并切换到对应的版本。
例如要阅读 Mathematics in Lean,可以运行
git clone --depth 1 https://mirror.sjtu.edu.cn/git/lean4-packages/mathematics_in_lean/
然后通过 cat lean-toolchain
获取需要安装的版本。
glean -install elan -version 3.1.1
安装 Lean
以下操作会安装 Lean 与 Lean 工具链,包含语言服务器、构建工具等。
glean -install lean --version 4.5.0
如需安装 nightly 版本,请以如下例子中的格式编辑命令。
glean -install lean --version 4.4.0-nightly-2023-11-12
nightly 可用版本参见 lean4_nightly
在构建项目前下载依赖
每当下载完一个 Lean 项目后,在启动 VSCode 或命令行运行 lake build
前,可以提前通过镜像下载依赖。
glean -lake-manifest-path ~/EG/lake-manifest.json
此处使用选项 -lake-manifest-path ~/EG/lake-manifest.json
来手动指定了 lake-manifest.json
文件的位置。
也可以在进入一个 Lean4 Lake 项目后,直接运行
glean
命令。这样,glean 会自动找到当前项目中 lake-manifest.json
文件的位置。
如何判断自己是否在在一个 Lean4 Lake 项目路径工作?
运行 ls
命令,如果能找到 lakefile.lean
,即代表正在 Lean4 Lake 项目路径工作。
使用 code .
启动 VSCode 来使用 Lean 时,也需要确保正在 Lean4 Lake 项目路径工作。
SJTUG Zhiyuan Mirror
由 上海交通大学 Linux 用户组 (SJTUG) 维护
沪交 ICP 备 20180085