Speed up exposition extraction and preserve completed work

.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 }}

.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

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,32 +204,85 @@ 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,
     destinations: tuple[Path, Path],
     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")
-    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
-        ]
-        results = [future.result() for future in futures]
-    combine(results, destinations)
-    prune_cache(cache, results)
-    return results
+    started = time.monotonic()
+    results: list[Extraction] = []
+    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:
+                    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
+        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")
+        except Exception:
+            LOGGER.exception("Could not write failed extraction timings")
+        raise
 
 
 def main() -> None:
@@ -259,17 +312,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),
     )

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"]

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