From 2c9833a63aca25004a3b3f48e5df8c7ed4d57f22 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 8 Oct 2026 09:22:05 -0700 Subject: [PATCH 1/2] Speed up exposition traversal and retain completed extraction work --- .github/workflows/docs.yml | 11 +-- .github/workflows/exposition-verify.yml | 7 +- python/lean_pool/exposition/extract.py | 58 ++++++++++++--- python/tests/test_ci_cache_contract.py | 29 ++++++++ python/tests/test_exposition_extract.py | 74 ++++++++++++++++++++ python/tests/test_exposition_lean_extract.py | 48 +++++++++++++ scripts/exposition/Extract.lean | 33 +++++---- scripts/exposition/tests/EmbeddedNames.lean | 68 ++++++++++++++++++ 8 files changed, 297 insertions(+), 31 deletions(-) create mode 100644 python/tests/test_exposition_lean_extract.py create mode 100644 scripts/exposition/tests/EmbeddedNames.lean diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 1ab56b13c3..24f02beda4 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -251,9 +251,9 @@ jobs: uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/exposition-cache/v1 - key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }} + key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }}-${{ github.run_id }}-${{ github.run_attempt }} restore-keys: | - Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- + Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- - name: Extract declarations # Per-project environments (see extract-all.sh); 2-way parallel to @@ -266,14 +266,17 @@ jobs: exposition-dump.jsonl exposition-commands.jsonl - name: Save project extraction cache - if: steps.extraction-cache.outputs.cache-hit != 'true' + id: extraction-cache-save + # A failed project must not discard its completed siblings. The reader + # accepts only fingerprinted, digest-verified output pairs. + if: always() && steps.extraction-cache.outcome == 'success' && steps.extraction-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/exposition-cache/v1 key: ${{ steps.extraction-cache.outputs.cache-primary-key }} - name: Prune old copies of project extraction cache - if: steps.extraction-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' + if: always() && steps.extraction-cache-save.outcome == 'success' && github.ref == 'refs/heads/main' continue-on-error: true env: GH_TOKEN: ${{ github.token }} diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml index 6e641f7e02..3c48b4bc07 100644 --- a/.github/workflows/exposition-verify.yml +++ b/.github/workflows/exposition-verify.yml @@ -178,9 +178,9 @@ jobs: uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/exposition-cache/v1 - key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }} + key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }}-${{ github.run_id }}-${{ github.run_attempt }} restore-keys: | - Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- + Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- - name: Extract declarations env: @@ -191,7 +191,8 @@ jobs: exposition-dump.jsonl exposition-commands.jsonl - name: Save project extraction cache - if: steps.extraction-cache.outputs.cache-hit != 'true' + # Preserve completed projects if a sibling fails or the job is cancelled. + if: always() && steps.extraction-cache.outcome == 'success' && steps.extraction-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/exposition-cache/v1 diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py index 4c880911c3..94ea4b6a88 100644 --- a/python/lean_pool/exposition/extract.py +++ b/python/lean_pool/exposition/extract.py @@ -16,7 +16,7 @@ import subprocess import tempfile import time -from concurrent.futures import ThreadPoolExecutor +from concurrent.futures import ThreadPoolExecutor, as_completed from dataclasses import asdict, dataclass from pathlib import Path @@ -204,6 +204,30 @@ def prune_cache(cache: Path, results: list[Extraction]) -> None: shutil.rmtree(path) +def write_timings( + destination: Path | None, started: float, results: list[Extraction], state: str +) -> None: + """Keep atomic progress diagnostics even if another project never finishes.""" + if destination is None: + return + destination.parent.mkdir(parents=True, exist_ok=True) + report = { + "seconds": time.monotonic() - started, + "state": state, + "projects": [asdict(item) for item in sorted(results, key=lambda x: x.project)], + } + with tempfile.NamedTemporaryFile( + mode="w", dir=destination.parent, delete=False + ) as output: + temporary = Path(output.name) + try: + output.write(json.dumps(report, default=str, indent=2) + "\n") + output.close() + temporary.replace(destination) + finally: + temporary.unlink(missing_ok=True) + + def run_extraction( root: Path, cache: Path, @@ -211,10 +235,14 @@ def run_extraction( jobs: int = 2, lean: str = "lean", refresh: bool = False, + timings: Path | None = None, ) -> list[Extraction]: """Extract every indexed project, reusing only matching content-addressed data.""" if jobs < 1: raise ValueError("jobs must be positive") + started = time.monotonic() + results: list[Extraction] = [] + write_timings(timings, started, results, "in_progress") names = projects(root) digests: dict[Path, str] = {} fingerprints = {name: fingerprint(root, name, digests) for name in names} @@ -226,9 +254,25 @@ def run_extraction( ) for name in names ] - results = [future.result() for future in futures] + try: + failure: Exception | None = None + for future in as_completed(futures): + try: + results.append(future.result()) + except Exception as error: + failure = failure or error + write_timings( + timings, started, results, "failed" if failure else "in_progress" + ) + if failure is not None: + raise failure + except BaseException: + write_timings(timings, started, results, "failed") + raise + results.sort(key=lambda result: result.project) combine(results, destinations) prune_cache(cache, results) + write_timings(timings, started, results, "complete") return results @@ -259,17 +303,11 @@ def main() -> None: arguments.jobs, arguments.lean, arguments.refresh, - ) - report = { - "seconds": time.monotonic() - started, - "projects": [asdict(item) for item in results], - } - Path(".lake/exposition-timings.json").write_text( - json.dumps(report, default=str, indent=2) + "\n" + Path(".lake/exposition-timings.json"), ) LOGGER.info( "Finished in %.1fs; %d/%d cache hits", - report["seconds"], + time.monotonic() - started, sum(item.cached for item in results), len(results), ) diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 66d337c322..388c8dae4f 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -298,6 +298,35 @@ def test_assembly_restores_projects_once_and_main_owns_full_cache(): assert "github.ref == 'refs/heads/main'" in step["if"] +def test_extraction_caches_survive_failure_and_retry_keys_can_advance(): + """Failed batches save verified siblings; immutable retry keys can gain work.""" + for workflow, job in ( + ("docs.yml", "exposition"), + ("exposition-verify.yml", "verify"), + ): + steps = yaml.safe_load((WORKFLOWS / workflow).read_text())["jobs"][job]["steps"] + names = {step.get("name"): step for step in steps} + restored = names["Restore project extraction cache"] + saved = names["Save project extraction cache"] + assert saved["if"].startswith("always() &&") + assert "steps.extraction-cache.outcome == 'success'" in saved["if"] + assert ( + "${{ github.run_id }}-${{ github.run_attempt }}" in restored["with"]["key"] + ) + assert "github.run_id" not in restored["with"]["restore-keys"] + # Builder/UI/tests do not produce extraction records; their edits must + # still verify minimal files without throwing away valid extraction. + extraction_key = restored["with"]["key"] + assert "scripts/exposition/**" not in extraction_key + assert "scripts/exposition/build-minimal.mjs" not in extraction_key + assert "scripts/exposition/Extract.lean" in extraction_key + assert "scripts/exposition/extract-all.sh" in extraction_key + if workflow == "docs.yml": + pruned = names["Prune old copies of project extraction cache"] + assert "steps.extraction-cache-save.outcome == 'success'" in pruned["if"] + assert "github.ref == 'refs/heads/main'" in pruned["if"] + + def test_minimal_build_wait_does_not_consume_verification_window() -> None: """A cold producer cannot use the verifier's six-hour execution allowance.""" jobs = yaml.safe_load((WORKFLOWS / "exposition-verify.yml").read_text())["jobs"] diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py index c170575800..08305905b4 100644 --- a/python/tests/test_exposition_extract.py +++ b/python/tests/test_exposition_extract.py @@ -5,6 +5,8 @@ import json import subprocess import sys +import time +from concurrent.futures import ThreadPoolExecutor from pathlib import Path import pytest @@ -56,6 +58,7 @@ def _run(root: Path, refresh: bool = False): tuple(root / name for name in OUTPUTS), lean=str(root / "lean"), refresh=refresh, + timings=root / ".lake/exposition-timings.json", ) @@ -169,6 +172,77 @@ def test_invalid_jsonl_is_not_cached(repository: Path) -> None: ) +def test_partial_batch_reuses_completed_project_after_failure(repository: Path) -> None: + """A retry preserves verified siblings without accepting the failed project.""" + _run(repository) + published = _outputs(repository) + executable = repository / "lean" + executable.write_text( + executable.read_text().replace( + "if pathlib.Path('fail').exists(): raise SystemExit(1)", + "if pathlib.Path('fail').exists() and module == 'LeanPool.B': " + "raise SystemExit(1)", + ) + ) + for name in ("A", "B"): + (repository / f"LeanPool/{name}.lean").write_text(f"-- {name} changed\n") + (repository / "fail").touch() + with pytest.raises(subprocess.CalledProcessError): + _run(repository) + assert _outputs(repository) == published + report = json.loads((repository / ".lake/exposition-timings.json").read_text()) + assert report["state"] == "failed" + assert [item["project"] for item in report["projects"]] == ["A"] + (repository / "fail").unlink() + assert [item.cached for item in _run(repository)] == [True, False] + calls = (repository / "calls").read_text().splitlines() + assert calls.count("LeanPool.A") == 2 + assert calls.count("LeanPool.B") == 3 + recovered = _outputs(repository) + _run(repository, refresh=True) + assert _outputs(repository) == recovered + + +def test_timings_record_completed_sibling_before_batch_finishes( + repository: Path, +) -> None: + """Cancellation can leave useful progress even while a project is stalled.""" + executable = repository / "lean" + executable.write_text( + executable.read_text().replace( + "source = pathlib.Path", + "import time\n" + "deadline = time.monotonic() + 5\n" + "while module == 'LeanPool.B' and not pathlib.Path('release').exists():\n" + " if time.monotonic() > deadline: raise SystemExit(1)\n" + " time.sleep(0.01)\n" + "source = pathlib.Path", + ) + ) + with ThreadPoolExecutor(max_workers=1) as executor: + future = executor.submit(_run, repository) + try: + deadline = time.monotonic() + 4 + while time.monotonic() < deadline: + report_path = repository / ".lake/exposition-timings.json" + if report_path.exists(): + report = json.loads(report_path.read_text()) + if report["projects"]: + break + time.sleep(0.01) + else: + pytest.fail("completed project was missing from progress diagnostics") + assert report["state"] == "in_progress" + assert [item["project"] for item in report["projects"]] == ["A"] + assert not future.done() + finally: + (repository / "release").touch() + future.result(timeout=5) + complete = json.loads(report_path.read_text()) + assert complete["state"] == "complete" + assert [item["project"] for item in complete["projects"]] == ["A", "B"] + + def test_empty_extraction_is_not_cached(repository: Path) -> None: """A successful exit with no records is a failed extraction, never a cache entry.""" executable = repository / "lean" diff --git a/python/tests/test_exposition_lean_extract.py b/python/tests/test_exposition_lean_extract.py new file mode 100644 index 0000000000..31292796c9 --- /dev/null +++ b/python/tests/test_exposition_lean_extract.py @@ -0,0 +1,48 @@ +"""Check the real pinned-Lean extractor on shared expressions and small oracles.""" + +from __future__ import annotations + +import os +import subprocess +from pathlib import Path + +import pytest + +ROOT = Path(__file__).resolve().parents[2] + + +def test_embedded_names_preserve_semantics_without_expanding_shared_nodes( + tmp_path, monkeypatch +): + """Compile the actual extractor, then compare name sets and detect DAG replay.""" + toolchain = (ROOT / "lean-toolchain").read_text().strip() + lean = ( + Path.home() + / ".elan/toolchains" + / toolchain.replace(":", "---").replace("/", "--") + / "bin/lean" + ) + if not lean.exists(): + if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1": + pytest.fail(f"required pinned Lean toolchain unavailable: {toolchain}") + pytest.skip("pinned Lean toolchain unavailable") + script = ROOT / "scripts/exposition/Extract.lean" + subprocess.run( + [str(lean), "-o", str(tmp_path / "Extract.olean"), script.name], + cwd=script.parent, + capture_output=True, + text=True, + check=True, + timeout=60, + ) + monkeypatch.setenv("LEAN_PATH", str(tmp_path)) + result = subprocess.run( + [str(lean), str(script.parent / "tests/EmbeddedNames.lean")], + cwd=ROOT, + capture_output=True, + text=True, + check=False, + timeout=30, + ) + assert result.returncode == 0, result.stdout + result.stderr + assert "shared-expression regression passed" in result.stdout diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean index 085ced77eb..9aab17184d 100644 --- a/scripts/exposition/Extract.lean +++ b/scripts/exposition/Extract.lean @@ -158,20 +158,16 @@ partial def evalNameExpr? (e : Expr) : Option Name := do | _ => none | _ => none -/-- Every `Name` value embedded anywhere in `e`. -/ -partial def collectEmbeddedNames (e : Expr) : Array Name := Id.run do - let mut acc : Array Name := #[] - if let some n := evalNameExpr? e then acc := acc.push n - match e with - | .app f a => return acc ++ collectEmbeddedNames f ++ collectEmbeddedNames a - | .lam _ t b _ => return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames b - | .forallE _ t b _ => return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames b - | .letE _ t v b _ => - return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames v - ++ collectEmbeddedNames b - | .mdata _ b => return acc ++ collectEmbeddedNames b - | .proj _ _ b => return acc ++ collectEmbeddedNames b - | _ => return acc +/-- Every embedded `Name`, visiting shared expression nodes only once. +Lean expressions are DAGs: expanding a shared subtree at every occurrence can +take exponential time even when its serialized expression is small. The +notation scan only needs membership, so repeated occurrences add no evidence. -/ +def collectEmbeddedNames (e : Expr) : Array Name := runST fun world => do + let names ← ST.mkRef (σ := world) (#[] : Array Name) + e.forEach (ω := world) (m := ST world) fun expression => do + if let some name := evalNameExpr? expression then + names.modify (·.push name) + names.get /-- Expand a seed set of used constants, tunnelling through generated pool auxiliaries, until exposed pool declarations (edges) or non-pool constants @@ -801,16 +797,25 @@ public unsafe def main (args : List String) : IO UInt32 := do -- them, parse-error recovery silently truncates commands. Lean.enableInitializersExecution let imports := modules.toArray.map fun module => ({ module } : Lean.Import) + let importStarted ← IO.monoMsNow + IO.eprintln s!"exposition: importing {modules}" let env ← Lean.importModules imports {} (trustLevel := 1024) (loadExts := true) + IO.eprintln s!"exposition: imports loaded in {(← IO.monoMsNow) - importStarted}ms" let coreContext : Lean.Core.Context := { fileName := "", fileMap := default, maxHeartbeats := 0 } let run : Lean.CoreM Unit := do + let declarationsStarted ← IO.monoMsNow let (exposed, names) ← Exposition.exposedDecls env + IO.eprintln s!"exposition: indexed {names.size} declarations in {(← IO.monoMsNow) - declarationsStarted}ms" + let dependenciesStarted ← IO.monoMsNow Exposition.extract outPath exposed names + IO.eprintln s!"exposition: declaration dependencies written in {(← IO.monoMsNow) - dependenciesStarted}ms" + let commandsStarted ← IO.monoMsNow Exposition.Commands.emitCommands commandsPath exposed names + IO.eprintln s!"exposition: command tables written in {(← IO.monoMsNow) - commandsStarted}ms" let (result, _) ← run.toIO coreContext { env } let _ := result return 0 diff --git a/scripts/exposition/tests/EmbeddedNames.lean b/scripts/exposition/tests/EmbeddedNames.lean new file mode 100644 index 0000000000..1041dea2e7 --- /dev/null +++ b/scripts/exposition/tests/EmbeddedNames.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vasily Ilin +-/ + +module + +import all Extract + +open Lean + +namespace ExpositionTests + +/-- The previous tree traversal provides a semantic oracle on small inputs. -/ +partial def treeNames (e : Expr) : Array Name := Id.run do + let mut names := #[] + if let some name := Exposition.evalNameExpr? e then names := names.push name + match e with + | .app f a => return names ++ treeNames f ++ treeNames a + | .lam _ t b _ => return names ++ treeNames t ++ treeNames b + | .forallE _ t b _ => return names ++ treeNames t ++ treeNames b + | .letE _ t v b _ => return names ++ treeNames t ++ treeNames v ++ treeNames b + | .mdata _ b => return names ++ treeNames b + | .proj _ _ b => return names ++ treeNames b + | _ => return names + +def normalize (names : Array Name) : List String := + (names.toList.map Name.toString).eraseDups.mergeSort (· ≤ ·) + +def sharedExpression (depth : Nat) (leaf : Expr) : Expr := Id.run do + let mut expression := leaf + for _ in [:depth] do + expression := mkApp2 (mkConst `pair) expression expression + return expression + +def check : IO Unit := do + let anonymous := mkConst ``Name.anonymous + let short := mkApp (mkConst ``Name.mkStr1) (mkStrLit "payload") + let nested := mkApp2 (mkConst ``Name.str) short (mkStrLit "child") + let numbered := mkApp2 (mkConst ``Name.num) nested (mkNatLit 7) + let expressions := #[ + anonymous, short, nested, numbered, + mkApp2 (mkConst ``Name.mkNum) nested (mkNatLit 9), + mkApp2 (mkConst ``Name.mkStr2) (mkStrLit "one") (mkStrLit "two"), + mkApp3 (mkConst ``Name.mkStr3) (mkStrLit "one") (mkStrLit "two") (mkStrLit "three"), + mkApp4 (mkConst ``Name.mkStr4) (mkStrLit "one") (mkStrLit "two") + (mkStrLit "three") (mkStrLit "four"), + mkLambda `binder .default short numbered, + mkForall `binder .default nested numbered, + mkLet `binder short nested numbered, + mkMData {} numbered, + mkProj `structure 0 numbered + ] + for expression in expressions do + for depth in [:8] do + let value := sharedExpression depth expression + unless normalize (Exposition.collectEmbeddedNames value) == normalize (treeNames value) do + throw <| IO.userError "memoized traversal lost an embedded name" + -- Only 18 pair nodes are stored, although the expanded tree has 262144 leaves. + let found := Exposition.collectEmbeddedNames (sharedExpression 18 short) + unless found == #[`payload] do + throw <| IO.userError s!"shared expressions were expanded repeatedly: {found.size} names" + IO.println "embedded-name semantics and shared-expression regression passed" + +end ExpositionTests + +#eval ExpositionTests.check From 87d852861fe6e18731e3a5befa6c07b600f13704 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 8 Oct 2026 17:41:46 +0000 Subject: [PATCH 2/2] Fix exposition failure diagnostics and enforce the pinned Lean regression Cover discovery, fingerprinting, publication, and pruning failures; exercise the real expression oracle in the existing selected Lean test file. reviewer-source-repair-619-2c9833-diagnostics-and-Lean-oracle-v1 --- python/lean_pool/exposition/extract.py | 49 +++++++----- python/tests/test_ci_pr_build.py | 31 ++++++++ python/tests/test_exposition_extract.py | 84 ++++++++++++++++++++ python/tests/test_exposition_lean_extract.py | 48 ----------- 4 files changed, 144 insertions(+), 68 deletions(-) delete mode 100644 python/tests/test_exposition_lean_extract.py diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py index 94ea4b6a88..2919f6d079 100644 --- a/python/lean_pool/exposition/extract.py +++ b/python/lean_pool/exposition/extract.py @@ -242,19 +242,25 @@ def run_extraction( raise ValueError("jobs must be positive") started = time.monotonic() results: list[Extraction] = [] - write_timings(timings, started, results, "in_progress") - names = projects(root) - digests: dict[Path, str] = {} - fingerprints = {name: fingerprint(root, name, digests) for name in names} - LOGGER.info("Extracting %d projects (%d at a time)", len(names), jobs) - with ThreadPoolExecutor(max_workers=jobs) as executor: - futures = [ - executor.submit( - extract_project, root, cache, name, fingerprints[name], lean, refresh - ) - for name in names - ] - try: + try: + write_timings(timings, started, results, "in_progress") + names = projects(root) + digests: dict[Path, str] = {} + fingerprints = {name: fingerprint(root, name, digests) for name in names} + LOGGER.info("Extracting %d projects (%d at a time)", len(names), jobs) + with ThreadPoolExecutor(max_workers=jobs) as executor: + futures = [ + executor.submit( + extract_project, + root, + cache, + name, + fingerprints[name], + lean, + refresh, + ) + for name in names + ] failure: Exception | None = None for future in as_completed(futures): try: @@ -266,14 +272,17 @@ def run_extraction( ) if failure is not None: raise failure - except BaseException: + results.sort(key=lambda result: result.project) + combine(results, destinations) + prune_cache(cache, results) + write_timings(timings, started, results, "complete") + return results + except BaseException: + try: write_timings(timings, started, results, "failed") - raise - results.sort(key=lambda result: result.project) - combine(results, destinations) - prune_cache(cache, results) - write_timings(timings, started, results, "complete") - return results + except Exception: + LOGGER.exception("Could not write failed extraction timings") + raise def main() -> None: diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index 94e701f232..ae50034c65 100644 --- a/python/tests/test_ci_pr_build.py +++ b/python/tests/test_ci_pr_build.py @@ -455,3 +455,34 @@ def test_required_toolchain_cannot_be_silently_skipped(monkeypatch): monkeypatch.setattr(Path, "is_file", lambda path: False) with pytest.raises(pytest.fail.Exception, match="required pinned Lean"): _lake() + + +def test_lake_exposition_embedded_names_preserve_semantics_without_dag_replay( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """The required pinned-Lean lane exercises the actual shared-expression oracle.""" + root = Path(__file__).resolve().parents[2] + lean = _lake().with_name("lean") + script = root / "scripts/exposition/Extract.lean" + subprocess.run( + [str(lean), "-j2", "-o", str(tmp_path / "Extract.olean"), script.name], + cwd=script.parent, + capture_output=True, + text=True, + check=True, + timeout=60, + ) + monkeypatch.setenv("LEAN_PATH", str(tmp_path)) + result = subprocess.run( + [str(lean), "-j2", str(script.parent / "tests/EmbeddedNames.lean")], + cwd=root, + capture_output=True, + text=True, + check=False, + timeout=30, + ) + assert result.returncode == 0, result.stdout + result.stderr + assert ( + "embedded-name semantics and shared-expression regression passed" + in result.stdout + ) diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py index 08305905b4..9e7d3dbebd 100644 --- a/python/tests/test_exposition_extract.py +++ b/python/tests/test_exposition_extract.py @@ -11,6 +11,7 @@ import pytest +from lean_pool.exposition import extract as extraction from lean_pool.exposition.extract import GLOBAL_INPUTS, OUTPUTS, run_extraction @@ -267,3 +268,86 @@ def test_additional_source_invalidates_project(repository: Path) -> None: directory.mkdir() (directory / "New.lean").write_text("-- new module\n") assert [item.cached for item in _run(repository)] == [False, True] + + +@pytest.mark.parametrize( + ("path", "exception", "message"), + [ + ("LeanPool/A.lean", ValueError, "existing project entry modules"), + ("scripts/exposition/Extract.lean", FileNotFoundError, r"Extract\.lean"), + ], +) +def test_pre_worker_failure_marks_timings_failed( + repository: Path, path: str, exception: type[Exception], message: str +) -> None: + """Discovery and fingerprint errors fail before any extraction can start.""" + (repository / path).unlink() + with pytest.raises(exception, match=message): + _run(repository) + report = json.loads((repository / ".lake/exposition-timings.json").read_text()) + assert report["state"] == "failed" + assert report["projects"] == [] + assert not (repository / "calls").exists() + assert not any((repository / name).exists() for name in OUTPUTS) + + +@pytest.mark.parametrize("stage", ["combine", "prune"]) +def test_publication_failure_preserves_completed_project_diagnostics( + repository: Path, monkeypatch: pytest.MonkeyPatch, stage: str +) -> None: + """An actual publication or pruning I/O failure retains completed projects.""" + _run(repository) + published = _outputs(repository) + failure = OSError(f"{stage} I/O failure") + if stage == "combine": + replace = Path.replace + + def reject_publication(path, target): + if Path(target) == repository / OUTPUTS[0]: + raise failure + return replace(path, target) + + monkeypatch.setattr(Path, "replace", reject_publication) + else: + obsolete = repository / ".lake/exposition-cache/v1/obsolete/generation" + obsolete.mkdir(parents=True) + remove = extraction.shutil.rmtree + + def reject_pruning(path, *arguments, **keywords): + if Path(path) == obsolete: + raise failure + return remove(path, *arguments, **keywords) + + monkeypatch.setattr(extraction.shutil, "rmtree", reject_pruning) + with pytest.raises(OSError, match=f"{stage} I/O failure") as error: + _run(repository) + assert error.value is failure + report = json.loads((repository / ".lake/exposition-timings.json").read_text()) + assert report["state"] == "failed" + assert [item["project"] for item in report["projects"]] == ["A", "B"] + assert all(item["cached"] for item in report["projects"]) + assert _outputs(repository) == published + + +def test_failed_timing_write_cannot_replace_original_failure( + repository: Path, monkeypatch: pytest.MonkeyPatch, caplog: pytest.LogCaptureFixture +) -> None: + """Failure diagnostics are best effort when their destination also fails.""" + failure = ValueError("original discovery failure") + write_timings = extraction.write_timings + + def reject_discovery(root): + raise failure + + def reject_failed_timings(destination, started, results, state): + if state == "failed": + raise OSError("timings destination unavailable") + write_timings(destination, started, results, state) + + monkeypatch.setattr(extraction, "projects", reject_discovery) + monkeypatch.setattr(extraction, "write_timings", reject_failed_timings) + with pytest.raises(ValueError, match="original discovery failure") as error: + _run(repository) + assert error.value is failure + assert "Could not write failed extraction timings" in caplog.text + assert not (repository / "calls").exists() diff --git a/python/tests/test_exposition_lean_extract.py b/python/tests/test_exposition_lean_extract.py deleted file mode 100644 index 31292796c9..0000000000 --- a/python/tests/test_exposition_lean_extract.py +++ /dev/null @@ -1,48 +0,0 @@ -"""Check the real pinned-Lean extractor on shared expressions and small oracles.""" - -from __future__ import annotations - -import os -import subprocess -from pathlib import Path - -import pytest - -ROOT = Path(__file__).resolve().parents[2] - - -def test_embedded_names_preserve_semantics_without_expanding_shared_nodes( - tmp_path, monkeypatch -): - """Compile the actual extractor, then compare name sets and detect DAG replay.""" - toolchain = (ROOT / "lean-toolchain").read_text().strip() - lean = ( - Path.home() - / ".elan/toolchains" - / toolchain.replace(":", "---").replace("/", "--") - / "bin/lean" - ) - if not lean.exists(): - if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1": - pytest.fail(f"required pinned Lean toolchain unavailable: {toolchain}") - pytest.skip("pinned Lean toolchain unavailable") - script = ROOT / "scripts/exposition/Extract.lean" - subprocess.run( - [str(lean), "-o", str(tmp_path / "Extract.olean"), script.name], - cwd=script.parent, - capture_output=True, - text=True, - check=True, - timeout=60, - ) - monkeypatch.setenv("LEAN_PATH", str(tmp_path)) - result = subprocess.run( - [str(lean), str(script.parent / "tests/EmbeddedNames.lean")], - cwd=ROOT, - capture_output=True, - text=True, - check=False, - timeout=30, - ) - assert result.returncode == 0, result.stdout + result.stderr - assert "shared-expression regression passed" in result.stdout