claude-bot
066b3f158b
Moves the Lean project to Lean 4.35.0 / Mathlib v4.35.0 to match the runner, caches the Mathlib project on the runner host, and builds and keeps the Docker image only after the Python and Lean jobs pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
lean-toolchain 指定 Lean 工具链版本，供 elan 和 Lake 使用。
lakefile.toml Lean Lake 工程配置：
- 定义项目。
- 声明 Mathlib 依赖。
- 让 lake env lean 能在正确环境中加载 Mathlib。 Mathlib 精确 revision 主要在 Docker 构建时解析，而不是完整锁定在仓库中。
LeanBench.lean Docker 构建时使用的 Lean smoke 文件：
- 导入 Mathlib。
- 放置少量声明。
- 验证 Mathlib olean、Lean 工具链和 lake env lean 能实际工作。 它不是项目运行时库，主要是环境健康检查。