From 279fee1e83095fbfc04235c197d0f8d590c0717d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 14:45:27 -0400 Subject: [PATCH] ci(comparator): reuse bounded Mathlib cache bootstrap Disable only lean-action's built-in Mathlib cache fetch in Comparator and call the existing get_mathlib.py --lean-action helper before the existing remote restore and strict contract/negative-control checks. Track helper and regression-test changes in both event filters, document the consumer, and cover cache ordering and strict proof checks in the wiring tests. The failure motivating #1786 is #1756 Comparator run 41090273729 attempt 1: its Mathlib bootstrap TLS/curl-55 errors skipped the proof-checking step. This reuses the unchanged helper from #1730/#1775; it does not claim to resolve the separate API-documentation memory/pin work or activate #1197. Self-validation on source-only base 9acffb0706ab25d05eb12693547990d6a89a550d: - 14 focused Mathlib-cache and Comparator Python tests pass. - Complete Python suite: 445 tests pass, with 17 expected skips. - check_hygiene.py --check-simp, check_docs.py --config-only and diff whitespace checks pass. - Removing the nine new workflow lines reproduces the old Comparator workflow byte for byte. Helper, Guide, dependency pins, proof contracts, sandbox and permissions are unchanged. - Rechecked lean-action v1 at fe408643ea7367d8c0404a8be3975bb145f5fb64; --lean-action preserves its unset/empty/explicit cache-URL handling. No Lean, curated abstract/catalogue, guide or renderer-source changes; no new PDF/render review is needed. Full six-gate validation, canonical hosted CI and outside-author-fleet operational review remain required. Issue: https://github.com/cslib-community/complexitylib/issues/1786 AI assistance: OpenAI Codex implemented and self-reviewed this bounded consumer follow-up, reusing the existing reviewed cache helper. --- .github/workflows/comparator.yml | 9 +++++++++ scripts/cache/README.md | 4 ++-- scripts/test_mathlib_cache.py | 22 ++++++++++++++++++++-- 3 files changed, 31 insertions(+), 4 deletions(-) diff --git a/.github/workflows/comparator.yml b/.github/workflows/comparator.yml index ab96d2a50..365c92026 100644 --- a/.github/workflows/comparator.yml +++ b/.github/workflows/comparator.yml @@ -8,6 +8,8 @@ on: - 'comparator/**' - 'scripts/check_comparator.py' - 'scripts/test_check_comparator.py' + - 'scripts/cache/get_mathlib.py' + - 'scripts/test_mathlib_cache.py' - 'lakefile.toml' - 'lean-toolchain' - 'lake-manifest.json' @@ -20,6 +22,8 @@ on: - 'comparator/**' - 'scripts/check_comparator.py' - 'scripts/test_check_comparator.py' + - 'scripts/cache/get_mathlib.py' + - 'scripts/test_mathlib_cache.py' - 'lakefile.toml' - 'lean-toolchain' - 'lake-manifest.json' @@ -57,6 +61,11 @@ jobs: test: 'false' lint: 'false' use-github-cache: 'false' + use-mathlib-cache: 'false' + - name: Restore Mathlib cache with retries + continue-on-error: true + timeout-minutes: 10 + run: python3 -B scripts/cache/get_mathlib.py --lean-action - name: Restore remote build outputs continue-on-error: true timeout-minutes: 10 diff --git a/scripts/cache/README.md b/scripts/cache/README.md index 609a271f5..3588090ed 100644 --- a/scripts/cache/README.md +++ b/scripts/cache/README.md @@ -32,8 +32,8 @@ pauses. Completed archives remain in place, so the pinned Mathlib client retries downloads. Exhausted attempts warn and leave the strict build/check commands to compile what is missing. Only the attempt's own process group is stopped on timeout on POSIX systems. -Lean CI and API docs disable only lean-action's built-in Mathlib fetch and call this helper with -`--lean-action`, preserving that action's URL handling: unset `MATHLIB_CACHE_GET_URL` selects +Lean CI, API docs and Comparator disable only lean-action's built-in Mathlib fetch and call this helper +with `--lean-action`, preserving that action's URL handling: unset `MATHLIB_CACHE_GET_URL` selects `https://cache.mathlib.org/mathlib4`, an empty value selects the Mathlib client's default, and an explicit URL is retained. Local `get.sh` and the Guide workflow use the same retries while retaining their existing client-default/environment behavior. API docs also use the existing missing-only diff --git a/scripts/test_mathlib_cache.py b/scripts/test_mathlib_cache.py index cb243df28..d67c2761b 100644 --- a/scripts/test_mathlib_cache.py +++ b/scripts/test_mathlib_cache.py @@ -147,11 +147,11 @@ def test_cache_failure_still_runs_and_preserves_the_strict_build_failure(self): class WorkflowWiringTests(unittest.TestCase): def test_only_optional_cache_step_is_relaxed_and_validation_remains(self): - for name in ("lean_action_ci.yml", "docs.yml"): + for name in ("lean_action_ci.yml", "docs.yml", "comparator.yml"): with self.subTest(workflow=name): text = (REPO / ".github/workflows" / name).read_text() action = text.split(" - uses: leanprover/lean-action@v1\n", 1)[1].split(" - ", 1)[0] - self.assertIn('use-mathlib-cache: "false"', action) + self.assertRegex(action, r"use-mathlib-cache: [\"']false[\"']") self.assertNotIn("continue-on-error", action) step = text.split(" - name: Restore Mathlib cache with retries\n", 1)[1].split(" - ", 1)[0] self.assertIn("continue-on-error: true", step) @@ -166,6 +166,24 @@ def test_only_optional_cache_step_is_relaxed_and_validation_remains(self): docs.index(" - name: Generate API documentation")) self.assertIn("DISABLE_EQUATIONS=1 lake -d docbuild build Complexity:docs", docs) + def test_comparator_restores_before_strict_contracts_and_tracks_its_helper(self): + text = (REPO / ".github/workflows/comparator.yml").read_text() + self.assertLess(text.index(" - uses: leanprover/lean-action@v1"), + text.index(" - name: Restore Mathlib cache with retries")) + self.assertLess(text.index(" - name: Restore Mathlib cache with retries"), + text.index("run: scripts/cache/get-missing.sh")) + self.assertLess(text.index("run: scripts/cache/get-missing.sh"), + text.index(" - name: Compare all reviewed contracts")) + contract_step = text.split(" - name: Compare all reviewed contracts", 1)[1] + self.assertIn("run: python3 scripts/check_comparator.py basic automation sat --negative-control", + contract_step) + self.assertNotIn("continue-on-error", contract_step) + for event, following in (("pull_request", "push"), ("push", "workflow_dispatch")): + with self.subTest(event=event): + trigger = text.split(f" {event}:\n", 1)[1].split(f" {following}:", 1)[0] + for dependency in ("scripts/cache/get_mathlib.py", "scripts/test_mathlib_cache.py"): + self.assertIn(f" - '{dependency}'", trigger) + if __name__ == "__main__": unittest.main()