Render complete project APIs with resumable documentation data

.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'
@@ -430,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
@@ -439,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
@@ -465,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
@@ -525,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: |
@@ -563,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 }}
@@ -574,21 +674,19 @@ 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'
         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

python/lean_pool/documentation.py

@@ -0,0 +1,159 @@
+"""Render API documentation for every independent project and verify coverage."""
+
+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."""
+    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=("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 == "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)
+        validate_site(root, root / "docbuild/.lake/build/doc")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())