claude-bot
3e0782c62a
Mathlib's post-update hook fetched the cache inside 'lake update', where a few dropped transfers failed the build before the retries could run. Disable the hook, retry up to six times, and keep the archives in a BuildKit cache mount so a retried image build resumes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
Dockerfile 构建完整运行镜像：
- 基于 Ubuntu 24.04。
- 安装 Python、Git、curl、SQLite 等。
- 安装 elan。
- 解析 Mathlib 和 Lean 兼容版本。
- 运行 lake update。
- 下载 Mathlib 预编译缓存。
- 用真实 Lean 编译 smoke 文件。
- 安装 lean-bench Python 包。
- 配置数据库、LLM 和 Lean 环境变量。
- 挂载 /books 与 /data。 镜像很重，Mathlib 缓存和编译对内存、磁盘要求较高。
docker-compose.yml 本地 Docker Compose 配置：
- 构建或拉取 lean-bench 镜像。
- 注入 DashScope API Key 和模型设置。
- 把本地 books/ 映射到 /books。
- 把本地 data/ 映射到 /data。
- 默认运行 doctor。
entrypoint.sh 容器入口：
- 创建数据库父目录。
- 设置运行环境。
- 把用户传入参数交给 lean-bench。
- 允许镜像直接执行 ingest、search 等子命令。
resolve-mathlib.sh 构建阶段解析 Lean/Mathlib 兼容性：
- 接受显式 Mathlib revision 或 auto。
- 查找合适的 Mathlib revision。
- 根据 Mathlib 对应配置确定 Lean toolchain。
- 更新 Lean 工程配置。 它解决“Lean 版本和 Mathlib revision 不兼容”的常见构建问题，但动态解析降低了可复现性。
smoke.py Docker 中的端到端 smoke test：
- 使用脚本化 LLM 回复。
- 走完整 ingest 流程。
- 调用真实 Lean，而不是 fake checker。
- 写入临时 SQLite 数据库。
- 检查生成条目确实被 Lean 验证并可查询。 这曾经由 Docker CI 调用；工作流删除后，当前没有自动执行者。