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