diff --git a/.github/workflows/docs-build.yml b/.github/workflows/docs-build.yml index f4fab617ef..5a79e5567d 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,9 +73,9 @@ jobs: .lake/packages/UnicodeBasic .lake/packages/BibtexQuery .lake/packages/MD4Lean - # Most pool lakefile edits leave many docInfo traces valid, so fall back to a - # checkpoint from an older lakefile; Lake rebuilds only what changed and the - # cursor identity still includes lakefile.toml. + # Prefer a checkpoint from the same pool lakefile, then fall back to an older + # one: Lake rebuilds only stale docInfo, and per-project progress rechecks + # only projects whose compiled modules changed. key: DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ hashFiles('lakefile.toml') }}-${{ github.run_id }}-${{ github.run_attempt }}-${{ inputs.stage }} 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..dbf029d9e6 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,147 @@ 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 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. + 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, dict[str, str | None]]] = {} + + def digest(module: str) -> tuple[str, dict[str, str | None]]: + if module not in digests: + path = sources[module] + digests[module] = ( + hashlib.sha256(path.read_bytes()).hexdigest(), + compiled_module_hashes(root, path), + ) + return digests[module] + + fingerprints = {} + 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["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() + 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 +256,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 +355,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 +393,37 @@ 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) + finished = set() + for module in batch: + 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 == project_fingerprints(root) + + +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..4bd6d96e85 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 through all consumed module artifacts. +# Missing public artifacts conservatively retain the build configuration. +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,14 +91,55 @@ def project_sources(root: Path, project: str) -> set[Path]: return sources +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 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 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} + 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 58b4c252b0..e386325191 100644 --- a/python/tests/test_documentation.py +++ b/python/tests/test_documentation.py @@ -30,20 +30,77 @@ 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, + 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(".", "/") + f".{artifact}") + ) + path.parent.mkdir(parents=True, exist_ok=True) + 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): + """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 +150,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 +163,107 @@ 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_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: + """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 +280,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) @@ -216,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 9e7d3dbebd..bcea5eab9d 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,45 @@ 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", + *, + 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(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( + 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 @@ -351,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]