Repository navigation
ci(cache): retry partial Mathlib bootstrap downloads in place #1730
Description
Observed during #1726/#1727: source run 41067048403 failed before building on attempts 1 and 2 because one, then three different Mathlib cache files returned HTTP 502. Attempt 3 passed all strict gates unchanged. Whole-job retries discarded thousands of successful downloads.
The executed lean-action fe408643 runs one bare lake exe cache get; its supported use-mathlib-cache: "false" input disables only that cache step. Pinned Mathlib 69552756 retries ordinary get without forcing existing archives, so an in-job retry requests the missing files. Our existing get.sh tolerates a Mathlib miss but attempts it only once; CI's later get-missing.sh restores Complexity outputs only.
Prepare a small bootstrap repair:
- Disable only lean-action's built-in Mathlib cache fetch, retaining its installation/configuration failures. Run bounded retries of the existing exact cache command within the same job, preserving successful downloads. After exhausted optional-cache retries, warn and leave all strict build/test/lint/import gates active; never continue-on-error the entire composite or replace
getwith forcedget!. - Preserve unset/empty/explicit
MATHLIB_CACHE_GET_URLbehavior and all existing cache, kill-switch and provenance controls. Reuse the existing bootstrap helper where small and concrete; avoid another parallel cache framework or changing Complexity's missing-only restore behavior. - Cover Lean CI and API docs consistently. Before docs generation, consider the existing missing-only Complexity cache helper: the failed API run cold-built local modules for about 54 minutes, while source CI reused accepted outputs. Keep cache failure as an optimization failure, not a skipped validation.
- Add meaningful partial-download/retry-limit/override/fallback tests, run all six default gates and relevant workflow/bootstrap/config checks, assess abstracts, and obtain independent CI/provenance review of the final revision.
Status: available; no implementation claim yet. Coordinate workflow edits with #1728 and preserve #1726's step-local worker-pool fix. Do not extend or restart the frozen capped API validation at 66c395fa for this follow-up. This is CI reliability/ergonomics, not a Lean mathematical change or a cache-benefit conclusion.
AI assistance: Codex inspected the executed action and existing bootstrap scripts after two recorded network failures.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
Worker
/root/mathlib_cache_retry_1730(Codex, session 2026-10-30): active on the bounded partial-Mathlib retry repair. Branchwork/mathlib-cache-retry-1730-codex, source-only worktree; no second dependency tree. I will preserve partial downloads, URL overrides, strict validation and the separate docs-memory/measurement controls, then hand the frozen revision to coordinator/rootfor serialized full validation and outside CI review.SamuelSchlesinger commentedon Oct 30, 2026
Worker
/root/mathlib_cache_retry_1730: active; implementation is frozen at11d6dc4cfor the coordinator's serialized full-six validation. Nine focused subprocess/workflow tests pass, including partial-download reuse, bounded retries/timeouts, URL compatibility and preservation of a strict build failure. The branch includes landed #1744 without changing its driver/protocol/tests; no study or API build ran. Next: finish canonical validation, then open the PR and request outside CI review.SamuelSchlesinger commentedon Oct 30, 2026
Worker
/root/mathlib_cache_retry_1730: validation is waiting on separate test-only repair #1753. After merging main, the unchanged measurement fixtures reject this host's free disk before reaching their assertions; all nine retry-specific tests pass. The six-file retry layer remains frozen on its published branch. Once #1753 lands, I will merge it normally, rerun the complete suite and finish the PR/CI-review handoff. No production budget or cache contents were altered.chore: inherit landed measurement fixture repair for cache validation
SamuelSchlesinger commentedon Oct 30, 2026
Worker
/root/mathlib_cache_retry_1730: awaiting outside CI/provenance review in #1775 atb41065d63c82b20ff85654612fdb377878d6c2e7. The six-file retry layer normally inherits landed #1755; the PR owns the validation/limitations record. All six default gates and 444 Python tests pass (17 optional skips). Canonical hosted CI and independent final-revision review remain before coordinator integration. No study or full API build was run.test(cache): isolate measurement fixtures from host free space (cslib…
ci(cache): retry partial Mathlib downloads in place (cslib-community#…
SamuelSchlesinger commentedon Oct 30, 2026
Completed — the bounded partial-download retry milestone landed through #1775, with outside review, validation and shared main/cache closeout recorded once. #1197's study/net-benefit objective and the #1726/#1727 pin, tag-policy and API-memory work remain open.
ci(comparator): reuse bounded Mathlib cache bootstrap (cslib-communit…
feat(polytime): certify fixed-list flatMap and filtered templates (cs…