Commit Graph

3 Commits

Author SHA1 Message Date
claude-bot 3e0782c62a ci: fetch the Mathlib cache only through the retry loop
ci / python (push) Successful in 15s
ci / lean (push) Successful in 28s
ci / image (push) Successful in 1m24s
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
2026-10-21 11:32:39 +00:00
claude-bot 09ea8a67ce ci: retry Mathlib cache fetches that drop a few transfers
ci / lean (push) Successful in 2m24s
ci / image (push) Failing after 19m16s
ci / python (push) Successful in 16s
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
2026-10-21 11:08:48 +00:00
claude-bot 066b3f158b ci: run tests, real Lean + Mathlib smoke and image build on the lean4.35 runner
ci / python (push) Successful in 30s
ci / lean (push) Failing after 8m14s
ci / image (push) Has been skipped
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
2026-10-21 10:58:42 +00:00