From 15013380c54f39d7f147fc138daa81b742812122 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 8 Oct 2026 21:34:04 -0700 Subject: [PATCH 1/2] Render documentation for every independent project --- .github/workflows/docs.yml | 10 ++-- python/lean_pool/documentation.py | 92 ++++++++++++++++++++++++++++++ python/tests/test_documentation.py | 85 +++++++++++++++++++++++++++ 3 files changed, 181 insertions(+), 6 deletions(-) create mode 100644 python/lean_pool/documentation.py create mode 100644 python/tests/test_documentation.py diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 24f02beda4..85f3384d08 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -15,6 +15,8 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/documentation.py' + - 'python/lean_pool/indexes.py' - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' @@ -574,14 +576,10 @@ jobs: --repository "$REPOSITORY" --key "$CACHE_KEY" - name: Build documentation - run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs + run: PYTHONPATH=python python3 -m lean_pool.documentation build - name: Validate documentation site - run: | - set -euo pipefail - test -s docbuild/.lake/build/doc/index.html - test -s docbuild/.lake/build/doc/LeanPool.html - test -s docbuild/.lake/build/doc/declarations/declaration-data.bmp + run: PYTHONPATH=python python3 -m lean_pool.documentation validate - name: Remove cached exposition if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request' diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py new file mode 100644 index 0000000000..eee340a76a --- /dev/null +++ b/python/lean_pool/documentation.py @@ -0,0 +1,92 @@ +"""Render API documentation for every independent project and verify coverage.""" + +from __future__ import annotations + +import argparse +import subprocess +from pathlib import Path + +from lean_pool.indexes import project_modules, structure_errors + + +def documentation_roots(root: Path) -> list[str]: + """Select complete public project roots without changing the fixed pool root.""" + errors = structure_errors(root) + if errors: + path, message = errors[0] + raise ValueError(f"{path}: {message}") + projects = project_modules(root) + if not projects: + raise ValueError("no LeanPool projects found") + return [ + "LeanPool", + *(f"LeanPool.{project}.Imports" for project in projects), + "Init", + "Std", + "Lake", + "Lean", + ] + + +def validate_site(root: Path, site: Path) -> None: + """Reject a root-only site or any missing page for a compiled pool source.""" + sources = [root / "LeanPool.lean", *sorted((root / "LeanPool").rglob("*.lean"))] + required = [ + site / "index.html", + site / "declarations/declaration-data.bmp", + *(site / path.relative_to(root).with_suffix(".html") for path in sources), + ] + missing = [ + path.relative_to(site) + for path in required + if not path.is_file() or not path.stat().st_size + ] + if missing: + sample = ", ".join(str(path) for path in missing[:5]) + raise ValueError( + f"documentation is missing {len(missing)} required pages/files: {sample}" + ) + + +def build_site(root: Path, lake: Path) -> None: + """Generate HTML from verified docInfo using every project's import closure.""" + roots = documentation_roots(root) + # doc-gen4's library docs facet follows only library roots. LeanPool's fixed + # root imports no projects, so supply their public roots to fromDb directly. + subprocess.run( + [ + str(lake), + "exe", + "doc-gen4", + "fromDb", + "--build", + ".lake/build", + "--manifest", + ".lake/build/doc-manifest.json", + ".lake/build/api-docs.db", + *roots, + ], + cwd=root / "docbuild", + check=True, + ) + validate_site(root, root / "docbuild/.lake/build/doc") + + +def main(argv: list[str] | None = None) -> int: + """Build the complete site or verify an existing documentation artifact.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("command", choices=("build", "validate")) + parser.add_argument("--repo", type=Path, default=Path.cwd()) + parser.add_argument("--lake", type=Path, default=Path.home() / ".elan/bin/lake") + arguments = parser.parse_args(argv) + root = arguments.repo.resolve() + if arguments.command == "build": + build_site(root, arguments.lake.expanduser().resolve()) + else: + documentation_roots(root) + validate_site(root, root / "docbuild/.lake/build/doc") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py new file mode 100644 index 0000000000..1d400ba4ff --- /dev/null +++ b/python/tests/test_documentation.py @@ -0,0 +1,85 @@ +"""Prevent API publication from omitting independent project modules.""" + +import subprocess +from pathlib import Path + +import pytest + +from lean_pool import documentation, indexes + + +@pytest.fixture +def repository(tmp_path: Path) -> Path: + """Create single-file and nested projects under the fixed discovery root.""" + (tmp_path / "LeanPool/Beta/Nested").mkdir(parents=True) + (tmp_path / "docbuild").mkdir() + for module in ("Alpha", "Beta", "Beta/Nested/Proof"): + (tmp_path / f"LeanPool/{module}.lean").write_text("module\n") + (tmp_path / "lakefile.toml").write_text( + "requiresModuleSystem = true\n[[lean_lib]]\n" + 'name = "LeanPool"\nglobs = ["LeanPool.*"]\n' + ) + assert indexes.main(["--repo", str(tmp_path), "--project-roots"]) == 0 + return tmp_path + + +def _page(site: Path, name: str) -> None: + """Write a nonempty artifact entry.""" + path = site / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text("documentation") + + +def test_fixed_root_does_not_hide_independent_projects(repository: Path) -> None: + """A root with no imports still selects every complete public project API.""" + before = (repository / "LeanPool.lean").read_bytes() + assert before.decode() == indexes.DISCOVERY_ROOT + roots = documentation.documentation_roots(repository) + assert "LeanPool.Alpha.Imports" in roots + assert "LeanPool.Beta.Imports" in roots + assert roots[-4:] == ["Init", "Std", "Lake", "Lean"] + assert (repository / "LeanPool.lean").read_bytes() == before + + +def test_new_source_must_enter_public_closure(repository: Path) -> None: + """Adding a proof cannot silently leave it outside the rendered closure.""" + (repository / "LeanPool/Beta/New.lean").write_text("module\n") + with pytest.raises(ValueError, match="every source"): + documentation.documentation_roots(repository) + assert indexes.main(["--repo", str(repository), "--project-roots"]) == 0 + assert "LeanPool.Beta.Imports" in documentation.documentation_roots(repository) + + +def test_root_only_site_is_rejected(repository: Path) -> None: + """The three files accepted by the former check cannot mask missing APIs.""" + site = repository / "docbuild/.lake/build/doc" + for name in ("index.html", "LeanPool.html", "declarations/declaration-data.bmp"): + _page(site, name) + with pytest.raises(ValueError, match="LeanPool/Alpha.html"): + documentation.validate_site(repository, site) + + +def test_every_source_page_is_required(repository: Path) -> None: + """Nested proofs and public wrappers both need nonempty HTML pages.""" + site = repository / "docbuild/.lake/build/doc" + for path in repository.glob("**/*.lean"): + _page(site, str(path.relative_to(repository).with_suffix(".html"))) + _page(site, "index.html") + _page(site, "declarations/declaration-data.bmp") + documentation.validate_site(repository, site) + (site / "LeanPool/Beta/Nested/Proof.html").write_text("") + with pytest.raises(ValueError, match="Nested/Proof.html"): + documentation.validate_site(repository, site) + + +def test_renderer_failure_propagates( + repository: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """Failed HTML generation never succeeds because old artifact files exist.""" + + def fail(*args: object, **kwargs: object) -> None: + raise subprocess.CalledProcessError(1, "doc-gen4") + + monkeypatch.setattr(documentation.subprocess, "run", fail) + with pytest.raises(subprocess.CalledProcessError): + documentation.build_site(repository, Path("/lake")) From f59d1bafacb3aeffbad1c6dc9befd76ed30a2271 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 9 Oct 2026 20:34:42 -0700 Subject: [PATCH 2/2] Preserve bounded documentation preparation and preview artifacts --- .github/workflows/docs.yml | 154 ++++++++++++++++++++----- python/lean_pool/documentation.py | 71 +++++++++++- python/tests/test_ci_cache_contract.py | 42 ++++++- python/tests/test_documentation.py | 83 +++++++++++++ 4 files changed, 320 insertions(+), 30 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 85f3384d08..e492cd1c3f 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -432,7 +432,7 @@ jobs: PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$REPOSITORY" --key "$CACHE_KEY" - build: + pool_doc_info: needs: - preflight - mathlib_doc_info @@ -441,7 +441,10 @@ jobs: ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || (github.event_name == 'workflow_dispatch' && inputs.preview)) runs-on: ubuntu-latest - name: Build doc-gen4 site + name: Prepare pool documentation data + outputs: + checkpoint_key: ${{ steps.checkpoint-identity.outputs.key }} + complete_checkpoint: ${{ steps.pool-doc-cache.outputs.cache-hit }} permissions: contents: read actions: write @@ -467,9 +470,8 @@ jobs: restore-keys: | LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- - # Prefer the latest complete docInfo database from this compatibility - # boundary. On a cold boundary, the preceding job has just produced the - # Mathlib-only checkpoint used by the conditional fallback below. + # Compatible partial inputs are safe to resume: Lake still checks every + # module, and HTML publication requires the complete target downstream. - name: Restore pool documentation checkpoint id: pool-doc-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -527,32 +529,128 @@ jobs: PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore --head "$BUILD_HEAD" --event "$BUILD_EVENT" - # This incrementally extends either a previous pool checkpoint or the - # Mathlib checkpoint produced by the preceding job. doc-gen serializes - # writes through one WAL database, so these targets intentionally share a - # single job instead of unsafe parallel shards. - - name: Build documentation data - run: cd docbuild && ~/.elan/bin/lake build LeanPool:docInfo + # Leave time to stop all SQLite writers and save valid partial inputs. + # The next serial job still requires the complete Lake target to succeed. + - name: Prepare documentation data within checkpoint budget + run: >- + PYTHONPATH=python python3 -m lean_pool.documentation prepare + --time-budget 18000 - - name: Validate pool documentation checkpoint + - name: Identify checkpoint handoff + id: checkpoint-identity + env: + CHECKPOINT_KEY: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} + COMPLETE_CHECKPOINT: ${{ steps.pool-doc-cache.outputs.cache-hit }} + run: | + key="$CHECKPOINT_KEY" + if [ "$COMPLETE_CHECKPOINT" != 'true' ]; then + key="$key-${{ github.run_id }}-${{ github.run_attempt }}-prepare" + fi + echo "key=$key" >> "$GITHUB_OUTPUT" + + - name: Save resumable pool documentation checkpoint + if: steps.pool-doc-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + docbuild/.lake/build + .lake/packages/doc-gen4 + .lake/packages/leansqlite + .lake/packages/UnicodeBasic + .lake/packages/BibtexQuery + .lake/packages/MD4Lean + key: ${{ steps.checkpoint-identity.outputs.key }} + + build: + needs: + - preflight + - mathlib_doc_info + - pool_doc_info + if: >- + needs.preflight.outputs.readme_only != 'true' && + ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || + (github.event_name == 'workflow_dispatch' && inputs.preview)) + runs-on: ubuntu-latest + name: Build doc-gen4 site + permissions: + contents: read + actions: write + steps: + - name: Checkout project + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + + - name: Restore Lean dependencies + id: dependency-cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/.elan + .lake/packages + key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} + + - name: Restore pool build + id: pool-build + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/build + key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.preflight.outputs.build_revision }} + restore-keys: | + LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + + # Use the exact checked checkpoint from preparation. A missing handoff + # fails here instead of silently repeating the whole cold build. + - name: Restore pool documentation checkpoint + id: pool-doc-cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + docbuild/.lake/build + .lake/packages/doc-gen4 + .lake/packages/leansqlite + .lake/packages/UnicodeBasic + .lake/packages/BibtexQuery + .lake/packages/MD4Lean + key: ${{ needs.pool_doc_info.outputs.checkpoint_key }} + fail-on-cache-miss: true + + - name: Install Lean + uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 + with: + auto-config: false + use-github-cache: false + use-mathlib-cache: false + + - name: Install Mathlib cache run: | set -euo pipefail - test -s docbuild/.lake/build/api-docs.db - test -n "$(find docbuild/.lake/build/doc-data -type f -name 'LeanPool*.doc' -print -quit)" - python3 - <<'PY' - import sqlite3 + ~/.elan/bin/lake exe cache get + expected=$(jq -r '.packages[] | select(.name == "mathlib") | .rev' lake-manifest.json) + actual=$(git -C .lake/packages/mathlib rev-parse HEAD) + if [ "$actual" != "$expected" ]; then + echo "::error::Mathlib checkout $actual does not match lake-manifest.json ($expected)." + exit 1 + fi - with sqlite3.connect("docbuild/.lake/build/api-docs.db") as connection: - checkpoint = connection.execute("PRAGMA wal_checkpoint(TRUNCATE)").fetchone() - integrity = connection.execute("PRAGMA quick_check").fetchone() - if checkpoint is None or checkpoint[0] != 0: - raise SystemExit(f"SQLite WAL checkpoint failed: {checkpoint!r}") - if integrity != ("ok",): - raise SystemExit(f"SQLite quick_check failed: {integrity!r}") - PY + - name: Reuse matching Lean CI build + if: steps.pool-build.outputs.cache-hit != 'true' + env: + GH_TOKEN: ${{ github.token }} + BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }} + BUILD_EVENT: ${{ github.event_name }} + run: >- + PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore + --head "$BUILD_HEAD" --event "$BUILD_EVENT" + + # Resume the preparation checkpoint in order. doc-gen serializes writes + # through one WAL database, so the two stages never run concurrently. + - name: Build documentation data + run: cd docbuild && ~/.elan/bin/lake build LeanPool:docInfo + + - name: Validate pool documentation checkpoint + run: PYTHONPATH=python python3 -m lean_pool.documentation checkpoint - name: Save pool documentation checkpoint - if: steps.pool-doc-cache.outputs.cache-hit != 'true' + if: needs.pool_doc_info.outputs.complete_checkpoint != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: | @@ -565,7 +663,7 @@ jobs: key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} - name: Prune old copies of pool documentation checkpoint - if: steps.pool-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' + if: needs.pool_doc_info.outputs.complete_checkpoint != 'true' && github.ref == 'refs/heads/main' continue-on-error: true env: GH_TOKEN: ${{ github.token }} @@ -586,7 +684,9 @@ jobs: run: rm -rf docbuild/.lake/build/doc/exposition - name: Upload documentation artifact - if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request' + if: >- + (github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || + (github.event_name == 'workflow_dispatch' && inputs.preview) uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 with: name: documentation-site diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py index eee340a76a..5d6f58deb0 100644 --- a/python/lean_pool/documentation.py +++ b/python/lean_pool/documentation.py @@ -3,11 +3,71 @@ from __future__ import annotations import argparse +import logging +import os +import signal +import sqlite3 import subprocess from pathlib import Path from lean_pool.indexes import project_modules, structure_errors +logger = logging.getLogger(__name__) + + +def validate_checkpoint(root: Path) -> None: + """Flush and check a resumable docInfo database before caching it.""" + build = root / "docbuild/.lake/build" + database = build / "api-docs.db" + if not database.is_file() or not database.stat().st_size: + raise ValueError("documentation checkpoint has no database") + if not any( + path.is_file() and path.stat().st_size + for path in (build / "doc-data").glob("LeanPool*.doc") + ): + raise ValueError("documentation checkpoint has no pool documentation data") + with sqlite3.connect(database) as connection: + checkpoint = connection.execute("PRAGMA wal_checkpoint(TRUNCATE)").fetchone() + integrity = connection.execute("PRAGMA quick_check").fetchone() + if checkpoint is None or checkpoint[0] != 0 or integrity != ("ok",): + raise ValueError(f"invalid documentation checkpoint: {checkpoint}, {integrity}") + + +def _stop_build(process: subprocess.Popen) -> None: + """Stop every writer before validating the shared SQLite checkpoint.""" + for sent_signal in (signal.SIGTERM, signal.SIGKILL): + try: + os.killpg(process.pid, sent_signal) + except ProcessLookupError: + pass + if sent_signal == signal.SIGTERM: + try: + process.wait(timeout=30) + except subprocess.TimeoutExpired: + pass + process.wait() + + +def prepare_data(root: Path, lake: Path, time_budget: float) -> bool: + """Prepare incremental docInfo inputs; downstream still builds the full target.""" + if time_budget <= 0: + raise ValueError("documentation preparation time budget must be positive") + command = [str(lake), "build", "LeanPool:docInfo"] + process = subprocess.Popen(command, cwd=root / "docbuild", start_new_session=True) + try: + result = process.wait(timeout=time_budget) + except subprocess.TimeoutExpired: + _stop_build(process) + validate_checkpoint(root) + logger.warning( + "Preparation time budget reached; full docInfo build still required" + ) + return False + if result: + raise subprocess.CalledProcessError(result, command) + validate_checkpoint(root) + return True + def documentation_roots(root: Path) -> list[str]: """Select complete public project roots without changing the fixed pool root.""" @@ -75,12 +135,19 @@ def build_site(root: Path, lake: Path) -> None: def main(argv: list[str] | None = None) -> int: """Build the complete site or verify an existing documentation artifact.""" parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("command", choices=("build", "validate")) + parser.add_argument( + "command", choices=("prepare", "checkpoint", "build", "validate") + ) parser.add_argument("--repo", type=Path, default=Path.cwd()) parser.add_argument("--lake", type=Path, default=Path.home() / ".elan/bin/lake") + parser.add_argument("--time-budget", type=float, default=18000) arguments = parser.parse_args(argv) root = arguments.repo.resolve() - if arguments.command == "build": + if arguments.command == "prepare": + prepare_data(root, arguments.lake.expanduser().resolve(), arguments.time_budget) + elif arguments.command == "checkpoint": + validate_checkpoint(root) + elif arguments.command == "build": build_site(root, arguments.lake.expanduser().resolve()) else: documentation_roots(root) diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 388c8dae4f..1feddff7db 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -75,7 +75,7 @@ def test_docs_generate_on_main_and_explicit_preview_only() -> None: ("pull_request", "refs/pull/123/merge", True, False, False), ("push", "refs/heads/main", False, True, False), ] - for name in ("exposition", "mathlib_doc_info", "build"): + for name in ("exposition", "mathlib_doc_info", "pool_doc_info", "build"): for event, ref, preview, readme, expected in scenarios: assert ( _docs_condition(jobs[name]["if"], event, ref, preview, readme) @@ -91,6 +91,46 @@ def test_docs_generate_on_main_and_explicit_preview_only() -> None: ) +def test_documentation_resumes_serially_before_rendering() -> None: + """A time-bounded checkpoint never bypasses the complete target or HTML check.""" + jobs = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())["jobs"] + preparation = jobs["pool_doc_info"] + build = jobs["build"] + assert "mathlib_doc_info" in preparation["needs"] + assert "pool_doc_info" in build["needs"] + assert "always()" not in build["if"] + steps = {step["name"]: step for step in preparation["steps"]} + assert ( + "--time-budget 18000" + in steps["Prepare documentation data within checkpoint budget"]["run"] + ) + save = steps["Save resumable pool documentation checkpoint"] + assert "always()" not in save["if"] + identity = steps["Identify checkpoint handoff"] + assert "github.run_id" in identity["run"] + assert "github.run_attempt" in identity["run"] + assert "checkpoint-identity.outputs.key" in save["with"]["key"] + assert not any("Prune" in step["name"] for step in preparation["steps"]) + final = {step["name"]: step for step in build["steps"]} + restore = final["Restore pool documentation checkpoint"]["with"] + assert "pool_doc_info.outputs.checkpoint_key" in restore["key"] + assert restore["fail-on-cache-miss"] is True + assert "restore-keys" not in restore + assert "complete_checkpoint" in final["Save pool documentation checkpoint"]["if"] + assert final["Build documentation data"]["run"].endswith( + "lake build LeanPool:docInfo" + ) + assert "if" not in final["Build documentation data"] + assert "if" not in final["Validate documentation site"] + upload = final["Upload documentation artifact"] + assert _docs_condition( + upload["if"], "workflow_dispatch", "refs/heads/topic", True, False + ) + assert not _docs_condition( + upload["if"], "pull_request", "refs/pull/123/merge", True, False + ) + + def test_single_and_sharded_builds_use_validation_cache() -> None: """Both execution paths validate before saving receipts and keep the same gate.""" jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py index 1d400ba4ff..a5ea70fcfb 100644 --- a/python/tests/test_documentation.py +++ b/python/tests/test_documentation.py @@ -1,6 +1,8 @@ """Prevent API publication from omitting independent project modules.""" +import sqlite3 import subprocess +import sys from pathlib import Path import pytest @@ -83,3 +85,84 @@ def fail(*args: object, **kwargs: object) -> None: monkeypatch.setattr(documentation.subprocess, "run", fail) with pytest.raises(subprocess.CalledProcessError): documentation.build_site(repository, Path("/lake")) + + +def _checkpoint(repository: Path) -> Path: + """Create a real database and one completed docInfo module.""" + build = repository / "docbuild/.lake/build" + (build / "doc-data").mkdir(parents=True) + (build / "doc-data/LeanPool.Alpha.doc").write_text("completed module") + database = build / "api-docs.db" + with sqlite3.connect(database) as connection: + connection.execute("CREATE TABLE completed (value INTEGER)") + return database + + +def _lake(repository: Path, source: str) -> Path: + """Make a subprocess fixture with the same Lake invocation contract.""" + path = repository / "lake" + path.write_text(f"#!{sys.executable}\n" + source) + path.chmod(0o755) + return path + + +def test_preparation_timeout_stops_sqlite_writers(repository: Path) -> None: + """A surviving child writer cannot corrupt or lock the handed-off checkpoint.""" + database = _checkpoint(repository) + child = """ +import signal, sqlite3, time +from pathlib import Path +signal.signal(signal.SIGTERM, signal.SIG_IGN) +connection = sqlite3.connect('.lake/build/api-docs.db') +connection.execute('PRAGMA journal_mode=WAL') +connection.execute('INSERT INTO completed VALUES (1)') +Path('writer-started').touch() +time.sleep(60) +connection.commit() +""" + lake = _lake( + repository, + "import subprocess, sys, time\n" + f"subprocess.Popen([sys.executable, '-c', {child!r}])\n" + "time.sleep(60)\n", + ) + assert not documentation.prepare_data(repository, lake, 1) + assert (repository / "docbuild/writer-started").exists() + with sqlite3.connect(database) as connection: + assert connection.execute("SELECT COUNT(*) FROM completed").fetchone() == (0,) + connection.execute("INSERT INTO completed VALUES (2)") + documentation.validate_checkpoint(repository) + + +def test_preparation_does_not_mask_compiler_failure(repository: Path) -> None: + """An existing valid checkpoint cannot turn a failed Lake build into success.""" + _checkpoint(repository) + with pytest.raises(subprocess.CalledProcessError) as error: + documentation.prepare_data( + repository, _lake(repository, "raise SystemExit(7)\n"), 1 + ) + assert error.value.returncode == 7 + + +def test_completed_preparation_preserves_database(repository: Path) -> None: + """Completed preparation hands off inputs while still requiring the renderer.""" + database = _checkpoint(repository) + assert documentation.prepare_data(repository, _lake(repository, "pass\n"), 1) + assert database.is_file() + assert not (repository / "docbuild/.lake/build/doc").exists() + + +def test_invalid_checkpoint_is_not_publishable(repository: Path) -> None: + """Interrupted or corrupt inputs are rejected before any cache publication.""" + database = _checkpoint(repository) + database.write_bytes(b"corrupt SQLite database") + with pytest.raises(sqlite3.DatabaseError): + documentation.validate_checkpoint(repository) + + +def test_empty_pool_data_is_not_a_checkpoint(repository: Path) -> None: + """A database without a completed pool module cannot seed continuation.""" + _checkpoint(repository) + (repository / "docbuild/.lake/build/doc-data/LeanPool.Alpha.doc").write_bytes(b"") + with pytest.raises(ValueError, match="no pool documentation data"): + documentation.validate_checkpoint(repository)