diff --git a/lean/README.md b/lean/README.md index 981acd2..2aac257 100644 --- a/lean/README.md +++ b/lean/README.md @@ -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。 - 放置少量声明。