ci: cache per-project validation and defer full docs

.github/workflows/docs.yml

@@ -13,6 +13,9 @@ on:
       - 'lean-toolchain'
       - 'docbuild/**'
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/quality.py'
+      - 'python/lean_pool/challenge.py'
+      - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
       - 'scripts/exposition/**'
       - '.github/workflows/docs.yml'
@@ -34,11 +37,20 @@ on:
       - 'lean-toolchain'
       - 'docbuild/**'
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/quality.py'
+      - 'python/lean_pool/challenge.py'
+      - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
       - 'scripts/exposition/**'
       - '.github/workflows/notice.yml'
       - '.github/workflows/docs.yml'
   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 }}
@@ -157,7 +169,10 @@ jobs:
     # 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'
+    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
     steps:
@@ -278,7 +293,10 @@ jobs:
   # can consume the remainder of GitHub's six-hour job limit.
   mathlib_doc_info:
     needs: preflight
-    if: needs.preflight.outputs.readme_only != 'true'
+    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
     steps:
@@ -368,7 +386,10 @@ jobs:
     needs:
       - preflight
       - mathlib_doc_info
-    if: needs.preflight.outputs.readme_only != 'true'
+    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
     steps:

.github/workflows/lean_action_ci.yml

@@ -34,6 +34,7 @@ on:
       - 'Challenge/challenges.yml'
       - 'python/lean_pool/challenge.py'
       - 'python/lean_pool/quality.py'
+      - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
       - 'python/pyproject.toml'
       - 'python/uv.lock'
@@ -61,6 +62,7 @@ on:
       - 'Challenge/challenges.yml'
       - 'python/lean_pool/challenge.py'
       - 'python/lean_pool/quality.py'
+      - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
       - 'python/pyproject.toml'
       - 'python/uv.lock'
@@ -229,9 +231,11 @@ jobs:
       # Publish once compilation succeeds, so docs can overlap the later
       # linters/quality checks without compiling the same PR a second time.
       - name: Package build for documentation
+        if: github.event_name != 'pull_request'
         run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
 
       - name: Share build with documentation
+        if: github.event_name != 'pull_request'
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
@@ -240,9 +244,24 @@ jobs:
           compression-level: 0
           retention-days: 1
 
+      # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same
+      # PR can reuse receipts, while main and other PRs cannot read them.
+      - name: Restore project validation
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/validation-cache/v1
+          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          restore-keys: |
+            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+
+      - name: Install validation dependencies
+        run: cd python && uv sync --locked
+
       - name: Lint
         run: |
-          ~/.elan/bin/lake exe runLinter LeanPool
+          cd python
+          uv run python -m lean_pool.validation_cache lint --repo ..
+          cd ..
           ~/.elan/bin/lake exe runLinter Challenge
           ~/.elan/bin/lake exe runLinter Solution
 
@@ -255,8 +274,14 @@ jobs:
       - name: Repository quality checks
         run: |
           cd python
-          uv sync --locked
-          uv run python -m lean_pool.quality --repo ..
+          uv run python -m lean_pool.validation_cache quality --repo ..
+
+      - name: Save project validation
+        # Successful receipts are tiny; retain PR results across registry rebases.
+        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/validation-cache/v1
+          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
       - name: Save Lean dependencies
         if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
@@ -465,9 +490,11 @@ jobs:
       # Publish once compilation succeeds, so docs can overlap the later
       # linters/quality checks without compiling the same PR a second time.
       - name: Package build for documentation
+        if: github.event_name != 'pull_request'
         run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
 
       - name: Share build with documentation
+        if: github.event_name != 'pull_request'
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
           name: lean-pool-build
@@ -476,9 +503,24 @@ jobs:
           compression-level: 0
           retention-days: 1
 
+      # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same
+      # PR can reuse receipts, while main and other PRs cannot read them.
+      - name: Restore project validation
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/validation-cache/v1
+          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          restore-keys: |
+            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+
+      - name: Install validation dependencies
+        run: cd python && uv sync --locked
+
       - name: Lint
         run: |
-          ~/.elan/bin/lake exe runLinter LeanPool
+          cd python
+          uv run python -m lean_pool.validation_cache lint --repo ..
+          cd ..
           ~/.elan/bin/lake exe runLinter Challenge
           ~/.elan/bin/lake exe runLinter Solution
 
@@ -491,8 +533,14 @@ jobs:
       - name: Repository quality checks
         run: |
           cd python
-          uv sync --locked
-          uv run python -m lean_pool.quality --repo ..
+          uv run python -m lean_pool.validation_cache quality --repo ..
+
+      - name: Save project validation
+        # Successful receipts are tiny; retain PR results across registry rebases.
+        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/validation-cache/v1
+          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
       - name: Save Lean dependencies
         if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'

.github/workflows/python_ci.yml

@@ -9,6 +9,8 @@ on:
       - 'NOTICE'
       - 'NOTICE.extra.yml'
       - '.github/workflows/python_ci.yml'
+      - '.github/workflows/lean_action_ci.yml'
+      - '.github/workflows/docs.yml'
   pull_request:
     branches:
       - main
@@ -23,6 +25,8 @@ on:
       - 'NOTICE'
       - 'NOTICE.extra.yml'
       - '.github/workflows/python_ci.yml'
+      - '.github/workflows/lean_action_ci.yml'
+      - '.github/workflows/docs.yml'
   workflow_dispatch:
 
 concurrency:

python/ci-performance.md

@@ -71,3 +71,45 @@ for both output files on cold extraction, cache reuse, and forced refresh.
 Cache reuse took under a millisecond, versus 5–13 seconds for extraction on that
 machine. This is a small-project correctness check, not a whole-pool timing claim.
 Measure full-run savings after the main-branch extraction cache has been seeded.
+
+## Pull-request scheduling and project validation
+
+Pull requests retain the required `Documentation preflight` check, including
+workspace compatibility and generated-root checks. Full exposition/doc-gen
+jobs run on main; use the Documentation workflow's `preview` input to generate
+branch artifacts on demand. Branch previews never deploy production Pages.
+Ordinary PR builds no longer package the large documentation build artifact.
+
+After compilation, Lean CI partitions every pool source into project units,
+including Basic, the root, nested files and unregistered modules. Declaration
+lint, axiom audits and option-backdoor audits import all owned modules; each
+compiled declaration is checked in its owning unit. Registry declarations use
+separate per-entry receipts. Static checks (registry/card consistency,
+reachability, forbidden constructs, size limits and Lake options), text style
+lint, and Challenge/Solution validation still run every time.
+
+`.lake/validation-cache/v1/passes.json` contains successful receipts keyed by
+source contents, each module's transitive compiler import inventory, toolchain,
+dependency pins, build options and checker code. Missing import inventories
+conservatively hash all local Lean sources. Changes to a project's registry
+entry invalidate its declaration check without invalidating sibling projects.
+Adding, deleting or editing modules changes the validation coverage. Failed
+checks never publish receipts. A registry-only rebase can therefore reuse
+proof validation while still checking the registry and generated cards.
+
+Actions saves the small receipt cache after all gates pass. PR cache scope is
+`refs/pull/<n>/merge`, so a PR can reuse its previous validation across rebases,
+but main and other PRs cannot consume its receipts. Main receipts are available
+to all branches. The first run after shipping, a toolchain bump or a checker
+change remains cold; subsequent runs should avoid validating unchanged projects.
+
+To bypass receipts for comparison, from `python/`:
+
+```sh
+uv run python -m lean_pool.validation_cache lint --repo .. --refresh
+uv run python -m lean_pool.validation_cache quality --repo .. --refresh
+```
+
+This does not eliminate GitHub's strict up-to-date check requirement or registry
+merge conflicts. CI still runs for a new merge result, with compilation handled
+by Lake's existing incremental build cache and validation reused by content.