From 15f79dee80a231bf0ed1cefa0ecb1ece3ff31af1 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 6 Nov 2026 10:13:50 -0800 Subject: [PATCH 1/3] Keep docs and exposition progress across routine pool changes Every infrastructure edit since the v4.35 bump restarted documentation analysis (~8 h for 31k modules) and exposition extraction (~3 h) from zero: their cache keys hashed `lakefile.toml`, the docs cursor hashed every source file plus helper scripts, and neither could restore across those changes. On main the analysis therefore never finished, and the site has not deployed since Oct 13. Docs: record completion per project, fingerprinted by the project's sources and Lake's compiled-module content hashes over its local import closure (Lake's setup inventories, so cross-project imports count). Unchanged projects are not sent to Lake again. Only toolchain, dependency, doc-gen and link-policy changes restart everything. Modules deleted from the pool are pruned from doc-gen's database (it cascades from `modules`) together with their markers. Import ordering is parsed only for projects with work left. Exposition: fingerprint compiled-module hashes instead of `lakefile.toml`, and let the extraction cache restore from any earlier generation; per-project fingerprints already decide validity. Missing inventories or compiled hashes fall back to the old, conservative behaviour. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/docs-build.yml | 6 +- .github/workflows/docs-publish.yml | 1 + .github/workflows/exposition-verify.yml | 1 + docbuild/README.md | 18 +- python/lean_pool/documentation.py | 244 +++++++++++++++++++----- python/lean_pool/exposition/extract.py | 25 ++- python/tests/test_documentation.py | 149 +++++++++++++-- python/tests/test_exposition_extract.py | 37 +++- 8 files changed, 404 insertions(+), 77 deletions(-) diff --git a/.github/workflows/docs-build.yml b/.github/workflows/docs-build.yml index 7574c8d55d..4babc6cbf4 100644 --- a/.github/workflows/docs-build.yml +++ b/.github/workflows/docs-build.yml @@ -60,6 +60,8 @@ jobs: }}-${{ inputs.build_revision }} restore-keys: | LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + # Keyed only by inputs that change every page. Per-project progress inside + # the checkpoint decides which projects a pool edit sends back to Lake. - name: Restore documentation checkpoint id: docs-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -71,11 +73,11 @@ jobs: .lake/packages/UnicodeBasic .lake/packages/BibtexQuery .lake/packages/MD4Lean - key: DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', + key: DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ github.run_id }}-${{ github.run_attempt }}-${{ inputs.stage }} restore-keys: | - DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}- + DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}- - name: Install Lean uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 with: diff --git a/.github/workflows/docs-publish.yml b/.github/workflows/docs-publish.yml index 88cfa07073..449b8dd855 100644 --- a/.github/workflows/docs-publish.yml +++ b/.github/workflows/docs-publish.yml @@ -97,6 +97,7 @@ jobs: }} restore-keys: | 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') }}- + Exposition-v1-${{ runner.os }}- - name: Extract declarations env: LEAN_CMD: /home/runner/.elan/bin/lean diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml index 432829f523..7a28c42fde 100644 --- a/.github/workflows/exposition-verify.yml +++ b/.github/workflows/exposition-verify.yml @@ -189,6 +189,7 @@ jobs: 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/Extract.lean', 'scripts/exposition/extract-all.sh', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}- + Exposition-v1-${{ runner.os }}- - name: Extract declarations env: diff --git a/docbuild/README.md b/docbuild/README.md index ecff8ef95a..06e3164eee 100644 --- a/docbuild/README.md +++ b/docbuild/README.md @@ -27,10 +27,18 @@ analysis, it records external names from dependency environments and renders all local module records directly from the database. Four sequential analysis stages each allow 90 minutes of analysis. They restore -the newest checkpoint compatible with the pinned dependencies, then process -modules in dependency order in batches of 128. Each successful batch advances a -cursor tied to all source files, configuration and linking policy. Changes reset -that cursor while retaining Lake's ordinary per-module trace checking. +the newest checkpoint compatible with the toolchain, dependency and doc-gen pins, +then process modules in dependency order in batches of 128. The checkpoint +records each completed project with a fingerprint of its sources and Lake's +content hashes of its compiled modules, including modules it imports from +other projects (read from Lake's per-module import inventories). Unchanged +projects are not handed to Lake again, so a merge re-analyzes only the projects +it touched and their importers, and a pool option change re-analyzes only +projects whose compiled modules changed. Changes +to the toolchain, dependency pins, doc-gen or linking policy restart every +project; Lake's per-module traces still apply to every project it is given. +Modules deleted from the pool are removed from the database together with +their markers before analysis. Before each batch, the runner snapshots the database and its markers. If the batch times out, its process group is stopped and that pair is restored before @@ -64,5 +72,5 @@ PYTHONPATH=python python3 -m lean_pool.documentation render Repeat `batch` until complete before running `render`. Preserve the whole `docbuild/.lake/build` tree together: a marker alone does not contain its SQLite -documentation data. Workflow artifacts retain analysis cursors for diagnosis; +documentation data. Workflow artifacts retain analysis progress for diagnosis; GitHub Actions reports publishing failures separately from PR validation. diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py index 4a2858ce3a..37ff764a5f 100644 --- a/python/lean_pool/documentation.py +++ b/python/lean_pool/documentation.py @@ -1,9 +1,11 @@ """Build resumable local API documentation outside pull-request CI. -Only successful batches advance the cursor. A timed-out or failed subprocess -is stopped together with its children before its database and Lake markers are -rolled back to the preceding consistent checkpoint. Lake still checks its own -traces when a new source snapshot invalidates the cursor. +Progress is recorded per project: a project whose sources and compiled modules +are unchanged is never handed to Lake again, so routine merges, option edits and +helper changes do not restart the whole pool. Only successful batches record +progress. A timed-out or failed subprocess is stopped together with its children +before its database and Lake markers are rolled back to the preceding consistent +checkpoint. Lake still checks its own traces for every project it is given. """ from __future__ import annotations @@ -32,7 +34,16 @@ r"(?m)^\s*(?:(?:public|private|meta)\s+)*import\s+(?:all\s+)?([^\n]+)" ) STATE = "documentation-progress.json" +# Bump when stored analysis must be discarded, e.g. a changed database contract. +STATE_VERSION = 2 TOOLCHAIN_ROOTS = frozenset({"Init", "Std", "Lean", "Lake"}) +COMPILED = Path(".lake/build/lib/lean") +IR = Path(".lake/build/ir") +LINK_POLICY = ( + "DOCGEN_LOCAL_MODULE_ROOTS", + "DOCGEN_DEPS_DOCS_URL", + "DOCGEN_DEPS_DOCS_URLS", +) def module_sources(root: Path) -> dict[str, Path]: @@ -43,39 +54,119 @@ def module_sources(root: Path) -> dict[str, Path]: } -def input_identity(root: Path) -> str: - """Invalidate the cursor on changes to sources, pins, helpers or link policy.""" - digest = hashlib.sha256() - paths = [ - *module_sources(root).values(), - *( - root / name - for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json") - ), - *( - root / "docbuild" / name - for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json") - ), - Path(__file__), - Path(__file__).with_name("indexes.py"), - Path(__file__).parent / "exposition" / "source_text.py", - ] - for path in paths: - name = path.relative_to(root) if path.is_relative_to(root) else Path(path.name) - digest.update(str(name).encode()) +def _digest_files(digest, root: Path, paths: list[Path]) -> None: + for path in sorted(paths): + digest.update(str(path.relative_to(root)).encode()) digest.update(b"\0" + path.read_bytes() + b"\0") - for name in ( - "DOCGEN_LOCAL_MODULE_ROOTS", - "DOCGEN_DEPS_DOCS_URL", - "DOCGEN_DEPS_DOCS_URLS", - ): + + +def input_identity(root: Path) -> str: + """Name the toolchain, dependency, doc-gen and link-policy inputs of every page. + + The pool's own `lakefile.toml` is left out: its options reach the analysis + only through compiled modules, which `project_fingerprints` hashes directly. + """ + digest = hashlib.sha256(f"version={STATE_VERSION}\0".encode()) + _digest_files( + digest, + root, + [ + root / "lean-toolchain", + root / "lake-manifest.json", + *( + root / "docbuild" / name + for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json") + ), + ], + ) + for name in LINK_POLICY: digest.update(name.encode() + b"=" + os.environ.get(name, "").encode() + b"\0") return digest.hexdigest() -def ordered_modules(root: Path) -> list[str]: - """Visit dependencies first so one target cannot hide an unbounded cold closure.""" +def project_of(module: str) -> str: + """Group `LeanPool....` modules; the empty library root is its own.""" + parts = module.split(".") + return parts[1] if len(parts) > 1 else "" + + +def local_closure(root: Path, project: str, modules: set[str]) -> set[str] | None: + """Read the project's local transitive imports from Lake's setup files. + + The entry module and `Imports` aggregate together import every project + source, so their inventories cover modules borrowed from other projects. + Return None unless they cover all of the project's own modules. + """ + entry = "LeanPool" + (f".{project}" if project else "") + own = {module for module in modules if project_of(module) == project} + closure = own & {entry, f"{entry}.Imports"} + for module in sorted(closure): + setup = root / IR / (module.replace(".", "/") + ".setup.json") + try: + inventory = json.loads(setup.read_text()) + if inventory["name"] != module or not isinstance( + inventory["importArts"], dict + ): + return None + except (OSError, ValueError, KeyError, TypeError): + return None + closure |= modules & set(inventory["importArts"]) + return closure if own <= closure else None + + +def project_fingerprints(root: Path) -> dict[str, str]: + """Hash the sources and compiled modules each project's pages depend on. + + That is the project's modules plus every pool module they import, from other + projects too. Without Lake's import inventory the whole pool is included; + without its compiled-module hashes the pool configuration stands in for them. + """ sources = module_sources(root) + modules = set(sources) + configuration = hashlib.sha256((root / "lakefile.toml").read_bytes()).hexdigest() + digests = {} + for module, path in sources.items(): + compiled = root / COMPILED / path.relative_to(root).with_suffix(".olean.hash") + source = hashlib.sha256(path.read_bytes()).hexdigest() + digests[module] = ( + source, + compiled.read_text().strip() if compiled.is_file() else None, + ) + fingerprints = {} + for project in sorted({project_of(module) for module in modules}): + closure = local_closure(root, project, modules) or modules + entries = {module: digests[module] for module in sorted(closure)} + if any(compiled is None for _, compiled in entries.values()): + entries["lakefile.toml"] = (configuration, None) + encoded = json.dumps(entries, sort_keys=True).encode() + fingerprints[project] = hashlib.sha256(encoded).hexdigest() + return fingerprints + + +def read_progress(build: Path, identity: str) -> dict[str, str]: + """Return completed project fingerprints saved under the same shared inputs.""" + path = build / STATE + state = json.loads(path.read_text()) if path.exists() else {} + if state.get("identity") != identity: + return {} + projects = state.get("projects") + if not isinstance(projects, dict): + raise ValueError("invalid documentation checkpoint progress") + return projects + + +def ordered_modules(root: Path, projects: set[str] | None = None) -> list[str]: + """Visit dependencies first so one target cannot hide an unbounded cold closure. + + Restricting to `projects` skips parsing the rest. Lake still fetches the + analysis of any module imported from another project; that project's own + record says whether its pages are already current. + """ + sources = { + name: path + for name, path in module_sources(root).items() + if projects is None or project_of(name) in projects + } graph = {} for name, path in sources.items(): imports = { @@ -137,6 +228,35 @@ def compiled_dependencies(root: Path) -> list[str]: ] +def prune_modules(build: Path, modules: set[str]) -> list[str]: + """Delete analysis of local modules that no longer exist, with their markers. + + doc-gen cascades every table from `modules`. Removing the marker too keeps a + module that later reappears unchanged from being skipped by Lake's trace. + """ + database = build / "api-docs.db" + if not database.is_file(): + return [] + with sqlite3.connect(database) as connection: + connection.execute("PRAGMA foreign_keys = ON") + stored = [ + name + for (name,) in connection.execute( + "SELECT name FROM modules WHERE name = 'LeanPool' " + "OR name LIKE 'LeanPool.%'" + ) + ] + stale = sorted(set(stored) - modules) + connection.executemany( + "DELETE FROM modules WHERE name = ?", [(name,) for name in stale] + ) + connection.close() + for name in stale: + for marker in (build / "doc-data").glob(f"{name}.doc*"): + marker.unlink() + return stale + + def validate_database(build: Path) -> None: """Check a closed batch's SQLite state before retaining it.""" database = build / "api-docs.db" @@ -207,21 +327,36 @@ def run_build(command: list[str], directory: Path, timeout: float) -> None: def build_batches(root: Path, lake: str, seconds: float, batch_size: int) -> bool: - """Advance verified module batches until complete or the time allowance ends.""" + """Analyze changed projects in verified batches until done or out of time.""" if seconds <= 0 or batch_size <= 0: raise ValueError("batch size and time allowance must be positive") build = root / "docbuild" / ".lake" / "build" - state_path = build / STATE identity = input_identity(root) - modules = ordered_modules(root) - state = json.loads(state_path.read_text()) if state_path.exists() else {} - cursor = state.get("cursor", 0) if state.get("identity") == identity else 0 - if not isinstance(cursor, int) or not 0 <= cursor <= len(modules): - raise ValueError("invalid documentation checkpoint cursor") - started = cursor + fingerprints = project_fingerprints(root) + done = { + project: value + for project, value in read_progress(build, identity).items() + if fingerprints.get(project) == value + } + with batch_checkpoint(build): + if stale := prune_modules(build, set(module_sources(root))): + validate_database(build) + LOGGER.info("Removed %s deleted modules", len(stale)) + pending = ordered_modules(root, set(fingerprints) - set(done)) + remaining: dict[str, int] = {} + for module in pending: + remaining[project_of(module)] = remaining.get(project_of(module), 0) + 1 + LOGGER.info( + "Documentation analysis: %s/%s projects reused, %s modules to check", + len(done), + len(fingerprints), + len(pending), + ) + write_progress(build, identity, done) deadline = time.monotonic() + seconds - while cursor < len(modules) and time.monotonic() < deadline: - batch = modules[cursor : cursor + batch_size] + position = 0 + while position < len(pending) and time.monotonic() < deadline: + batch = pending[position : position + batch_size] command = [lake, "build", *(f"+{name}:docInfo" for name in batch)] try: with batch_checkpoint(build): @@ -230,24 +365,33 @@ def build_batches(root: Path, lake: str, seconds: float, batch_size: int) -> boo ) validate_database(build) except subprocess.TimeoutExpired: - if cursor == started: + if position == 0: raise RuntimeError( "no batch completed within the time allowance" ) from None break - cursor += len(batch) - state_path.write_text( - json.dumps({"identity": identity, "cursor": cursor}) + "\n" - ) - LOGGER.info("Documentation analysis: %s/%s modules", cursor, len(modules)) - return cursor == len(modules) + position += len(batch) + for module in batch: + project = project_of(module) + remaining[project] -= 1 + if not remaining[project]: + done[project] = fingerprints[project] + write_progress(build, identity, done) + LOGGER.info("Documentation analysis: %s/%s modules", position, len(pending)) + return done == fingerprints + + +def write_progress(build: Path, identity: str, done: dict[str, str]) -> None: + """Record completed projects, dropping those that no longer exist.""" + build.mkdir(parents=True, exist_ok=True) + state = {"identity": identity, "projects": dict(sorted(done.items()))} + (build / STATE).write_text(json.dumps(state) + "\n") def require_complete(root: Path) -> None: """Refuse to render or publish an incomplete or different source snapshot.""" build = root / "docbuild" / ".lake" / "build" - state = json.loads((build / STATE).read_text()) - if state != {"identity": input_identity(root), "cursor": len(module_sources(root))}: + if read_progress(build, input_identity(root)) != project_fingerprints(root): raise ValueError("documentation analysis is incomplete for this snapshot") validate_database(build) diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py index 2919f6d079..ff49a02678 100644 --- a/python/lean_pool/exposition/extract.py +++ b/python/lean_pool/exposition/extract.py @@ -28,13 +28,17 @@ GLOBAL_INPUTS = ( "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", ) +# Build options reach the extractor only through compiled modules, so Lake's +# content hashes stand in for them. Without those hashes, fall back to the file. +BUILD_CONFIGURATION = "lakefile.toml" +COMPILED = Path(".lake/build/lib/lean") + def file_digest(path: Path) -> str: """Hash a file without loading large extraction outputs into memory.""" @@ -87,9 +91,24 @@ def project_sources(root: Path, project: str) -> set[Path]: return sources +def compiled_hashes(root: Path, sources: set[Path]) -> set[Path] | None: + """Locate Lake's content hash of each source's compiled module, if all exist.""" + paths = { + root / COMPILED / source.relative_to(root).with_suffix(".olean.hash") + for source in sources + } + return paths if all(path.is_file() for path in paths) else None + + def fingerprint(root: Path, project: str, digests: dict[Path, str]) -> str: - """Hash source contents, dependencies, build configuration, and extractor code.""" - paths = project_sources(root, project) | {root / name for name in GLOBAL_INPUTS} + """Hash sources, compiled modules, dependency pins, and extractor code. + + Hashing compiled modules rather than the build configuration keeps an + option change that leaves a project's `.olean` identical from invalidating it. + """ + sources = project_sources(root, project) + paths = sources | {root / name for name in GLOBAL_INPUTS} + paths |= compiled_hashes(root, sources) or {root / BUILD_CONFIGURATION} inputs = {} for path in sorted(paths): if path not in digests: diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py index 58b4c252b0..bc90bb6039 100644 --- a/python/tests/test_documentation.py +++ b/python/tests/test_documentation.py @@ -30,20 +30,66 @@ def repository(tmp_path: Path) -> Path: (tmp_path / name).write_text("pinned\n") for name in ("lean-toolchain", "lakefile.toml", "lake-manifest.json"): (tmp_path / "docbuild" / name).write_text("pinned\n") + for module, imports in ( + ("LeanPool", {}), + ("LeanPool.A", {"LeanPool.Z": {}, "Mathlib.Logic.Basic": {}}), + ("LeanPool.Z", {}), + ): + inventory(tmp_path, module, imports) return tmp_path -def populate(build: Path, value: str = "previous") -> None: - """Write a real consistent SQLite database and its corresponding marker.""" +def inventory(root: Path, module: str, imports: dict) -> None: + """Write Lake's transitive import inventory for one module.""" + path = root / documentation.IR / (module.replace(".", "/") + ".setup.json") + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps({"name": module, "importArts": imports})) + + +def populate(build: Path, value: str = "previous", modules: tuple = ()) -> None: + """Write a consistent SQLite database shaped like doc-gen's, with a marker.""" build.mkdir(parents=True, exist_ok=True) with sqlite3.connect(build / "api-docs.db") as connection: + connection.execute("PRAGMA foreign_keys = ON") connection.execute("CREATE TABLE IF NOT EXISTS contents (value TEXT)") + connection.execute("CREATE TABLE IF NOT EXISTS modules (name TEXT PRIMARY KEY)") + connection.execute( + "CREATE TABLE IF NOT EXISTS name_info (module_name TEXT NOT NULL, " + "FOREIGN KEY (module_name) REFERENCES modules(name) ON DELETE CASCADE)" + ) connection.execute("DELETE FROM contents") connection.execute("INSERT INTO contents VALUES (?)", (value,)) + for name in modules: + connection.execute("INSERT OR IGNORE INTO modules VALUES (?)", (name,)) + connection.execute("INSERT INTO name_info VALUES (?)", (name,)) + connection.close() (build / "doc-data").mkdir(exist_ok=True) (build / "doc-data" / "module.doc").write_text(value) +def compile_modules(root: Path, digest: str = "0", *modules: str) -> None: + """Write Lake's compiled-module content hashes for the named modules.""" + for module in modules or tuple(documentation.module_sources(root)): + path = ( + root / documentation.COMPILED / (module.replace(".", "/") + ".olean.hash") + ) + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(digest) + + +def recording_build(commands: list): + """Stand in for Lake: record each batch and store its modules in the database.""" + + def build(command, directory, timeout): + commands.append(command) + names = tuple( + item.removeprefix("+").removesuffix(":docInfo") for item in command[2:] + ) + populate(directory / ".lake" / "build", modules=names) + + return build + + def test_import_order_ignores_comments_and_strings(repository: Path) -> None: """A project aggregate cannot trigger its entire cold closure in one batch.""" modules = documentation.ordered_modules(repository) @@ -93,17 +139,10 @@ def test_first_failed_batch_leaves_no_checkpoint(tmp_path: Path) -> None: assert not (tmp_path / "doc-data").exists() -def test_resume_skips_verified_batches_but_rechecks_changed_sources( - repository: Path, monkeypatch -) -> None: - """Only the same source and policy snapshot may reuse the saved cursor.""" - commands = [] - - def build(command, directory, timeout): - commands.append(command) - populate(directory / ".lake" / "build") - - monkeypatch.setattr(documentation, "run_build", build) +def test_resume_rechecks_only_changed_projects(repository: Path, monkeypatch) -> None: + """An edit sends its project and importers back to Lake; shared inputs reset all.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) assert documentation.build_batches(repository, "lake", 60, 2) assert len(commands) == 2 documentation.require_complete(repository) @@ -113,10 +152,89 @@ def build(command, directory, timeout): with pytest.raises(ValueError, match="incomplete"): documentation.require_complete(repository) assert documentation.build_batches(repository, "lake", 60, 2) - assert len(commands) == 4 + assert commands[2:] == [ + ["lake", "build", "+LeanPool.Z:docInfo", "+LeanPool.A:docInfo"] + ] + documentation.require_complete(repository) monkeypatch.setenv("DOCGEN_DEPS_DOCS_URL", "https://example.com/new-docs") with pytest.raises(ValueError, match="incomplete"): documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert len(commands[3:]) == 1 and len(commands[3]) == 5 + + +def test_option_edit_reuses_projects_with_unchanged_compiled_modules( + repository: Path, monkeypatch +) -> None: + """Pool options reach pages only through compiled modules, so hash those instead.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + compile_modules(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + (repository / "lakefile.toml").write_text("changed options\n") + documentation.require_complete(repository) + compile_modules(repository, "1", "LeanPool.A") + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [["lake", "build", "+LeanPool.A:docInfo"]] + + +@pytest.mark.parametrize("contents", [None, "broken", '{"name": "LeanPool.Z"}']) +def test_missing_inventory_hashes_the_whole_pool( + repository: Path, monkeypatch, contents +) -> None: + """Without Lake's import inventory, any pool edit re-checks the project.""" + path = repository / documentation.IR / "LeanPool/A.setup.json" + if contents is None: + path.unlink() + else: + path.write_text(contents) + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + assert documentation.build_batches(repository, "lake", 60, 3) + (repository / "LeanPool.lean").write_text("module\n-- changed\n") + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [ + ["lake", "build", "+LeanPool:docInfo", "+LeanPool.A:docInfo"] + ] + + +def test_option_edit_without_compiled_hashes_rechecks_everything( + repository: Path, monkeypatch +) -> None: + """Missing Lake hashes conservatively tie every project to the pool options.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + assert documentation.build_batches(repository, "lake", 60, 3) + (repository / "lakefile.toml").write_text("changed options\n") + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert len(commands) == 2 and len(commands[1]) == 5 + + +def test_deleted_modules_leave_the_database_and_markers( + repository: Path, monkeypatch +) -> None: + """A removed module cannot keep a page, and its return is analyzed again.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + assert documentation.build_batches(repository, "lake", 60, 3) + build = repository / "docbuild" / ".lake" / "build" + populate(build, modules=("Mathlib.Logic.Basic",)) + (build / "doc-data" / "LeanPool.Z.doc").write_text("marker") + (build / "doc-data" / "LeanPool.Z.doc.trace").write_text("trace") + (repository / "LeanPool" / "Z.lean").unlink() + (repository / "LeanPool" / "A.lean").write_text("module\n") + assert documentation.build_batches(repository, "lake", 60, 3) + with sqlite3.connect(build / "api-docs.db") as connection: + modules = {name for (name,) in connection.execute("SELECT name FROM modules")} + orphans = connection.execute( + "SELECT COUNT(*) FROM name_info WHERE module_name = 'LeanPool.Z'" + ).fetchone() + assert modules == {"LeanPool", "LeanPool.A", "Mathlib.Logic.Basic"} + assert orphans == (0,) + assert not list((build / "doc-data").glob("LeanPool.Z.doc*")) + documentation.require_complete(repository) def test_timeout_advances_only_completed_batches(repository: Path, monkeypatch) -> None: @@ -133,7 +251,8 @@ def build(command, directory, timeout): monkeypatch.setattr(documentation, "run_build", build) assert not documentation.build_batches(repository, "lake", 60, 2) build_path = repository / "docbuild" / ".lake" / "build" - assert json.loads((build_path / documentation.STATE).read_text())["cursor"] == 2 + progress = json.loads((build_path / documentation.STATE).read_text()) + assert len(progress["projects"]) == 2 assert (build_path / "doc-data" / "module.doc").read_text() == "1" with pytest.raises(ValueError, match="incomplete"): documentation.require_complete(repository) diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py index 9e7d3dbebd..78610b8000 100644 --- a/python/tests/test_exposition_extract.py +++ b/python/tests/test_exposition_extract.py @@ -12,13 +12,19 @@ import pytest from lean_pool.exposition import extract as extraction -from lean_pool.exposition.extract import GLOBAL_INPUTS, OUTPUTS, run_extraction +from lean_pool.exposition.extract import ( + BUILD_CONFIGURATION, + COMPILED, + GLOBAL_INPUTS, + OUTPUTS, + run_extraction, +) @pytest.fixture def repository(tmp_path: Path) -> Path: """Create two projects and a fake Lean process producing valid extractor JSONL.""" - for name in GLOBAL_INPUTS: + for name in (*GLOBAL_INPUTS, BUILD_CONFIGURATION): path = tmp_path / name path.parent.mkdir(parents=True, exist_ok=True) path.write_text("configuration\n") @@ -108,6 +114,33 @@ def test_global_input_invalidates_every_project(repository: Path, name: str) -> assert not any(item.cached for item in _run(repository)) +def _compile(root: Path, project: str, digest: str = "0") -> None: + path = root / COMPILED / f"LeanPool/{project}.olean.hash" + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(digest) + + +def test_missing_compiled_hashes_fall_back_to_build_configuration( + repository: Path, +) -> None: + """A project without Lake's module hashes is invalidated by any option edit.""" + _compile(repository, "A") + _run(repository) + (repository / BUILD_CONFIGURATION).write_text("changed configuration\n") + assert [item.cached for item in _run(repository)] == [True, False] + + +def test_compiled_hashes_replace_build_configuration(repository: Path) -> None: + """An option edit that leaves compiled modules identical keeps their extraction.""" + for project in ("A", "B"): + _compile(repository, project) + _run(repository) + (repository / BUILD_CONFIGURATION).write_text("changed configuration\n") + assert all(item.cached for item in _run(repository)) + _compile(repository, "B", "1") + assert [item.cached for item in _run(repository)] == [True, False] + + @pytest.mark.parametrize("contents", [None, "broken", "{}", '{"name": "wrong"}']) def test_missing_inventory_conservatively_hashes_pool( repository: Path, contents From 6dc13d34e72cd46d35d0a3e5f51aa90513fe7d3d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 6 Nov 2026 10:19:10 -0800 Subject: [PATCH 2/3] Fingerprint documented projects after their batch, not before A real doc-gen run showed Lake can compile a stale module while it analyzes it; the fingerprint taken at the start then never matches and rendering refuses the completed analysis. Hash each project's closure when its last module finishes instead. Co-Authored-By: Claude Opus 5.5 --- python/lean_pool/documentation.py | 44 +++++++++++++++++++----------- python/tests/test_documentation.py | 18 ++++++++++++ 2 files changed, 46 insertions(+), 16 deletions(-) diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py index 37ff764a5f..33051c939e 100644 --- a/python/lean_pool/documentation.py +++ b/python/lean_pool/documentation.py @@ -114,28 +114,36 @@ def local_closure(root: Path, project: str, modules: set[str]) -> set[str] | Non return closure if own <= closure else None -def project_fingerprints(root: Path) -> dict[str, str]: +def project_fingerprints( + root: Path, projects: set[str] | None = None +) -> dict[str, str]: """Hash the sources and compiled modules each project's pages depend on. That is the project's modules plus every pool module they import, from other projects too. Without Lake's import inventory the whole pool is included; without its compiled-module hashes the pool configuration stands in for them. + Only the closures of `projects` (default: all) are read. """ sources = module_sources(root) modules = set(sources) configuration = hashlib.sha256((root / "lakefile.toml").read_bytes()).hexdigest() - digests = {} - for module, path in sources.items(): - compiled = root / COMPILED / path.relative_to(root).with_suffix(".olean.hash") - source = hashlib.sha256(path.read_bytes()).hexdigest() - digests[module] = ( - source, - compiled.read_text().strip() if compiled.is_file() else None, - ) + digests: dict[str, tuple[str, str | None]] = {} + + def digest(module: str) -> tuple[str, str | None]: + if module not in digests: + path = sources[module] + compiled = root / COMPILED / path.relative_to(root) + compiled = compiled.with_suffix(".olean.hash") + digests[module] = ( + hashlib.sha256(path.read_bytes()).hexdigest(), + compiled.read_text().strip() if compiled.is_file() else None, + ) + return digests[module] + fingerprints = {} - for project in sorted({project_of(module) for module in modules}): + for project in sorted(projects or {project_of(module) for module in modules}): closure = local_closure(root, project, modules) or modules - entries = {module: digests[module] for module in sorted(closure)} + entries = {module: digest(module) for module in sorted(closure)} if any(compiled is None for _, compiled in entries.values()): entries["lakefile.toml"] = (configuration, None) encoded = json.dumps(entries, sort_keys=True).encode() @@ -371,14 +379,18 @@ def build_batches(root: Path, lake: str, seconds: float, batch_size: int) -> boo ) from None break position += len(batch) + finished = set() for module in batch: - project = project_of(module) - remaining[project] -= 1 - if not remaining[project]: - done[project] = fingerprints[project] + remaining[project_of(module)] -= 1 + if not remaining[project_of(module)]: + finished.add(project_of(module)) + # Lake may have compiled modules during the batch, so fingerprint the + # finished projects as analyzed rather than as they were at the start. + if finished: + done.update(project_fingerprints(root, finished)) write_progress(build, identity, done) LOGGER.info("Documentation analysis: %s/%s modules", position, len(pending)) - return done == fingerprints + return done == project_fingerprints(root) def write_progress(build: Path, identity: str, done: dict[str, str]) -> None: diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py index bc90bb6039..9881aebd48 100644 --- a/python/tests/test_documentation.py +++ b/python/tests/test_documentation.py @@ -163,6 +163,24 @@ def test_resume_rechecks_only_changed_projects(repository: Path, monkeypatch) -> assert len(commands[3:]) == 1 and len(commands[3]) == 5 +def test_modules_compiled_during_analysis_are_recorded_as_analyzed( + repository: Path, monkeypatch +) -> None: + """Lake may compile a stale module while analyzing; record what it analyzed.""" + commands: list = [] + record = recording_build(commands) + + def build(command, directory, timeout): + record(command, directory, timeout) + compile_modules(repository) + + monkeypatch.setattr(documentation, "run_build", build) + assert documentation.build_batches(repository, "lake", 60, 3) + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert len(commands) == 1 + + def test_option_edit_reuses_projects_with_unchanged_compiled_modules( repository: Path, monkeypatch ) -> None: From 6082bc2364daaa5c43447c906ce281dd5dd6614e Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 6 Nov 2026 10:51:48 -0800 Subject: [PATCH 3/3] fix: fingerprint documentation companion artifacts --- python/lean_pool/documentation.py | 38 ++++++--- python/lean_pool/exposition/extract.py | 50 +++++++++--- python/tests/test_documentation.py | 100 +++++++++++++++++++++++- python/tests/test_exposition_extract.py | 73 ++++++++++++++++- 4 files changed, 233 insertions(+), 28 deletions(-) diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py index 33051c939e..dbf029d9e6 100644 --- a/python/lean_pool/documentation.py +++ b/python/lean_pool/documentation.py @@ -114,29 +114,49 @@ def local_closure(root: Path, project: str, modules: set[str]) -> set[str] | Non return closure if own <= closure else None +def compiled_module_hashes(root: Path, source: Path) -> dict[str, str | None]: + """Identify each consumed module artifact, including absent legacy companions. + + Lake's cached content hash is used when available. Otherwise stream the + artifact itself, so a missing hash never hides a changed companion. + """ + identities = {} + for suffix in ("olean", "olean.server", "olean.private"): + artifact = root / COMPILED / source.relative_to(root).with_suffix(f".{suffix}") + if not artifact.is_file(): + identities[suffix] = None + continue + cached = Path(f"{artifact}.hash") + identity = cached if cached.is_file() and cached.stat().st_size else artifact + with identity.open("rb") as stream: + digest = hashlib.file_digest(stream, "sha256").hexdigest() + kind = "cached" if identity == cached else "artifact" + identities[suffix] = f"{kind}:{digest}" + return identities + + def project_fingerprints( root: Path, projects: set[str] | None = None ) -> dict[str, str]: """Hash the sources and compiled modules each project's pages depend on. That is the project's modules plus every pool module they import, from other - projects too. Without Lake's import inventory the whole pool is included; - without its compiled-module hashes the pool configuration stands in for them. - Only the closures of `projects` (default: all) are read. + projects too. Without Lake's import inventory the whole pool is included. + Missing public artifacts retain the pool configuration as a fallback; present + artifacts use cached or directly computed content hashes. Only the closures + of `projects` (default: all) are read. """ sources = module_sources(root) modules = set(sources) configuration = hashlib.sha256((root / "lakefile.toml").read_bytes()).hexdigest() - digests: dict[str, tuple[str, str | None]] = {} + digests: dict[str, tuple[str, dict[str, str | None]]] = {} - def digest(module: str) -> tuple[str, str | None]: + def digest(module: str) -> tuple[str, dict[str, str | None]]: if module not in digests: path = sources[module] - compiled = root / COMPILED / path.relative_to(root) - compiled = compiled.with_suffix(".olean.hash") digests[module] = ( hashlib.sha256(path.read_bytes()).hexdigest(), - compiled.read_text().strip() if compiled.is_file() else None, + compiled_module_hashes(root, path), ) return digests[module] @@ -144,7 +164,7 @@ def digest(module: str) -> tuple[str, str | None]: for project in sorted(projects or {project_of(module) for module in modules}): closure = local_closure(root, project, modules) or modules entries = {module: digest(module) for module in sorted(closure)} - if any(compiled is None for _, compiled in entries.values()): + if any(compiled["olean"] is None for _, compiled in entries.values()): entries["lakefile.toml"] = (configuration, None) encoded = json.dumps(entries, sort_keys=True).encode() fingerprints[project] = hashlib.sha256(encoded).hexdigest() diff --git a/python/lean_pool/exposition/extract.py b/python/lean_pool/exposition/extract.py index ff49a02678..4bd6d96e85 100644 --- a/python/lean_pool/exposition/extract.py +++ b/python/lean_pool/exposition/extract.py @@ -34,8 +34,8 @@ "python/lean_pool/exposition/source_text.py", ) -# Build options reach the extractor only through compiled modules, so Lake's -# content hashes stand in for them. Without those hashes, fall back to the file. +# Build options reach the extractor through all consumed module artifacts. +# Missing public artifacts conservatively retain the build configuration. BUILD_CONFIGURATION = "lakefile.toml" COMPILED = Path(".lake/build/lib/lean") @@ -91,29 +91,55 @@ def project_sources(root: Path, project: str) -> set[Path]: return sources -def compiled_hashes(root: Path, sources: set[Path]) -> set[Path] | None: - """Locate Lake's content hash of each source's compiled module, if all exist.""" - paths = { - root / COMPILED / source.relative_to(root).with_suffix(".olean.hash") - for source in sources - } - return paths if all(path.is_file() for path in paths) else None +def compiled_hashes( + root: Path, sources: set[Path], digests: dict[Path, str] | None = None +) -> dict[Path, str | None]: + """Identify present artifacts and absent companions; stream uncached content.""" + if digests is None: + digests = {} + identities = {} + for source in sorted(sources): + for suffix in ("olean", "olean.server", "olean.private"): + artifact = ( + root / COMPILED / source.relative_to(root).with_suffix(f".{suffix}") + ) + if not artifact.is_file(): + identities[artifact] = None + continue + cached = Path(f"{artifact}.hash") + identity = ( + cached if cached.is_file() and cached.stat().st_size else artifact + ) + if identity not in digests: + digests[identity] = file_digest(identity) + kind = "cached" if identity == cached else "artifact" + identities[artifact] = f"{kind}:{digests[identity]}" + return identities def fingerprint(root: Path, project: str, digests: dict[Path, str]) -> str: """Hash sources, compiled modules, dependency pins, and extractor code. - Hashing compiled modules rather than the build configuration keeps an - option change that leaves a project's `.olean` identical from invalidating it. + Hashing public, server and private artifacts instead of the configuration + preserves reuse only when every consumed compiled artifact stays identical. """ sources = project_sources(root, project) paths = sources | {root / name for name in GLOBAL_INPUTS} - paths |= compiled_hashes(root, sources) or {root / BUILD_CONFIGURATION} + compiled = compiled_hashes(root, sources, digests) + if any( + compiled[root / COMPILED / source.relative_to(root).with_suffix(".olean")] + is None + for source in sources + ): + paths.add(root / BUILD_CONFIGURATION) inputs = {} for path in sorted(paths): if path not in digests: digests[path] = file_digest(path) inputs[path.relative_to(root).as_posix()] = digests[path] + inputs.update( + {path.relative_to(root).as_posix(): value for path, value in compiled.items()} + ) return hashlib.sha256(json.dumps(inputs, sort_keys=True).encode()).hexdigest() diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py index 9881aebd48..e386325191 100644 --- a/python/tests/test_documentation.py +++ b/python/tests/test_documentation.py @@ -67,14 +67,25 @@ def populate(build: Path, value: str = "previous", modules: tuple = ()) -> None: (build / "doc-data" / "module.doc").write_text(value) -def compile_modules(root: Path, digest: str = "0", *modules: str) -> None: - """Write Lake's compiled-module content hashes for the named modules.""" +def compile_modules( + root: Path, + digest: str = "0", + *modules: str, + artifact: str = "olean", + cache_hash: bool = True, +) -> None: + """Write real artifact presence and optional Lake content-hash sidecars.""" for module in modules or tuple(documentation.module_sources(root)): path = ( - root / documentation.COMPILED / (module.replace(".", "/") + ".olean.hash") + root / documentation.COMPILED / (module.replace(".", "/") + f".{artifact}") ) path.parent.mkdir(parents=True, exist_ok=True) - path.write_text(digest) + path.write_text(f"compiled {digest}\n") + cached = Path(f"{path}.hash") + if cache_hash: + cached.write_text(digest) + else: + cached.unlink(missing_ok=True) def recording_build(commands: list): @@ -353,3 +364,84 @@ def test_reused_analysis_propagates_completion( assert (process.returncode == 0) == expected if expected: assert output.read_text() == "complete=true\n" + + +@pytest.mark.parametrize("artifact", ["olean.server", "olean.private"]) +def test_companion_only_changes_invalidate_completion_and_reanalyze( + repository: Path, monkeypatch, artifact: str +) -> None: + """Unchanged public oleans cannot conceal new documentation metadata.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + compile_modules(repository) + compile_modules(repository, "old", "LeanPool.A", artifact=artifact) + assert documentation.build_batches(repository, "lake", 60, 3) + documentation.require_complete(repository) + (repository / "lakefile.toml").write_text("changed documentation options\n") + compile_modules(repository, "new", "LeanPool.A", artifact=artifact) + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [["lake", "build", "+LeanPool.A:docInfo"]] + documentation.require_complete(repository) + + +@pytest.mark.parametrize("artifact", ["olean.server", "olean.private"]) +def test_companion_presence_and_absence_invalidate_completed_projects( + repository: Path, monkeypatch, artifact: str +) -> None: + """Legacy modules may omit companions, but their later appearance matters.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + compile_modules(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + documentation.require_complete(repository) + compile_modules(repository, "new", "LeanPool.A", artifact=artifact) + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + path = repository / documentation.COMPILED / f"LeanPool/A.{artifact}" + path.unlink() # A leftover hash must not stand in for an absent artifact. + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [["lake", "build", "+LeanPool.A:docInfo"]] * 2 + documentation.require_complete(repository) + + +@pytest.mark.parametrize("artifact", ["olean", "olean.server", "olean.private"]) +def test_missing_cached_hash_still_tracks_actual_artifact_content( + repository: Path, monkeypatch, artifact: str +) -> None: + """Hash actual output when Lake's sidecar is absent, without guessing validity.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + compile_modules(repository) + compile_modules( + repository, "old", "LeanPool.A", artifact=artifact, cache_hash=False + ) + assert documentation.build_batches(repository, "lake", 60, 3) + compile_modules( + repository, "new", "LeanPool.A", artifact=artifact, cache_hash=False + ) + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [["lake", "build", "+LeanPool.A:docInfo"]] + documentation.require_complete(repository) + + +def test_missing_public_artifact_keeps_conservative_configuration_identity( + repository: Path, monkeypatch +) -> None: + """An old hash alone is not evidence of a current compiled public module.""" + commands: list = [] + monkeypatch.setattr(documentation, "run_build", recording_build(commands)) + compile_modules(repository) + (repository / documentation.COMPILED / "LeanPool/A.olean").unlink() + assert documentation.build_batches(repository, "lake", 60, 3) + (repository / "lakefile.toml").write_text("changed options\n") + with pytest.raises(ValueError, match="incomplete"): + documentation.require_complete(repository) + assert documentation.build_batches(repository, "lake", 60, 3) + assert commands[1:] == [["lake", "build", "+LeanPool.A:docInfo"]] diff --git a/python/tests/test_exposition_extract.py b/python/tests/test_exposition_extract.py index 78610b8000..bcea5eab9d 100644 --- a/python/tests/test_exposition_extract.py +++ b/python/tests/test_exposition_extract.py @@ -114,10 +114,22 @@ def test_global_input_invalidates_every_project(repository: Path, name: str) -> assert not any(item.cached for item in _run(repository)) -def _compile(root: Path, project: str, digest: str = "0") -> None: - path = root / COMPILED / f"LeanPool/{project}.olean.hash" +def _compile( + root: Path, + project: str, + digest: str = "0", + *, + artifact: str = "olean", + cache_hash: bool = True, +) -> None: + path = root / COMPILED / f"LeanPool/{project}.{artifact}" path.parent.mkdir(parents=True, exist_ok=True) - path.write_text(digest) + path.write_text(f"compiled {digest}\n") + cached = Path(f"{path}.hash") + if cache_hash: + cached.write_text(digest) + else: + cached.unlink(missing_ok=True) def test_missing_compiled_hashes_fall_back_to_build_configuration( @@ -384,3 +396,58 @@ def reject_failed_timings(destination, started, results, state): assert error.value is failure assert "Could not write failed extraction timings" in caplog.text assert not (repository / "calls").exists() + + +@pytest.mark.parametrize("artifact", ["olean.server", "olean.private"]) +def test_companion_only_changes_invalidate_extraction( + repository: Path, artifact: str +) -> None: + """Public module stability does not make changed companion metadata reusable.""" + for project in ("A", "B"): + _compile(repository, project) + _compile(repository, "B", "old", artifact=artifact) + _run(repository) + (repository / BUILD_CONFIGURATION).write_text("changed documentation options\n") + _compile(repository, "B", "new", artifact=artifact) + assert [item.cached for item in _run(repository)] == [True, False] + assert all(item.cached for item in _run(repository)) + + +@pytest.mark.parametrize("artifact", ["olean.server", "olean.private"]) +def test_companion_presence_and_absence_invalidate_extraction( + repository: Path, artifact: str +) -> None: + """A legacy absent companion and a newly present one have different identities.""" + for project in ("A", "B"): + _compile(repository, project) + _run(repository) + _compile(repository, "B", "new", artifact=artifact) + assert [item.cached for item in _run(repository)] == [True, False] + (repository / COMPILED / f"LeanPool/B.{artifact}").unlink() + assert [item.cached for item in _run(repository)] == [True, False] + assert all(item.cached for item in _run(repository)) + + +@pytest.mark.parametrize("artifact", ["olean", "olean.server", "olean.private"]) +def test_missing_cached_hash_still_tracks_extraction_artifact( + repository: Path, artifact: str +) -> None: + """An uncached companion is hashed directly instead of being ignored.""" + for project in ("A", "B"): + _compile(repository, project) + _compile(repository, "B", "old", artifact=artifact, cache_hash=False) + _run(repository) + _compile(repository, "B", "new", artifact=artifact, cache_hash=False) + assert [item.cached for item in _run(repository)] == [True, False] + + +def test_missing_public_artifact_keeps_extraction_configuration_fallback( + repository: Path, +) -> None: + """A stale public hash with no artifact cannot disable the options fallback.""" + for project in ("A", "B"): + _compile(repository, project) + (repository / COMPILED / "LeanPool/B.olean").unlink() + _run(repository) + (repository / BUILD_CONFIGURATION).write_text("changed options\n") + assert [item.cached for item in _run(repository)] == [True, False]