ci(comparator): reuse bounded Mathlib cache bootstrap

.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

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

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()