From ffe4624ccac188d55f840ebca5e859fddfcd4475 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 12:14:26 -0400 Subject: [PATCH] ci(cache): retry partial Mathlib downloads in place Share three bounded non-forced cache-get attempts between local bootstrap, Lean CI and API docs. Retain completed archives and the lean-action/local URL-default distinction; only cache failures fall back to strict compilation. Docs reuse the existing missing-only Complexity helper. Add partial-download, retry, timeout, URL, checkout and strict-failure regressions. No Lean, abstract or renderer-source impact. AI assistance: Codex worker /root/mathlib_cache_retry_1730 for #1730. --- .github/workflows/docs.yml | 9 ++ .github/workflows/lean_action_ci.yml | 7 +- scripts/cache/README.md | 14 +++ scripts/cache/get.sh | 3 +- scripts/cache/get_mathlib.py | 66 +++++++++++ scripts/test_mathlib_cache.py | 171 +++++++++++++++++++++++++++ 6 files changed, 268 insertions(+), 2 deletions(-) create mode 100644 scripts/cache/get_mathlib.py create mode 100644 scripts/test_mathlib_cache.py diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index ec877a7a1..405ca98af 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -33,6 +33,15 @@ jobs: build: "false" test: "false" lint: "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 missing Complexitylib build outputs + continue-on-error: true + timeout-minutes: 10 + run: scripts/cache/get-missing.sh - name: Generate API documentation run: DISABLE_EQUATIONS=1 lake -d docbuild build Complexity:docs # Also catches library changes that break one of the guide's examples. diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index d0491c21a..f7653bebb 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -46,7 +46,7 @@ jobs: - name: "Documentation pins" run: python3 -B scripts/check_docs.py --config-only # lean-action has no hook between installing the toolchain and building, so here it only - # installs elan and fetches Mathlib's cache. The steps around it do the rest of what it did: + # installs elan. The steps around it do the rest of what it did, with bounded cache retries: # restore and save `.lake` under the same Actions cache key, then build, test and lint. - name: Restore .lake from the Actions cache id: lake-cache @@ -65,6 +65,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 # The earlier script tests run before Lean is installed and skip this real build test. # Exercise both compiler setup-input omissions with an isolated, cache-disabled project. - name: Test Lake build handoff reuse diff --git a/scripts/cache/README.md b/scripts/cache/README.md index 30cf2a4a9..843f2ff5f 100644 --- a/scripts/cache/README.md +++ b/scripts/cache/README.md @@ -26,6 +26,20 @@ CI reads the cache too. After restoring `.lake` from the GitHub Actions cache, L input hash already matches a build trace in `.lake`. A fresh runner would otherwise download a complete set on every run, although `.lake` usually has most of it. +Mathlib downloads are retried in the same checkout by `scripts/cache/get_mathlib.py`: at most +three ordinary `lake exe cache get` attempts, each limited to three minutes, with two-second +pauses. Completed archives remain in place, so the pinned Mathlib client retries only missing +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 +`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 +Complexitylib restore before generation. Cache failures remain optional; installation and +validation failures remain strict. + The Lean workflows also restore elan and the toolchain named in `lean-toolchain` (`~/.elan`, about 600 MB) from the Actions cache before `leanprover/lean-action` runs, so that the action does not download the toolchain. On a miss, `.github/actions/install-lean` installs them with bounded diff --git a/scripts/cache/get.sh b/scripts/cache/get.sh index d54352efb..84313b22c 100755 --- a/scripts/cache/get.sh +++ b/scripts/cache/get.sh @@ -7,6 +7,7 @@ # `main` CI has uploaded (Lake looks back up to 100 commits). Missing outputs are not an error: # `lake build` compiles whatever the cache did not provide. See scripts/cache/README.md. set -u +script_dir="$(cd "$(dirname "$0")" && pwd)" || exit 1 if [ -n "${COMPLEXITYLIB_CACHE_CHECKOUT:-}" ]; then cd "$COMPLEXITYLIB_CACHE_CHECKOUT" || exit 1 else @@ -15,7 +16,7 @@ fi url="${COMPLEXITYLIB_CACHE_URL-https://storage.googleapis.com/complexitylib-lake-cache}" -lake exe cache get || echo "warning: Mathlib cache download failed; lake build will compile Mathlib" >&2 +COMPLEXITYLIB_CACHE_CHECKOUT="$PWD" python3 "$script_dir/get_mathlib.py" if [ -z "$url" ]; then echo "COMPLEXITYLIB_CACHE_URL is empty; skipping the Complexitylib cache." >&2 exit 0 diff --git a/scripts/cache/get_mathlib.py b/scripts/cache/get_mathlib.py new file mode 100644 index 000000000..1d2ecb315 --- /dev/null +++ b/scripts/cache/get_mathlib.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Retry optional Mathlib downloads in place; ordinary `get` keeps completed archives.""" + +import argparse +import os +from pathlib import Path +import signal +import subprocess +import sys +import time + +ATTEMPTS = 3 +ATTEMPT_SECONDS = 180 +RETRY_SECONDS = 2 +ROOT = Path(__file__).resolve().parents[2] + + +def restore(root, env, lean_action=False): + env = dict(env) + if lean_action: + # Preserve lean-action fe408643's unset/empty/explicit URL handling. + if "MATHLIB_CACHE_GET_URL" not in env: + env["MATHLIB_CACHE_GET_URL"] = "https://cache.mathlib.org/mathlib4" + elif not env["MATHLIB_CACHE_GET_URL"]: + del env["MATHLIB_CACHE_GET_URL"] + for attempt in range(1, ATTEMPTS + 1): + print(f"Mathlib cache attempt {attempt}/{ATTEMPTS}", flush=True) + try: + process = subprocess.Popen(["lake", "exe", "cache", "get"], cwd=root, env=env, + start_new_session=(os.name == "posix")) + try: + if process.wait(timeout=ATTEMPT_SECONDS) == 0: + return True + reason = f"exit status {process.returncode}" + finally: + if process.poll() is None: + if os.name == "posix": + try: + os.killpg(process.pid, signal.SIGKILL) + except ProcessLookupError: + pass + else: + process.kill() + process.wait() + except (OSError, subprocess.TimeoutExpired) as error: + reason = str(error) + print(f"warning: Mathlib cache attempt failed: {reason}", file=sys.stderr, flush=True) + if attempt < ATTEMPTS: + time.sleep(RETRY_SECONDS) + print("warning: Mathlib cache download failed; lake build will compile missing outputs", + file=sys.stderr) + return False + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--lean-action", action="store_true", + help="retain lean-action's cache URL defaults") + args = parser.parse_args() + root = Path(os.environ.get("COMPLEXITYLIB_CACHE_CHECKOUT") or ROOT) + restore(root, os.environ, args.lean_action) + return 0 # Cache availability never substitutes for the subsequent strict build. + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/test_mathlib_cache.py b/scripts/test_mathlib_cache.py new file mode 100644 index 000000000..cb243df28 --- /dev/null +++ b/scripts/test_mathlib_cache.py @@ -0,0 +1,171 @@ +"""Exercise bounded optional-cache retries using subprocesses, without Lean or network access.""" + +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile +import unittest +from unittest.mock import patch + +REPO = Path(__file__).resolve().parent.parent +spec = importlib.util.spec_from_file_location("get_mathlib", REPO / "scripts/cache/get_mathlib.py") +cache = importlib.util.module_from_spec(spec) +spec.loader.exec_module(cache) + +FAKE_LAKE = r'''#!/usr/bin/env python3 +import json, os, pathlib, sys, time +args = sys.argv[1:] +artifacts = pathlib.Path(os.environ["MATHLIB_TEST_CACHE"]) +artifacts.mkdir(exist_ok=True) +with open(os.environ["MATHLIB_TEST_LOG"], "a") as target: + target.write(json.dumps({"args": args, "url": os.environ.get("MATHLIB_CACHE_GET_URL"), + "cwd": os.getcwd(), "existing": sorted(p.name for p in artifacts.iterdir())}) + "\n") +if args == ["exe", "cache", "get"]: + mode = os.environ.get("MATHLIB_TEST_MODE", "success") + if mode == "partial": + first = artifacts / "first.ltar" + if not first.exists(): + first.write_text("completed first archive") + sys.exit(1) + (artifacts / "second.ltar").write_text("completed second archive") + elif mode == "fail": + sys.exit(17) + elif mode == "hang": + time.sleep(30) +elif args[:1] == ["build"]: + sys.exit(23) +''' + + +@unittest.skipUnless(os.name == "posix", "subprocess fixtures require POSIX executable scripts") +class MathlibCacheTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="mathlib-cache-retry-") + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + self.log = self.root / "events.jsonl" + self.artifacts = self.root / "archives" + bin_dir = self.root / "bin" + bin_dir.mkdir() + lake = bin_dir / "lake" + lake.write_text(FAKE_LAKE) + lake.chmod(0o755) + self.env = {k: v for k, v in os.environ.items() + if not k.startswith(("MATHLIB_CACHE_", "COMPLEXITYLIB_CACHE_", "GIT_"))} + self.env.update(PATH=str(bin_dir) + os.pathsep + os.environ["PATH"], + MATHLIB_TEST_LOG=str(self.log), MATHLIB_TEST_CACHE=str(self.artifacts), + GIT_CONFIG_GLOBAL=os.devnull, GIT_CONFIG_NOSYSTEM="1") + + def events(self): + return [json.loads(line) for line in self.log.read_text().splitlines()] + + def restore(self, *, lean_action=False, **changes): + with patch.object(cache, "RETRY_SECONDS", 0): + return cache.restore(self.root, {**self.env, **changes}, lean_action) + + def test_partial_download_is_kept_and_only_ordinary_get_is_retried(self): + self.assertTrue(self.restore(MATHLIB_TEST_MODE="partial")) + events = self.events() + self.assertEqual(len(events), 2) + self.assertEqual([e["args"] for e in events], [["exe", "cache", "get"]] * 2) + self.assertEqual([e["existing"] for e in events], [[], ["first.ltar"]]) + self.assertEqual((self.artifacts / "first.ltar").read_text(), "completed first archive") + self.assertEqual((self.artifacts / "second.ltar").read_text(), "completed second archive") + self.assertTrue(all(Path(e["cwd"]) == self.root for e in events)) + + def test_success_does_not_retry(self): + self.assertTrue(self.restore()) + self.assertEqual(len(self.events()), 1) + + def test_exhausted_failures_stop_after_three_attempts(self): + self.assertFalse(self.restore(MATHLIB_TEST_MODE="fail")) + self.assertEqual(len(self.events()), 3) + + def test_action_url_unset_empty_and_explicit_match_the_action(self): + for supplied, expected in ((None, "https://cache.mathlib.org/mathlib4"), + ("", None), ("https://cache.example.invalid", "https://cache.example.invalid")): + with self.subTest(supplied=supplied): + changes = {} if supplied is None else {"MATHLIB_CACHE_GET_URL": supplied} + self.assertTrue(self.restore(lean_action=True, **changes)) + self.assertEqual(self.events()[-1]["url"], expected) + + def test_local_url_environment_is_unchanged(self): + for supplied in (None, "", "https://cache.example.invalid"): + with self.subTest(supplied=supplied): + changes = {} if supplied is None else {"MATHLIB_CACHE_GET_URL": supplied} + env = {**self.env, **changes, "COMPLEXITYLIB_CACHE_CHECKOUT": str(self.root), + "COMPLEXITYLIB_CACHE_URL": ""} + result = subprocess.run([str(REPO / "scripts/cache/get.sh")], cwd=self.root, + env=env, capture_output=True, text=True) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertEqual(self.events()[-1]["url"], supplied) + + def test_get_script_keeps_relative_checkout_overrides(self): + env = {**self.env, "COMPLEXITYLIB_CACHE_CHECKOUT": self.root.name, + "COMPLEXITYLIB_CACHE_URL": ""} + result = subprocess.run([str(REPO / "scripts/cache/get.sh")], cwd=self.root.parent, + env=env, capture_output=True, text=True) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertEqual(Path(self.events()[-1]["cwd"]), self.root) + + def test_timeout_stops_each_owned_process_before_retrying(self): + created = [] + original = subprocess.Popen + def start(*args, **kwargs): + process = original(*args, **kwargs) + created.append(process) + return process + with patch.object(cache, "ATTEMPT_SECONDS", .1), patch.object(cache.subprocess, "Popen", side_effect=start): + self.assertFalse(self.restore(MATHLIB_TEST_MODE="hang")) + self.assertEqual(len(created), 3) + self.assertTrue(all(p.poll() is not None for p in created)) + + @unittest.skipUnless(shutil.which("git"), "git is required for the real build wrapper") + def test_cache_failure_still_runs_and_preserves_the_strict_build_failure(self): + for name in ("scripts/build.sh", "scripts/cache/ensure.sh", "scripts/cache/get.sh", + "scripts/cache/get_mathlib.py"): + target = self.root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy(REPO / name, target) + for name in ("lean-toolchain", "lake-manifest.json", "lakefile.toml"): + (self.root / name).write_text("fixture\n") + subprocess.run(["git", "init", "-q"], cwd=self.root, env=self.env, check=True) + subprocess.run(["git", "-c", "user.name=Cache fixture", "-c", + "user.email=cache@example.invalid", "commit", "--allow-empty", "-qm", "fixture"], + cwd=self.root, env=self.env, check=True) + env = {**self.env, "MATHLIB_TEST_MODE": "fail", "COMPLEXITYLIB_CACHE_URL": ""} + result = subprocess.run([str(self.root / "scripts/build.sh"), "--wfail", "--iofail"], + cwd=self.root, env=env, capture_output=True, text=True) + self.assertEqual(result.returncode, 23, result.stdout + result.stderr) + self.assertIn("will compile missing outputs", result.stderr) + self.assertEqual([e["args"] for e in self.events()], + [["exe", "cache", "get"]] * 3 + [["build", "--wfail", "--iofail"]]) + + +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"): + 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.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) + self.assertIn("timeout-minutes: 10", step) + self.assertIn("python3 -B scripts/cache/get_mathlib.py --lean-action", step) + ci = (REPO / ".github/workflows/lean_action_ci.yml").read_text() + for command in ("lake build --wfail --iofail", "lake test --wfail --iofail", "lake lint", + "lake exe mk_all --check", "lake exe lint-style", "lake exe checkInitImports"): + self.assertIn(command, ci) + docs = (REPO / ".github/workflows/docs.yml").read_text() + self.assertLess(docs.index("run: scripts/cache/get-missing.sh"), + docs.index(" - name: Generate API documentation")) + self.assertIn("DISABLE_EQUATIONS=1 lake -d docbuild build Complexity:docs", docs) + + +if __name__ == "__main__": + unittest.main()