Update lean/README.md
This commit is contained in:
+3
-3
@@ -1,14 +1,14 @@
|
||||
[lean-toolchain](/Users/zzyang/ProjectResearch/lean-bench/lean/lean-toolchain)
|
||||
[lean-toolchain](lean-bench/lean/lean-toolchain)
|
||||
指定 Lean 工具链版本,供 elan 和 Lake 使用。
|
||||
|
||||
[lakefile.toml](/Users/zzyang/ProjectResearch/lean-bench/lean/lakefile.toml)
|
||||
[lakefile.toml](lean-bench/lean/lakefile.toml)
|
||||
Lean Lake 工程配置:
|
||||
- 定义项目。
|
||||
- 声明 Mathlib 依赖。
|
||||
- 让 lake env lean 能在正确环境中加载 Mathlib。
|
||||
Mathlib 精确 revision 主要在 Docker 构建时解析,而不是完整锁定在仓库中。
|
||||
|
||||
[LeanBench.lean](/Users/zzyang/ProjectResearch/lean-bench/lean/LeanBench.lean)
|
||||
[LeanBench.lean](lean-bench/lean/LeanBench.lean)
|
||||
Docker 构建时使用的 Lean smoke 文件:
|
||||
- 导入 Mathlib。
|
||||
- 放置少量声明。
|
||||
|
||||
Reference in New Issue
Block a user