diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md
index c03277e3e4..2ad6c96c8a 100644
--- a/.github/CODE_QUALITY.md
+++ b/.github/CODE_QUALITY.md
@@ -135,10 +135,16 @@ Scheduled update checks are future work.
 
 ### 10. Documentation
 
-[`docs.yml`](workflows/docs.yml) builds doc-gen4 documentation with the nested
-[`docbuild/`](../docbuild/) Lake project. Pull requests build the docs site as a
-check. Pushes to `main` build `LeanPool:docs` and deploy
-`docbuild/.lake/build/doc` to GitHub Pages.
+[`docs.yml`](workflows/docs.yml) retains cheap workspace and generated-index
+preflight checks for PRs and merge groups. It does not generate documentation.
+
+[`docs-publish.yml`](workflows/docs-publish.yml) publishes documentation daily
+at 06:23 UTC or on manual dispatch, independently of merges. It documents only
+LeanPool modules and links dependencies to their hosted documentation. Bounded
+analysis jobs save consistent incremental checkpoints; a separate rendering job
+and exposition build must both finish and validate before Pages is replaced.
+The published `SOURCE_SHA` records the documented snapshot. See the
+[documentation operations guide](../docbuild/README.md).
 
 ## Future Work
 
diff --git a/.github/workflows/docs-build.yml b/.github/workflows/docs-build.yml
new file mode 100644
index 0000000000..ad0aca8ca7
--- /dev/null
+++ b/.github/workflows/docs-build.yml
@@ -0,0 +1,158 @@
+name: Documentation build stage
+'on':
+  workflow_call:
+    inputs:
+      phase:
+        required: true
+        type: string
+      stage:
+        required: true
+        type: string
+      build_revision:
+        required: true
+        type: string
+      previous_complete:
+        type: string
+        default: 'false'
+    outputs:
+      complete:
+        value: ${{ jobs.receipt.outputs.complete }}
+permissions:
+  contents: read
+  actions: write
+env:
+  DOCGEN_LOCAL_MODULE_ROOTS: LeanPool
+  DOCGEN_DEPS_DOCS_URL: https://leanprover-community.github.io/mathlib4_docs
+  DOCGEN_DEPS_DOCS_URLS: TauCeti=https://taucetiproject.github.io/TauCeti/docs
+jobs:
+  build:
+    name: Documentation ${{ inputs.phase }} ${{ inputs.stage }}
+    if: inputs.phase == 'render' || inputs.previous_complete != 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 330
+    outputs:
+      complete: ${{ steps.analysis.outputs.complete }}
+    steps:
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+      with:
+        persist-credentials: false
+    - 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')
+          }}-${{ inputs.build_revision }}
+        restore-keys: |
+          LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+    - name: Restore documentation checkpoint
+      id: docs-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: DocsState-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', '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') }}-
+    - 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
+        ~/.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
+    - 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: push
+      run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+    - name: Verify documentation workspace
+      run: PYTHONPATH=python python3 -m lean_pool.documentation prepare
+    - name: Verify pinned doc-gen compatibility
+      run: cd docbuild && ~/.elan/bin/lake build doc-gen4
+    - name: Analyze a bounded batch
+      id: analysis
+      if: inputs.phase == 'analysis'
+      run: PYTHONPATH=python python3 -m lean_pool.documentation batch --seconds 5400 --lake /home/runner/.elan/bin/lake
+    - name: Save completed analysis batches
+      if: inputs.phase == 'analysis'
+      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.docs-cache.outputs.cache-primary-key }}
+    - name: Render and validate the complete local API
+      if: inputs.phase == 'render'
+      run: PYTHONPATH=python python3 -m lean_pool.documentation render --lake /home/runner/.elan/bin/lake
+    - name: Upload documentation artifact
+      if: inputs.phase == 'render'
+      uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+      with:
+        name: documentation-site
+        path: docbuild/.lake/build/doc
+        if-no-files-found: error
+        retention-days: 3
+    - name: Upload documentation progress
+      if: always()
+      uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+      with:
+        name: documentation-progress-${{ inputs.stage }}
+        path: docbuild/.lake/build/documentation-progress.json
+        if-no-files-found: ignore
+        include-hidden-files: true
+        retention-days: 7
+  receipt:
+    needs: build
+    if: always()
+    runs-on: ubuntu-latest
+    outputs:
+      complete: ${{ steps.result.outputs.complete }}
+    steps:
+    - id: result
+      name: Report completed or reused analysis
+      env:
+        RESULT: ${{ needs.build.result }}
+        PREVIOUS: ${{ inputs.previous_complete }}
+        PHASE: ${{ inputs.phase }}
+        COMPLETE: ${{ needs.build.outputs.complete }}
+      run: |
+        set -euo pipefail
+        if [ "$RESULT" = skipped ]; then
+          test "$PHASE" = analysis
+          test "$PREVIOUS" = true
+          COMPLETE=true
+        else
+          test "$RESULT" = success
+        fi
+        echo "complete=${COMPLETE:-false}" >> "$GITHUB_OUTPUT"
diff --git a/.github/workflows/docs-publish.yml b/.github/workflows/docs-publish.yml
new file mode 100644
index 0000000000..689d575621
--- /dev/null
+++ b/.github/workflows/docs-publish.yml
@@ -0,0 +1,312 @@
+name: Daily documentation
+'on':
+  schedule:
+  - cron: 23 6 * * *
+  workflow_dispatch: {}
+concurrency:
+  group: daily-documentation-${{ github.ref }}
+  cancel-in-progress: false
+permissions:
+  contents: read
+  actions: write
+  pages: write
+  id-token: write
+jobs:
+  prepare:
+    runs-on: ubuntu-latest
+    outputs:
+      build_revision: ${{ steps.identity.outputs.revision }}
+    steps:
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+      with:
+        persist-credentials: false
+    - name: Identify compiled sources
+      id: identity
+      run: |
+        revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
+        echo "revision=$revision" >> "$GITHUB_OUTPUT"
+  exposition:
+    needs: prepare
+    runs-on: ubuntu-latest
+    name: Build exposition site
+    permissions:
+      contents: read
+      actions: write
+    steps:
+    - name: Checkout project
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+      with:
+        persist-credentials: false
+    - 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.prepare.outputs.build_revision }}
+        restore-keys: |
+          LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+    - 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
+        ~/.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
+    - 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: push
+      run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+    - name: Build pool
+      run: ~/.elan/bin/lake build LeanPool
+    - name: Restore project extraction cache
+      id: extraction-cache
+      uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+      with:
+        path: .lake/exposition-cache/v1
+        key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml',
+          'scripts/exposition/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') }}-
+    - name: Extract declarations
+      env:
+        LEAN_CMD: /home/runner/.elan/bin/lean
+        EXTRACT_JOBS: '2'
+      run: ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh exposition-dump.jsonl exposition-commands.jsonl
+    - name: Save project extraction cache
+      id: extraction-cache-save
+      if: always() && steps.extraction-cache.outcome == 'success' && steps.extraction-cache.outputs.cache-hit !=
+        'true'
+      uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
+      with:
+        path: .lake/exposition-cache/v1
+        key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
+    - name: Upload extraction timings and logs
+      if: always()
+      uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+      with:
+        name: exposition-extraction-diagnostics
+        path: |
+          .lake/exposition-timings.json
+          .lake/exposition-cache/v1/**/extract.log
+          .lake/exposition-cache/v1/**/failed.log
+        include-hidden-files: true
+        retention-days: 7
+    - name: Install uv
+      uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+      with:
+        enable-cache: true
+    - name: Generate site
+      run: |
+        cd python
+        uv sync --locked
+        uv run python -m lean_pool.exposition \
+          --dump ../exposition-dump.jsonl \
+          --commands ../exposition-commands.jsonl \
+          --repo-root .. \
+          --out ../exposition-site \
+          --commit ${{ github.sha }}
+    - name: Upload exposition artifact
+      uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+      with:
+        name: exposition-site
+        path: exposition-site
+        if-no-files-found: error
+        retention-days: 3
+    timeout-minutes: 330
+  analysis_1:
+    needs:
+    - prepare
+    uses: ./.github/workflows/docs-build.yml
+    with:
+      phase: analysis
+      stage: '1'
+      build_revision: ${{ needs.prepare.outputs.build_revision }}
+  analysis_2:
+    needs:
+    - prepare
+    - analysis_1
+    uses: ./.github/workflows/docs-build.yml
+    with:
+      phase: analysis
+      stage: '2'
+      build_revision: ${{ needs.prepare.outputs.build_revision }}
+      previous_complete: ${{ needs.analysis_1.outputs.complete }}
+  analysis_3:
+    needs:
+    - prepare
+    - analysis_2
+    uses: ./.github/workflows/docs-build.yml
+    with:
+      phase: analysis
+      stage: '3'
+      build_revision: ${{ needs.prepare.outputs.build_revision }}
+      previous_complete: ${{ needs.analysis_2.outputs.complete }}
+  analysis_4:
+    needs:
+    - prepare
+    - analysis_3
+    uses: ./.github/workflows/docs-build.yml
+    with:
+      phase: analysis
+      stage: '4'
+      build_revision: ${{ needs.prepare.outputs.build_revision }}
+      previous_complete: ${{ needs.analysis_3.outputs.complete }}
+  analysis_complete:
+    needs: analysis_4
+    runs-on: ubuntu-latest
+    steps:
+    - name: Require complete analysis before rendering
+      env:
+        COMPLETE: ${{ needs.analysis_4.outputs.complete }}
+      run: |
+        if [ "$COMPLETE" != true ]; then
+          echo "::error::Documentation analysis remains incomplete; verified progress is saved for the next run."
+          exit 1
+        fi
+  build:
+    needs:
+    - prepare
+    - analysis_complete
+    uses: ./.github/workflows/docs-build.yml
+    with:
+      phase: render
+      stage: render
+      build_revision: ${{ needs.prepare.outputs.build_revision }}
+  deployment_freshness:
+    needs:
+    - exposition
+    - build
+    if: github.ref == 'refs/heads/main'
+    runs-on: ubuntu-latest
+    name: Check deployment freshness
+    outputs:
+      deploy: ${{ steps.check.outputs.deploy }}
+    steps:
+    - name: Compare with latest Documentation run
+      id: check
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        set -euo pipefail
+        latest_run=$(gh api --method GET \
+          "repos/${GITHUB_REPOSITORY}/actions/workflows/docs-publish.yml/runs" \
+          -f branch=main -F exclude_pull_requests=true -F per_page=1 \
+          --jq '.workflow_runs[0].run_number')
+        if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then
+          echo "::error::Could not determine the latest Documentation run on main."
+          exit 1
+        fi
+        if (( latest_run > GITHUB_RUN_NUMBER )); then
+          echo "deploy=false" >> "$GITHUB_OUTPUT"
+          echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run."
+        else
+          echo "deploy=true" >> "$GITHUB_OUTPUT"
+        fi
+  deploy:
+    needs:
+    - exposition
+    - build
+    - deployment_freshness
+    if: needs.deployment_freshness.outputs.deploy == 'true'
+    runs-on: ubuntu-latest
+    name: Deploy documentation
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+    - name: Download documentation artifact
+      uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+      with:
+        name: documentation-site
+        path: site
+    - name: Download exposition artifact
+      uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+      with:
+        name: exposition-site
+        path: site/exposition
+    - name: Validate assembled Pages tree
+      run: |
+        set -euo pipefail
+        test -s site/index.html
+        test -s site/exposition/index.html
+        test -s site/exposition/decls/index.html
+        test -s site/exposition/assets/landing.js
+        test -s site/exposition/data/decls.json
+        jq -e --arg commit "$GITHUB_SHA" '
+          .commit == $commit
+          and (.projects | length > 0)
+          and (.totals.projects == (.projects | length))
+          and (.totals.decls > 0)
+        ' site/exposition/data/index.json > /dev/null
+        first_project=$(jq -r '.projects[0].slug' site/exposition/data/index.json)
+        test -s "site/exposition/p/${first_project}/index.html"
+        mkdir -p site/deployments
+        printf '%s\n' "$GITHUB_SHA" > "site/deployments/${GITHUB_SHA}.txt"
+        test "$(cat site/SOURCE_SHA)" = "$GITHUB_SHA"
+    - name: Configure Pages
+      uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b
+    - name: Upload Pages artifact
+      uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b
+      with:
+        path: site
+    - name: Recheck deployment freshness
+      id: final-freshness
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        set -euo pipefail
+        latest_run=$(gh api --method GET \
+          "repos/${GITHUB_REPOSITORY}/actions/workflows/docs-publish.yml/runs" \
+          -f branch=main -F exclude_pull_requests=true -F per_page=1 \
+          --jq '.workflow_runs[0].run_number')
+        if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then
+          echo "::error::Could not determine the latest Documentation run on main."
+          exit 1
+        fi
+        if (( latest_run > GITHUB_RUN_NUMBER )); then
+          echo "deploy=false" >> "$GITHUB_OUTPUT"
+          echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run."
+        else
+          echo "deploy=true" >> "$GITHUB_OUTPUT"
+        fi
+    - name: Deploy Pages
+      id: deployment
+      if: steps.final-freshness.outputs.deploy == 'true'
+      uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128
+    - name: Verify deployed site
+      if: steps.final-freshness.outputs.deploy == 'true'
+      env:
+        PAGE_URL: ${{ steps.deployment.outputs.page_url }}
+      run: |
+        curl --fail --silent --show-error \
+          --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \
+          --output deployed-commit.txt \
+          "${PAGE_URL%/}/deployments/${GITHUB_SHA}.txt"
+        cmp "site/deployments/${GITHUB_SHA}.txt" deployed-commit.txt
+        curl --fail --silent --show-error \
+          --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \
+          --output /dev/null \
+          "${PAGE_URL%/}/exposition/index.html"
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 3e4aeb1480..6b3b0ec462 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -3,48 +3,16 @@ name: Documentation
 on:
   merge_group:
     types: [checks_requested]
-  push:
-    branches:
-      - main
-    paths:
-      - '**/*.lean'
-      - 'LeanPool/projects/**'
-      - 'LeanPool/projects.yml'
-      - 'lakefile.toml'
-      - 'lake-manifest.json'
-      - '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'
-      - 'python/lean_pool/ci_cache.py'
-      - 'python/lean_pool/rebase_fastpath.py'
-      - 'scripts/exposition/**'
-      - '.github/workflows/docs.yml'
   pull_request:
     branches:
       - main
-  workflow_dispatch:
-    inputs:
-      preview:
-        description: "Generate full documentation for this branch on demand"
-        type: boolean
-        required: false
-        default: false
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
-  # PR updates should supersede stale work, but the first main build after a
-  # toolchain bump must be allowed to finish and seed the new caches.
-  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
+  cancel-in-progress: true
 
 permissions:
   contents: read
-  pages: write
-  id-token: write
   actions: read
 
 jobs:
@@ -72,14 +40,12 @@ jobs:
               files=$(git diff --name-only --no-renames "$BASE"..HEAD)
             fi
             # Git may quote names containing Unicode or control characters.
-            if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then
+            if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs[^/]*\.yml$)' <<< "$files"; then
               applicable=true
             fi
           fi
           echo "applicable=$applicable" >> "$GITHUB_OUTPUT"
-  # Fail cheap consistency checks before either multi-hour documentation job
-  # starts. In particular, a stale generated root should not spend runner time
-  # building documentation that cannot be merged.
+  # Cheap configuration/index checks remain independent of daily publication.
   preflight:
     needs: scope
     if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
@@ -217,523 +183,3 @@ jobs:
       - name: Check regenerated LeanPool root without Lean
         if: steps.rebase.outputs.rebase_only == 'true'
         run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index
-
-  # Runs in parallel with the doc-gen4 build; its (small) artifact is merged
-  # into the Pages tree by the `deploy` job. Restores the root build cache but
-  # never saves it — Lean Action CI owns that cache, while the documentation
-  # jobs own doc-gen's separate caches.
-  exposition:
-    # Exposition consumes compiled Lean, not doc-gen's Mathlib SQLite data.
-    # Reuse the matching CI artifact directly instead of waiting for docInfo.
-    needs: preflight
-    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 exposition 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') }}-
-
-      - 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
-          ~/.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
-
-      - 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"
-
-      - name: Build pool
-        run: ~/.elan/bin/lake build LeanPool
-
-      - name: Restore project extraction cache
-        id: extraction-cache
-        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
-        with:
-          path: .lake/exposition-cache/v1
-          key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/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') }}-
-
-      - name: Extract declarations
-        # Per-project environments (see extract-all.sh); 2-way parallel to
-        # stay inside the runner's memory.
-        env:
-          LEAN_CMD: /home/runner/.elan/bin/lean
-          EXTRACT_JOBS: "2"
-        run: >-
-          ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh
-          exposition-dump.jsonl exposition-commands.jsonl
-
-      - name: Save project extraction cache
-        id: extraction-cache-save
-        # A failed project must not discard its completed siblings. The reader
-        # accepts only fingerprinted, digest-verified output pairs.
-        if: always() && steps.extraction-cache.outcome == 'success' && steps.extraction-cache.outputs.cache-hit != 'true'
-        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
-        with:
-          path: .lake/exposition-cache/v1
-          key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
-
-      - name: Upload extraction timings and logs
-        if: always()
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        with:
-          name: exposition-extraction-diagnostics
-          path: |
-            .lake/exposition-timings.json
-            .lake/exposition-cache/v1/**/extract.log
-            .lake/exposition-cache/v1/**/failed.log
-          include-hidden-files: true
-          retention-days: 7
-
-      - name: Install uv
-        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
-        with:
-          enable-cache: true
-
-      - name: Generate site
-        run: |
-          cd python
-          uv sync --locked
-          uv run python -m lean_pool.exposition \
-            --dump ../exposition-dump.jsonl \
-            --commands ../exposition-commands.jsonl \
-            --repo-root .. \
-            --out ../exposition-site \
-            --commit ${{ github.sha }}
-
-      - name: Upload exposition artifact
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        with:
-          name: exposition-site
-          path: exposition-site
-          if-no-files-found: error
-          retention-days: 3
-
-  # Mathlib dominates a cold doc-gen bootstrap. Give it a separate job and
-  # persist the verified SQLite checkpoint immediately, before any pool module
-  # can consume the remainder of GitHub's six-hour job limit.
-  mathlib_doc_info:
-    needs: preflight
-    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 Mathlib documentation data
-    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') }}
-
-      # Mathlib's compiled artifacts come from the dependency cache; doc-gen's
-      # SQLite data and extra dependencies have their own checkpoint.
-      - name: Restore Mathlib documentation checkpoint
-        id: mathlib-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: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
-
-      - name: Install Lean
-        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-
-      - name: Install and verify Mathlib cache
-        run: |
-          set -euo pipefail
-          ~/.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
-
-      # Lake materializes the exact dependencies in docbuild/lake-manifest.json;
-      # do not run `lake update`, which can re-resolve and rewrite that lockfile.
-      - name: Build Mathlib documentation data
-        run: cd docbuild && ~/.elan/bin/lake build Mathlib:docInfo
-
-      - name: Validate Mathlib documentation checkpoint
-        run: |
-          set -euo pipefail
-          test -s docbuild/.lake/build/api-docs.db
-          test -n "$(find docbuild/.lake/build/doc-data -type f -name 'Mathlib*.doc' -print -quit)"
-          python3 - <<'PY'
-          import sqlite3
-
-          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
-
-      # PR caches remain scoped to refs/pull/N/merge, so saving here safely
-      # hands the cold checkpoint to this workflow's downstream job and reruns.
-      - name: Save Mathlib documentation checkpoint
-        if: steps.mathlib-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: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
-
-  build:
-    needs:
-      - preflight
-      - mathlib_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') }}-
-
-      # 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.
-      - 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: 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 }}
-          restore-keys: |
-            DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-
-
-      - name: Restore Mathlib documentation checkpoint
-        if: steps.pool-doc-cache.outputs.cache-matched-key == ''
-        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: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
-          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
-          ~/.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
-
-      - 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"
-
-      # 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
-
-      - name: Validate pool documentation checkpoint
-        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
-
-          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: Save 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: 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: Build documentation
-        run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs
-
-      - 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
-
-      - 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'
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
-        with:
-          name: documentation-site
-          path: docbuild/.lake/build/doc
-          if-no-files-found: error
-          retention-days: 3
-
-  # Main bootstrap runs are intentionally not cancelled because they may be
-  # the only producer of a new compatibility cache. If main advanced while a
-  # run was building, retain those caches but never enter the Pages environment
-  # or deploy stale HTML.
-  deployment_freshness:
-    needs:
-      - exposition
-      - build
-    if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'
-    runs-on: ubuntu-latest
-    name: Check deployment freshness
-    outputs:
-      deploy: ${{ steps.check.outputs.deploy }}
-    steps:
-      - name: Compare with latest Documentation run
-        id: check
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          set -euo pipefail
-          latest_run=$(gh api --method GET \
-            "repos/${GITHUB_REPOSITORY}/actions/workflows/docs.yml/runs" \
-            -f branch=main -F exclude_pull_requests=true -F per_page=1 \
-            --jq '.workflow_runs[0].run_number')
-          if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then
-            echo "::error::Could not determine the latest Documentation run on main."
-            exit 1
-          fi
-          if (( latest_run > GITHUB_RUN_NUMBER )); then
-            echo "deploy=false" >> "$GITHUB_OUTPUT"
-            echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run."
-          else
-            echo "deploy=true" >> "$GITHUB_OUTPUT"
-          fi
-
-  # The two expensive sites build independently after preflight.
-  # Let the dependency graph join them instead of racing one job against a
-  # polling timeout. If either build fails, no incomplete tree is deployed.
-  deploy:
-    needs:
-      - exposition
-      - build
-      - deployment_freshness
-    if: needs.deployment_freshness.outputs.deploy == 'true'
-    runs-on: ubuntu-latest
-    name: Deploy documentation
-    environment:
-      name: github-pages
-      url: ${{ steps.deployment.outputs.page_url }}
-    steps:
-      - name: Download documentation artifact
-        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
-        with:
-          name: documentation-site
-          path: site
-
-      - name: Download exposition artifact
-        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
-        with:
-          name: exposition-site
-          path: site/exposition
-
-      - name: Validate assembled Pages tree
-        run: |
-          set -euo pipefail
-          test -s site/index.html
-          test -s site/exposition/index.html
-          test -s site/exposition/decls/index.html
-          test -s site/exposition/assets/landing.js
-          test -s site/exposition/data/decls.json
-          jq -e --arg commit "$GITHUB_SHA" '
-            .commit == $commit
-            and (.projects | length > 0)
-            and (.totals.projects == (.projects | length))
-            and (.totals.decls > 0)
-          ' site/exposition/data/index.json > /dev/null
-          first_project=$(jq -r '.projects[0].slug' site/exposition/data/index.json)
-          test -s "site/exposition/p/${first_project}/index.html"
-          mkdir -p site/deployments
-          printf '%s\n' "$GITHUB_SHA" > "site/deployments/${GITHUB_SHA}.txt"
-
-      - name: Configure Pages
-        uses: actions/configure-pages@983d7736d9b0ae728b81ab479565c72886d7745b
-
-      - name: Upload Pages artifact
-        uses: actions/upload-pages-artifact@7b1f4a764d45c48632c6b24a0339c27f5614fb0b
-        with:
-          path: site
-
-      # Narrow the race between the gate job and the irreversible deployment.
-      # Comparing workflow runs (rather than raw main HEAD) deliberately ignores
-      # newer commits that do not match this workflow's path filters.
-      - name: Recheck deployment freshness
-        id: final-freshness
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          set -euo pipefail
-          latest_run=$(gh api --method GET \
-            "repos/${GITHUB_REPOSITORY}/actions/workflows/docs.yml/runs" \
-            -f branch=main -F exclude_pull_requests=true -F per_page=1 \
-            --jq '.workflow_runs[0].run_number')
-          if ! [[ "$latest_run" =~ ^[0-9]+$ ]]; then
-            echo "::error::Could not determine the latest Documentation run on main."
-            exit 1
-          fi
-          if (( latest_run > GITHUB_RUN_NUMBER )); then
-            echo "deploy=false" >> "$GITHUB_OUTPUT"
-            echo "::notice::Skipping superseded Documentation run $GITHUB_RUN_NUMBER; main has run $latest_run."
-          else
-            echo "deploy=true" >> "$GITHUB_OUTPUT"
-          fi
-
-      - name: Deploy Pages
-        id: deployment
-        if: steps.final-freshness.outputs.deploy == 'true'
-        uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128
-
-      - name: Verify deployed site
-        if: steps.final-freshness.outputs.deploy == 'true'
-        env:
-          PAGE_URL: ${{ steps.deployment.outputs.page_url }}
-        run: |
-          curl --fail --silent --show-error \
-            --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \
-            --output deployed-commit.txt \
-            "${PAGE_URL%/}/deployments/${GITHUB_SHA}.txt"
-          cmp "site/deployments/${GITHUB_SHA}.txt" deployed-commit.txt
-          curl --fail --silent --show-error \
-            --retry 30 --retry-delay 10 --retry-all-errors --retry-max-time 300 \
-            --output /dev/null \
-            "${PAGE_URL%/}/exposition/index.html"
diff --git a/docbuild/README.md b/docbuild/README.md
new file mode 100644
index 0000000000..ecff8ef95a
--- /dev/null
+++ b/docbuild/README.md
@@ -0,0 +1,68 @@
+# Daily documentation
+
+API documentation and exposition publish through
+[Daily documentation](../.github/workflows/docs-publish.yml) at **06:23 UTC daily**.
+Maintainers can also dispatch that workflow manually. Publication never runs on a
+PR, merge group or ordinary push. The independent `Documentation preflight`
+check still validates workspace compatibility and generated indexes.
+
+Each run uses one fixed Git revision. The previously published site stays online
+until API documentation and exposition both pass validation. `/SOURCE_SHA` and
+`/deployments/<commit>.txt` identify the published revision. A manual dispatch
+on another branch produces build artifacts but cannot publish Pages.
+
+## Incremental analysis
+
+The pinned doc-gen fork implements interproject linking from upstream
+[PR396](https://github.com/leanprover/doc-gen4/pull/396). Only `LeanPool` modules
+receive full analysis and HTML pages. Mathlib and Lean references link to hosted
+Mathlib documentation; Tau Ceti references link to its own documentation. These
+sites may describe a different dependency revision, so declaration links use
+their name resolver. Toolchain upgrades must select a compatible doc-gen revision
+as well as updating the nested manifest.
+
+The runtime discovers every local module directly. It never modifies the empty
+production `LeanPool.lean` or loads an import-all Lean environment. After local
+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.
+
+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
+the completed work is saved. A build error fails the stage and does not publish
+a checkpoint from the failed batch. Every saved database passes SQLite integrity
+and WAL checks. Checkpoint keys include the run, attempt and stage; cache
+maintenance retains the latest saved main checkpoint.
+
+If all four allowances are used, the run reports failure and leaves the site
+unchanged. The next daily or manually dispatched run resumes saved progress.
+Repeated no-progress failures require diagnosis rather than repeated retries.
+
+HTML rendering has its own job budget and requires complete analysis for the
+same snapshot. Validation requires a page for every local module, rejects
+accidentally rendered dependency trees and verifies the source marker when the
+two sites are assembled. Announcement jobs continue to defer projects whose
+published documentation is unavailable.
+
+## Local commands
+
+From the repository root, after fetching the compiled Lean artifacts:
+
+```bash
+export DOCGEN_LOCAL_MODULE_ROOTS=LeanPool
+export DOCGEN_DEPS_DOCS_URL=https://leanprover-community.github.io/mathlib4_docs
+export DOCGEN_DEPS_DOCS_URLS=TauCeti=https://taucetiproject.github.io/TauCeti/docs
+PYTHONPATH=python python3 -m lean_pool.documentation prepare
+PYTHONPATH=python python3 -m lean_pool.documentation batch --seconds 5400
+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;
+GitHub Actions reports publishing failures separately from PR validation.
diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
index a8f7ef65e7..969915f1e3 100644
--- a/docbuild/lake-manifest.json
+++ b/docbuild/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.3.0",
  "packagesDir": "../.lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/doc-gen4",
+ [{"url": "https://github.com/kim-em/doc-gen4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "20b0edcaf3d2882fe2c906158e79f2f5dbebe57c",
+   "scope": "",
+   "rev": "9a591946b68fbb4cec5355d0c7a8187a0984c6ba",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc3",
+   "inputRev": "9a591946b68fbb4cec5355d0c7a8187a0984c6ba",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
index 2ee0bea710..0d591dc528 100644
--- a/docbuild/lakefile.toml
+++ b/docbuild/lakefile.toml
@@ -8,6 +8,7 @@ name = "lean-pool"
 path = "../"
 
 [[require]]
-scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.35.0-rc3"
+git = "https://github.com/kim-em/doc-gen4"
+# Interproject linking, pinned to the Lean v4.35.0-rc3-compatible revision.
+rev = "9a591946b68fbb4cec5355d0c7a8187a0984c6ba"
diff --git a/python/lean_pool/ci_cache.py b/python/lean_pool/ci_cache.py
index e90aba847d..b33b36acd7 100644
--- a/python/lean_pool/ci_cache.py
+++ b/python/lean_pool/ci_cache.py
@@ -17,6 +17,7 @@
     "LeanValidation-v1-",
     "DocsInfo-v3-",
     "DocsInfoMathlib-v3-",
+    "DocsState-v1-",
     "Exposition-v1-",
 )
 
diff --git a/python/lean_pool/documentation.py b/python/lean_pool/documentation.py
new file mode 100644
index 0000000000..b18f10ff7f
--- /dev/null
+++ b/python/lean_pool/documentation.py
@@ -0,0 +1,322 @@
+"""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.
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import logging
+import os
+import re
+import shutil
+import signal
+import sqlite3
+import subprocess
+import tempfile
+import time
+from contextlib import contextmanager
+from graphlib import TopologicalSorter
+from pathlib import Path
+
+from lean_pool.exposition.source_text import code_view
+from lean_pool.indexes import structure_errors
+
+LOGGER = logging.getLogger(__name__)
+IMPORTS = re.compile(
+    r"(?m)^\s*(?:(?:public|private|meta)\s+)*import\s+(?:all\s+)?([^\n]+)"
+)
+STATE = "documentation-progress.json"
+
+
+def module_sources(root: Path) -> dict[str, Path]:
+    """Discover every local module, including the empty library root."""
+    paths = [root / "LeanPool.lean", *sorted((root / "LeanPool").rglob("*.lean"))]
+    return {
+        ".".join(path.relative_to(root).with_suffix("").parts): path for path in paths
+    }
+
+
+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())
+        digest.update(b"\0" + path.read_bytes() + b"\0")
+    for name in (
+        "DOCGEN_LOCAL_MODULE_ROOTS",
+        "DOCGEN_DEPS_DOCS_URL",
+        "DOCGEN_DEPS_DOCS_URLS",
+    ):
+        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."""
+    sources = module_sources(root)
+    graph = {}
+    for name, path in sources.items():
+        imports = {
+            item
+            for line in IMPORTS.findall(code_view(path.read_text()))
+            for item in line.split()
+        }
+        graph[name] = sorted(imports & sources.keys())
+    return list(TopologicalSorter(graph).static_order())
+
+
+def prepare(root: Path) -> None:
+    """Require complete indexes and identical shared dependency/toolchain pins."""
+    errors = structure_errors(root)
+    if errors:
+        raise ValueError(f"invalid project aggregates: {errors[:3]}")
+    if (root / "lean-toolchain").read_bytes() != (
+        root / "docbuild" / "lean-toolchain"
+    ).read_bytes():
+        raise ValueError("documentation toolchain differs from the pool")
+    manifests = [
+        json.loads((directory / "lake-manifest.json").read_text())
+        for directory in (root, root / "docbuild")
+    ]
+    packages = [
+        {item["name"].strip("«»"): item for item in manifest["packages"]}
+        for manifest in manifests
+    ]
+    for name, package in packages[0].items():
+        inherited = packages[1].get(name, {})
+        if any(package.get(field) != inherited.get(field) for field in ("url", "rev")):
+            raise ValueError(f"documentation dependency differs from the pool: {name}")
+
+
+def external_modules(root: Path) -> list[str]:
+    """Collect external links without loading a combined pool environment."""
+    sources = module_sources(root)
+    imports = {"Init", "Std", "Lean", "Lake"}
+    for path in sources.values():
+        imports.update(
+            item
+            for line in IMPORTS.findall(code_view(path.read_text()))
+            for item in line.split()
+            if item not in sources
+        )
+    return sorted(imports)
+
+
+def validate_database(build: Path) -> None:
+    """Check a closed batch's SQLite state before retaining it."""
+    database = build / "api-docs.db"
+    if not database.is_file() or database.stat().st_size == 0:
+        raise ValueError("documentation database is missing or empty")
+    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}")
+
+
+@contextmanager
+def batch_checkpoint(build: Path):
+    """Restore the last complete database/marker pair if a batch fails or times out."""
+    build.mkdir(parents=True, exist_ok=True)
+    with tempfile.TemporaryDirectory(prefix="lean-pool-docs-") as directory:
+        saved = Path(directory)
+        database = build / "api-docs.db"
+        if database.exists():
+            validate_database(build)
+            shutil.copy2(database, saved / database.name)
+        markers = build / "doc-data"
+        if markers.exists():
+            shutil.copytree(markers, saved / markers.name)
+        try:
+            yield
+        except BaseException:
+            for suffix in ("", "-wal", "-shm", "-journal"):
+                (build / f"api-docs.db{suffix}").unlink(missing_ok=True)
+            shutil.rmtree(markers, ignore_errors=True)
+            if (saved / database.name).exists():
+                shutil.copy2(saved / database.name, database)
+            if (saved / markers.name).exists():
+                shutil.copytree(saved / markers.name, markers)
+            raise
+
+
+def stop_build(process: subprocess.Popen) -> None:
+    """Stop descendants even when their failed parent has already exited."""
+    try:
+        os.killpg(process.pid, signal.SIGTERM)
+    except ProcessLookupError:
+        pass
+    try:
+        process.wait(timeout=5)
+    except subprocess.TimeoutExpired:
+        pass
+    # A parent can exit before a child that still holds the SQLite database.
+    try:
+        os.killpg(process.pid, signal.SIGKILL)
+    except ProcessLookupError:
+        pass
+    process.wait()
+
+
+def run_build(command: list[str], directory: Path, timeout: float) -> None:
+    """Bound a native build and reap its entire process group before rollback."""
+    process = subprocess.Popen(command, cwd=directory, start_new_session=True)
+    try:
+        status = process.wait(timeout=timeout)
+    except BaseException:
+        stop_build(process)
+        raise
+    if status:
+        stop_build(process)
+        raise subprocess.CalledProcessError(status, command)
+
+
+def build_batches(root: Path, lake: str, seconds: float, batch_size: int) -> bool:
+    """Advance verified module batches until complete or the time allowance ends."""
+    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
+    deadline = time.monotonic() + seconds
+    while cursor < len(modules) and time.monotonic() < deadline:
+        batch = modules[cursor : cursor + batch_size]
+        command = [lake, "build", *(f"+{name}:docInfo" for name in batch)]
+        try:
+            with batch_checkpoint(build):
+                run_build(
+                    command, root / "docbuild", max(1, deadline - time.monotonic())
+                )
+                validate_database(build)
+        except subprocess.TimeoutExpired:
+            if cursor == started:
+                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)
+
+
+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))}:
+        raise ValueError("documentation analysis is incomplete for this snapshot")
+    validate_database(build)
+
+
+def render(root: Path, lake: str) -> None:
+    """Render fresh local pages from the complete analysis checkpoint."""
+    require_complete(root)
+    build = root / "docbuild" / ".lake" / "build"
+    shutil.rmtree(build / "doc" / "LeanPool", ignore_errors=True)
+    # Loading one import-all Lean environment would combine the independent
+    # projects' memory requirements. The database already holds every local
+    # module; only external names need an environment before rendering it.
+    commands = [
+        [
+            "externals",
+            "--build",
+            ".lake/build",
+            "--srcDirs",
+            "..",
+            "api-docs.db",
+            *external_modules(root),
+        ],
+        [
+            "fromDb",
+            "--build",
+            ".lake/build",
+            "--manifest",
+            ".lake/build/doc-manifest.json",
+            ".lake/build/api-docs.db",
+        ],
+    ]
+    for command in commands:
+        subprocess.run(
+            [lake, "exe", "doc-gen4", *command], cwd=root / "docbuild", check=True
+        )
+    validate_site(root)
+    commit = subprocess.check_output(["git", "rev-parse", "HEAD"], cwd=root, text=True)
+    (build / "doc" / "SOURCE_SHA").write_text(commit)
+
+
+def validate_site(root: Path) -> None:
+    """Require every local module page and reject accidentally rendered dependencies."""
+    site = root / "docbuild" / ".lake" / "build" / "doc"
+    required = ["index.html", "declarations/declaration-data.bmp"]
+    required += [name.replace(".", "/") + ".html" for name in module_sources(root)]
+    missing = [
+        name
+        for name in required
+        if not (site / name).is_file() or (site / name).stat().st_size == 0
+    ]
+    if missing:
+        raise ValueError(f"missing documentation pages: {missing[:10]}")
+    for name in ("Mathlib", "TauCeti", "Init", "Std", "Lean", "Lake"):
+        if (site / name).exists() or (site / f"{name}.html").exists():
+            raise ValueError(f"unexpected dependency documentation: {name}")
+
+
+def main() -> None:
+    """Expose preparation, bounded analysis and complete-site rendering commands."""
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("command", choices=("prepare", "batch", "render", "validate"))
+    parser.add_argument("--repo", type=Path, default=Path("."))
+    parser.add_argument("--lake", default="lake")
+    parser.add_argument("--seconds", type=float, default=5400)
+    parser.add_argument("--batch-size", type=int, default=128)
+    arguments = parser.parse_args()
+    logging.basicConfig(level=logging.INFO)
+    root = arguments.repo.resolve()
+    if arguments.command == "prepare":
+        prepare(root)
+    elif arguments.command == "batch":
+        complete = build_batches(
+            root, arguments.lake, arguments.seconds, arguments.batch_size
+        )
+        if output := os.environ.get("GITHUB_OUTPUT"):
+            with Path(output).open("a") as stream:
+                stream.write(f"complete={str(complete).lower()}\n")
+    elif arguments.command == "render":
+        render(root, arguments.lake)
+    else:
+        require_complete(root)
+        validate_site(root)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py
index f8ec886aa9..3e79ee6e19 100644
--- a/python/tests/test_ci_cache_contract.py
+++ b/python/tests/test_ci_cache_contract.py
@@ -44,62 +44,33 @@ def test_shared_cache_paths_and_keys_match() -> None:
     assert contracts["build"][1] == (".lake/build",)
 
 
-def _docs_condition(condition: str, event: str, ref: str, preview: bool, readme: bool):
-    """Evaluate the small event predicate used by docs job allocation."""
-    expression = condition
-    values = {
-        "needs.preflight.outputs.readme_only": repr(str(readme).lower()),
-        "github.event_name": repr(event),
-        "github.ref": repr(ref),
-        "inputs.preview": repr(preview),
+def test_documentation_publishing_is_scheduled_and_independent() -> None:
+    """PRs retain preflight while generation runs only on schedule or dispatch."""
+    preflight = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())
+    assert set(preflight.get("on", preflight.get(True))) == {
+        "pull_request",
+        "merge_group",
     }
-    for name, value in values.items():
-        expression = expression.replace(name, value)
-    return eval(
-        expression.replace("&&", " and ").replace("||", " or "),
-        {"__builtins__": {}},
-        {},
-    )
-
-
-def test_docs_generate_on_main_and_explicit_preview_only() -> None:
-    """PRs scope preflight without allocating heavy docs runners."""
-    jobs = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())["jobs"]
-    assert jobs["preflight"]["name"] == "Documentation preflight"
-    assert jobs["preflight"]["needs"] == "scope"
-    scenarios = [
-        ("pull_request", "refs/pull/123/merge", False, False, False),
-        ("push", "refs/heads/main", False, False, True),
-        ("workflow_dispatch", "refs/heads/main", False, False, True),
-        ("workflow_dispatch", "refs/heads/topic", False, False, False),
-        ("workflow_dispatch", "refs/heads/topic", True, False, True),
-        ("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 event, ref, preview, readme, expected in scenarios:
-            assert (
-                _docs_condition(jobs[name]["if"], event, ref, preview, readme)
-                == expected
-            )
-    # Branch previews produce artifacts but cannot replace production Pages.
-    assert not _docs_condition(
-        jobs["deployment_freshness"]["if"],
+    assert set(preflight["jobs"]) == {"scope", "preflight"}
+    assert preflight["jobs"]["preflight"]["name"] == "Documentation preflight"
+    publishing = yaml.safe_load((WORKFLOWS / "docs-publish.yml").read_text())
+    assert set(publishing.get("on", publishing.get(True))) == {
+        "schedule",
         "workflow_dispatch",
-        "refs/heads/topic",
-        True,
-        False,
+    }
+    assert publishing["concurrency"]["cancel-in-progress"] is False
+    assert publishing["jobs"]["build"]["needs"] == ["prepare", "analysis_complete"]
+    stages = yaml.safe_load((WORKFLOWS / "docs-build.yml").read_text())
+    assert stages["env"]["DOCGEN_LOCAL_MODULE_ROOTS"] == "LeanPool"
+    assert "TauCeti=" in stages["env"]["DOCGEN_DEPS_DOCS_URLS"]
+    steps = stages["jobs"]["build"]["steps"]
+    names = [step.get("name") for step in steps]
+    assert names.index("Save completed analysis batches") > names.index(
+        "Analyze a bounded batch"
+    )
+    assert names.index("Render and validate the complete local API") > names.index(
+        "Save completed analysis batches"
     )
-
-
-def test_documentation_helper_changes_trigger_main_publishing() -> None:
-    """Documentation's preparation/rendering helpers also trigger publication."""
-    workflow = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())
-    events = workflow.get("on", workflow.get(True))
-    assert {
-        "python/lean_pool/documentation.py",
-        "python/lean_pool/indexes.py",
-    } <= set(events["push"]["paths"])
 
 
 def test_single_and_sharded_builds_use_validation_cache() -> None:
@@ -316,7 +287,7 @@ def test_assembly_restores_projects_once_and_main_owns_full_cache():
 def test_extraction_caches_survive_failure_and_retry_keys_can_advance():
     """Failed batches save verified siblings; immutable retry keys can gain work."""
     for workflow, job in (
-        ("docs.yml", "exposition"),
+        ("docs-publish.yml", "exposition"),
         ("exposition-verify.yml", "verify"),
     ):
         steps = yaml.safe_load((WORKFLOWS / workflow).read_text())["jobs"][job]["steps"]
diff --git a/python/tests/test_documentation.py b/python/tests/test_documentation.py
new file mode 100644
index 0000000000..460f02d977
--- /dev/null
+++ b/python/tests/test_documentation.py
@@ -0,0 +1,205 @@
+"""Exercise checkpoint recovery, dependency ordering and publication boundaries."""
+
+from __future__ import annotations
+
+import json
+import sqlite3
+import subprocess
+import sys
+from pathlib import Path
+
+import pytest
+import yaml
+
+from lean_pool import documentation
+
+
+@pytest.fixture
+def repository(tmp_path: Path) -> Path:
+    """Provide local modules with an import order different from their filenames."""
+    (tmp_path / "LeanPool").mkdir()
+    (tmp_path / "docbuild").mkdir()
+    (tmp_path / "LeanPool.lean").write_text("module\n")
+    (tmp_path / "LeanPool" / "A.lean").write_text(
+        "module\nimport all LeanPool.Z\n"
+        "/- public import LeanPool.A -/\n"
+        'def text := "import LeanPool.A"\n'
+    )
+    (tmp_path / "LeanPool" / "Z.lean").write_text("module\n")
+    for name in ("lakefile.toml", "lake-manifest.json", "lean-toolchain"):
+        (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")
+    return tmp_path
+
+
+def populate(build: Path, value: str = "previous") -> None:
+    """Write a real consistent SQLite database and its corresponding marker."""
+    build.mkdir(parents=True, exist_ok=True)
+    with sqlite3.connect(build / "api-docs.db") as connection:
+        connection.execute("CREATE TABLE IF NOT EXISTS contents (value TEXT)")
+        connection.execute("DELETE FROM contents")
+        connection.execute("INSERT INTO contents VALUES (?)", (value,))
+    (build / "doc-data").mkdir(exist_ok=True)
+    (build / "doc-data" / "module.doc").write_text(value)
+
+
+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)
+    assert modules.index("LeanPool.Z") < modules.index("LeanPool.A")
+    assert set(modules) == {"LeanPool", "LeanPool.A", "LeanPool.Z"}
+    assert documentation.external_modules(repository) == ["Init", "Lake", "Lean", "Std"]
+
+
+@pytest.mark.parametrize(
+    "error", [RuntimeError("failed"), subprocess.TimeoutExpired("lake", 1)]
+)
+def test_failed_batch_restores_database_and_markers(tmp_path: Path, error) -> None:
+    """A failed process must not leave half-updated data paired with valid markers."""
+    populate(tmp_path)
+    with pytest.raises(type(error)), documentation.batch_checkpoint(tmp_path):
+        populate(tmp_path, "incomplete")
+        (tmp_path / "doc-data" / "extra.doc").write_text("incomplete")
+        raise error
+    with sqlite3.connect(tmp_path / "api-docs.db") as connection:
+        assert connection.execute("SELECT value FROM contents").fetchall() == [
+            ("previous",)
+        ]
+    assert (tmp_path / "doc-data" / "module.doc").read_text() == "previous"
+    assert not (tmp_path / "doc-data" / "extra.doc").exists()
+    documentation.validate_database(tmp_path)
+
+
+def test_first_failed_batch_leaves_no_checkpoint(tmp_path: Path) -> None:
+    """An interrupted bootstrap must never look like an existing valid database."""
+    with pytest.raises(RuntimeError), documentation.batch_checkpoint(tmp_path):
+        populate(tmp_path)
+        raise RuntimeError("failed")
+    assert not (tmp_path / "api-docs.db").exists()
+    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)
+    assert documentation.build_batches(repository, "lake", 60, 2)
+    assert len(commands) == 2
+    documentation.require_complete(repository)
+    assert documentation.build_batches(repository, "lake", 60, 2)
+    assert len(commands) == 2
+    (repository / "LeanPool" / "Z.lean").write_text("module\n-- changed\n")
+    with pytest.raises(ValueError, match="incomplete"):
+        documentation.require_complete(repository)
+    assert documentation.build_batches(repository, "lake", 60, 2)
+    assert len(commands) == 4
+    monkeypatch.setenv("DOCGEN_DEPS_DOCS_URL", "https://example.com/new-docs")
+    with pytest.raises(ValueError, match="incomplete"):
+        documentation.require_complete(repository)
+
+
+def test_timeout_advances_only_completed_batches(repository: Path, monkeypatch) -> None:
+    """Timeout recovery keeps the prior batch and resumes at the interrupted target."""
+    calls = 0
+
+    def build(command, directory, timeout):
+        nonlocal calls
+        calls += 1
+        populate(directory / ".lake" / "build", str(calls))
+        if calls == 2:
+            raise subprocess.TimeoutExpired(command, 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
+    assert (build_path / "doc-data" / "module.doc").read_text() == "1"
+    with pytest.raises(ValueError, match="incomplete"):
+        documentation.require_complete(repository)
+    assert documentation.build_batches(repository, "lake", 60, 2)
+    assert calls == 3
+
+
+@pytest.mark.parametrize("failed_parent", [False, True])
+def test_native_build_failure_stops_child_writers(
+    tmp_path: Path, failed_parent: bool
+) -> None:
+    """A descendant cannot modify the restored checkpoint after its parent is killed."""
+    script = tmp_path / "parent.py"
+    result = tmp_path / "late-write"
+    child = (
+        "import time,pathlib; time.sleep(1); "
+        "pathlib.Path('late-write').write_text('bad')"
+    )
+    script.write_text(
+        "import subprocess,sys,time\n"
+        f"subprocess.Popen([sys.executable, '-c', {child!r}])\n"
+        + ("sys.exit(1)\n" if failed_parent else "time.sleep(60)\n")
+    )
+    error = (
+        subprocess.CalledProcessError if failed_parent else subprocess.TimeoutExpired
+    )
+    with pytest.raises(error):
+        documentation.run_build([sys.executable, str(script)], tmp_path, 0.2)
+    subprocess.run([sys.executable, "-c", "import time; time.sleep(1.1)"], check=True)
+    assert not result.exists()
+
+
+def test_site_requires_every_module_and_excludes_dependencies(repository: Path) -> None:
+    """A root-only site or accidental Mathlib tree cannot pass publication checks."""
+    site = repository / "docbuild" / ".lake" / "build" / "doc"
+    for name in ("index.html", "declarations/declaration-data.bmp", "LeanPool.html"):
+        path = site / name
+        path.parent.mkdir(parents=True, exist_ok=True)
+        path.write_text("content")
+    with pytest.raises(ValueError, match="missing documentation pages"):
+        documentation.validate_site(repository)
+    for name in ("A", "Z"):
+        (site / "LeanPool").mkdir(exist_ok=True)
+        (site / "LeanPool" / f"{name}.html").write_text("content")
+    documentation.validate_site(repository)
+    (site / "Mathlib").mkdir()
+    with pytest.raises(ValueError, match="unexpected dependency"):
+        documentation.validate_site(repository)
+
+
+@pytest.mark.parametrize(
+    "result,previous,phase,expected",
+    [
+        ("success", "false", "analysis", True),
+        ("failure", "false", "analysis", False),
+        ("cancelled", "false", "analysis", False),
+        ("skipped", "true", "analysis", True),
+        ("skipped", "false", "analysis", False),
+        ("skipped", "true", "render", False),
+    ],
+)
+def test_reused_analysis_propagates_completion(
+    tmp_path: Path, result: str, previous: str, phase: str, expected: bool
+) -> None:
+    """Propagate completed stages and reject failures or unintended skips."""
+    workflow = Path(__file__).resolve().parents[2] / ".github/workflows/docs-build.yml"
+    command = yaml.safe_load(workflow.read_text())["jobs"]["receipt"]["steps"][0]["run"]
+    output = tmp_path / "output"
+    process = subprocess.run(
+        ["bash", "-c", command],
+        env={
+            "RESULT": result,
+            "PREVIOUS": previous,
+            "PHASE": phase,
+            "COMPLETE": "true",
+            "GITHUB_OUTPUT": str(output),
+        },
+        capture_output=True,
+    )
+    assert (process.returncode == 0) == expected
+    if expected:
+        assert output.read_text() == "complete=true\n"