diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index f6e4f2e28..8de73d5ef 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -65,6 +65,12 @@ jobs: test: "false" lint: "false" use-github-cache: "false" + # 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 + env: + COMPLEXITYLIB_TEST_LAKE_HANDOFF: "1" + run: python3 -B -m unittest discover -s scripts -p 'test_cache_handoff.py' # Download the outputs that `main` CI uploaded for the nearest uploaded ancestor of this # commit, skipping modules that `.lake` already has (scripts/cache/README.md). The script # deepens the depth-1 checkout to 100 generations to find that ancestor. Lake reuses an diff --git a/scripts/cache/README.md b/scripts/cache/README.md index 4c4bcffcc..c32146c44 100644 --- a/scripts/cache/README.md +++ b/scripts/cache/README.md @@ -53,6 +53,12 @@ existing hard-linked cache objects. Merge groups do not publish to GCS: the norm `main` run remains the only public-cache writer. This makes its outputs available sooner to following builds while preserving the public cache's authorization boundary. +- **Payload.** The archive keeps compiled outputs (including private/server OLeans, IR and native + code), hashes and traces. It omits only `ir/**/*.setup.json` and `ir/**/*.irsetup.json`: Lake's + transient compiler setup inputs. Lake writes these inside a compilation action and does not + require them to reuse completed modules. Other JSON files are retained. File-type/link checks + still cover omitted entries; the 100,000-file, 4 GiB unpacked and 1 GiB compressed payload limits + are unchanged. Packing reports retained and omitted counts/sizes, including on a limit miss. - **Kill switch.** Setting the repository variable `DISABLE_BUILD_HANDOFF` to `1` or `true` (`gh variable set DISABLE_BUILD_HANDOFF --body 1`) disables both merge-group staging and `main` restoration without a commit; `scripts/cache_handoff.py` also honors `DISABLE_BUILD_HANDOFF` in diff --git a/scripts/cache_handoff.py b/scripts/cache_handoff.py index 790988582..44eb1b998 100644 --- a/scripts/cache_handoff.py +++ b/scripts/cache_handoff.py @@ -3,8 +3,9 @@ This optional cache never replaces validation. Only the latest current attempt of the authoritative Lean workflow may supply an artifact; misses leave the normal build to run. -The complete root build directory is validated and swapped as a unit, preserving Lake's +Reusable root build outputs are validated and swapped as a unit, preserving Lake's shared hardlinked artifacts and avoiding partially restored module/trace bundles. +Lake's transient module setup inputs are omitted; compilation recreates them when needed. """ from __future__ import annotations @@ -72,6 +73,18 @@ def artifact_name(sha: str, run_id: int, attempt: int) -> str: return f"lean-build-{sha}-{run_id}-{attempt}" +def module_setup_input(path: Path) -> bool: + """Recognize only Lake's module/IR compiler setup inputs, relative to the build directory. + + Lake 4.36's Module.setupFile/irSetupFile use these suffixes under ir/. They are + written inside the compile actions, absent from checkArtifactsExist/getMTime and + ModuleOutputArtifacts, and unnecessary for reusing a completed module build. + Other JSON outputs and every artifact, hash and trace remain in the handoff. + """ + return (len(path.parts) > 1 and path.parts[0] == "ir" + and path.name.endswith((".setup.json", ".irsetup.json"))) + + def pack(root: Path, output: Path, env: dict) -> str: context = source_context(root, env, "merge_group") run_id, attempt = (int(env.get(key, "0")) for key in ("GITHUB_RUN_ID", "GITHUB_RUN_ATTEMPT")) @@ -83,15 +96,24 @@ def pack(root: Path, output: Path, env: dict) -> str: build = root / ".lake/build" directory(build) files = [] + omitted_files = omitted_bytes = 0 for path in sorted(build.rglob("*")): info = path.lstat() if stat.S_ISDIR(info.st_mode): continue require(stat.S_ISREG(info.st_mode), f"Non-regular build output: {path}") + # Validate the file type before omitting anything: setup-named links are + # rejected by the same boundary checks as every other build entry. + if module_setup_input(path.relative_to(build)): + omitted_files += 1 + omitted_bytes += info.st_size + continue files.append((path, info)) total = sum(info.st_size for _, info in files) require(0 < len(files) <= MAX_FILES and 0 < total <= MAX_BYTES, - "Build output count or size is outside handoff limits") + f"Build output count or size is outside handoff limits: {len(files)} files / " + f"{total} bytes (limits {MAX_FILES} files / {MAX_BYTES} bytes; omitted " + f"{omitted_files} module setup inputs / {omitted_bytes} bytes)") output.parent.mkdir(parents=True, exist_ok=True) with tempfile.TemporaryDirectory(prefix="lean-handoff-pack-", dir=output.parent) as temp: stage = Path(temp) @@ -107,7 +129,8 @@ def pack(root: Path, output: Path, env: dict) -> str: with path.open("rb") as source: bundle.addfile(member, source) compressed = archive.stat().st_size - require(compressed <= MAX_ARCHIVE_BYTES, "Handoff archive is too large") + require(compressed <= MAX_ARCHIVE_BYTES, + f"Handoff archive is too large: {compressed} bytes (limit {MAX_ARCHIVE_BYTES})") require(source_context(root, env, "merge_group") == context, "Sources changed while packing the build") metadata = {**context, "producer": {"event": "merge_group", "run_id": run_id, @@ -120,7 +143,9 @@ def pack(root: Path, output: Path, env: dict) -> str: if env.get("GITHUB_OUTPUT"): with Path(env["GITHUB_OUTPUT"]).open("a") as handle: handle.write(f"artifact-name={name}\n") - print(f"Build handoff packed: {len(files)} files, {compressed} bytes ({name})") + print(f"Build handoff packed: {len(files)} files / {total} bytes, " + f"{compressed} compressed bytes; omitted {omitted_files} module setup inputs / " + f"{omitted_bytes} bytes ({name})") return name diff --git a/scripts/test_cache_handoff.py b/scripts/test_cache_handoff.py index e0f3e689d..1c491991f 100644 --- a/scripts/test_cache_handoff.py +++ b/scripts/test_cache_handoff.py @@ -187,6 +187,132 @@ def test_pack_rejects_symlinks_and_empty_build(self): with self.assertRaises(handoff.Rejected): self.pack() + def test_pack_omits_only_module_setup_inputs_after_file_type_checks(self): + omitted = ("ir/Example.setup.json", "ir/Nested/Example.irsetup.json") + retained = ("ir/report.json", "lib/lean/Example.setup.json", "ir/Example.setup.json.hash") + for name in omitted + retained: + path = self.build / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(b"setup input" * 100 if name in omitted else b"retained") + kept = [p for p in self.build.rglob("*") if p.is_file() + and p.relative_to(self.build).as_posix() not in omitted] + total = sum(p.stat().st_size for p in kept) + # The quota still applies to the actual payload; the omitted inputs alone exceed it. + with patch.object(handoff, "MAX_BYTES", total): + self.pack() + with tarfile.open(self.output / "build.tar.gz") as bundle: + names = set(bundle.getnames()) + for name in omitted: + self.assertNotIn(f".lake/build/{name}", names) + self.assertTrue((self.build / name).is_file()) + for name in retained: + self.assertIn(f".lake/build/{name}", names) + inventory = json.loads((self.output / "metadata.json").read_text())["archive"] + self.assertEqual((inventory["files"], inventory["bytes"]), (len(kept), total)) + + for directory in (False, True): + link = self.build / "ir/Linked.setup.json" + link.symlink_to(self.base if directory else self.root / "lakefile.toml", + target_is_directory=directory) + with self.assertRaisesRegex(handoff.Rejected, "Non-regular build output"): + handoff.pack(self.root, self.base / f"links-{directory}", self.env) + link.unlink() + + def test_limit_miss_reports_actual_inventory_and_omission(self): + (self.build / "ir").mkdir() + (self.build / "ir/Example.setup.json").write_bytes(b"setup") + total = sum(p.stat().st_size for p in self.build.rglob("*") + if p.is_file() and not handoff.module_setup_input(p.relative_to(self.build))) + with patch.object(handoff, "MAX_BYTES", 1), self.assertRaises(handoff.Rejected) as error: + self.pack() + self.assertIn(f"3 files / {total} bytes", str(error.exception)) + self.assertIn("limits 100000 files / 1 bytes", str(error.exception)) + self.assertIn("omitted 1 module setup inputs / 5 bytes", str(error.exception)) + self.assertFalse(self.output.exists()) + + def test_setup_inputs_alone_do_not_make_a_nonempty_payload(self): + shutil.rmtree(self.build) + path = self.build / "ir/Example.setup.json" + path.parent.mkdir(parents=True) + path.write_text("setup") + with self.assertRaisesRegex(handoff.Rejected, "0 files / 0 bytes"): + self.pack() + self.assertTrue(path.is_file()) + self.assertFalse(self.output.exists()) + + @unittest.skipUnless(os.environ.get("COMPLEXITYLIB_TEST_LAKE_HANDOFF") == "1", + "real Lake regression runs after Lean installation") + def test_real_lake_reuses_module_and_native_outputs_without_setup_inputs(self): + # No dependencies or shared artifact cache: reuse must come from the handoff itself. + shutil.rmtree(self.build) + (self.root / "lean-toolchain").write_bytes((handoff.ROOT / "lean-toolchain").read_bytes()) + (self.root / "lake-manifest.json").unlink() + (self.root / "lakefile.toml").write_text( + 'name = "handoff_fixture"\nenableArtifactCache = false\n' + '[leanOptions]\ncompiler.postponeCompile = true\n' + '[[lean_lib]]\nname = "Fixture"\n' + '[[lean_exe]]\nname = "fixture"\nroot = "Main"\n') + (self.root / "Fixture").mkdir() + basic = ("module\nnamespace Fixture\n" + "@[noinline] public def twice (n : Nat) : Nat := n + n\nend Fixture\n") + (self.root / "Fixture/Basic.lean").write_text(basic) + (self.root / "Fixture.lean").write_text( + "module\npublic import Fixture.Basic\n" + "namespace Fixture\npublic def answer : Nat := twice 21\nend Fixture\n") + (self.root / "Main.lean").write_text( + "import Fixture\ndef main : IO Unit := IO.println Fixture.answer\n") + env = {**os.environ, "LAKE_CACHE_DIR": str(self.base / "producer-lake-cache"), + "LEAN_NUM_THREADS": "2"} + + def run(*args, cwd=None): + result = subprocess.run(args, cwd=cwd or self.root, env=env, text=True, + capture_output=True, timeout=120) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + return result.stdout + + run("lake", "build", "fixture") + setup = [p.relative_to(self.build) for p in self.build.rglob("*.json") + if handoff.module_setup_input(p.relative_to(self.build))] + self.assertTrue(any(p.name.endswith(".setup.json") for p in setup)) + self.assertTrue(any(p.name.endswith(".irsetup.json") for p in setup)) + for name in ("lib/lean/Fixture/Basic.olean.server", "lib/lean/Fixture/Basic.olean.private", + "lib/lean/Fixture/Basic.ir", "ir/Fixture/Basic.c", "bin/fixture"): + self.assertTrue((self.build / name).is_file(), name) + run("git", "add", ".") + run("git", "-c", "commit.gpgsign=false", "-c", "user.name=Test", + "-c", "user.email=test@example.invalid", "commit", "-qm", "Real Lake fixture") + self.env["GITHUB_SHA"] = run("git", "rev-parse", "HEAD").strip() + self.api = API(self.env["GITHUB_SHA"]) + self.pack() + self.assertTrue(all((self.build / p).is_file() for p in setup)) + + consumer = self.base / "consumer" + run("git", "clone", "--no-local", "-q", str(self.root), str(consumer)) + self.root = consumer + self.build = consumer / ".lake/build" + self.build.parent.mkdir() + env["LAKE_CACHE_DIR"] = str(self.base / "empty-consumer-lake-cache") + self.restore() + self.assertTrue(all(not (self.build / p).exists() for p in setup)) + outputs = {p.relative_to(self.build): (handoff.digest(p), p.stat().st_mtime_ns) + for p in self.build.rglob("*") if p.is_file() and p.suffix != ".hash"} + # --no-build rejects any required rebuild. The ordinary build must also leave the + # compiled modules, IR, executable and saved traces unchanged, without setup inputs. + run("lake", "build", "--no-build", "fixture") + run("lake", "build", "fixture") + self.assertTrue(all(not (self.build / p).exists() for p in setup)) + for name, expected in outputs.items(): + path = self.build / name + self.assertEqual((handoff.digest(path), path.stat().st_mtime_ns), expected, str(name)) + self.assertEqual(run(str(self.build / "bin/fixture")).strip(), "42") + + # A genuine source change still compiles and recreates both kinds of setup input. + (consumer / "Fixture/Basic.lean").write_text(basic.replace("n + n", "n + n + 1")) + run("lake", "build", "fixture") + self.assertTrue((self.build / "ir/Fixture/Basic.setup.json").is_file()) + self.assertTrue((self.build / "ir/Fixture/Basic.irsetup.json").is_file()) + self.assertEqual(run(str(self.build / "bin/fixture")).strip(), "43") + def test_identity_mismatch_or_unsuccessful_run_never_downloads(self): cases = ({"head_sha": "f" * 40}, {"event": "pull_request"}, {"event": "workflow_dispatch"}, {"workflow_id": 8},