Limit each Lean file's build time in CI (60 min hard, 600 s per changed file)

.github/CODE_QUALITY.md

@@ -9,8 +9,9 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for
 [`lean_action_ci.yml`](workflows/lean_action_ci.yml) currently runs:
 
 - `lake exe mk_all --module --check` (the pool and project indexes must use `module` and `public import`)
-- `lake build LeanPool`
+- `lake build LeanPool`, with a 60-minute hard limit on every Lean process
 - a warning scan over the build log
+- a per-file build-time limit: every added or modified `LeanPool` file must build in under 600 s
 - the `LeanPoolLinters` compiler plugin, loaded by Lake for every LeanPool module
 - `lake exe runLinter` on `LeanPool`
 - `lake exe lint-style` on `LeanPool`
@@ -20,6 +21,17 @@ With `warningAsError = true` in `lakefile.toml`, every Lean warning is a
 compile error (locally too). The warning scan over the build log remains for
 warnings Lake itself prints.
 
+Build-time limits follow Tau Ceti's CI performance gate.
+[`build_time_limits.py`](../python/lean_pool/build_time_limits.py) wraps every CI
+`lake build` and stops any Lean process still running after 60 minutes, which fails
+the build. After the build, it reads Lake's per-module times from the log and fails
+when a file the PR adds or modifies took more than 600 s. Times are Lake's
+wall-clock times on GitHub's 4-vCPU runners. Existing files are checked only once a
+PR changes them. A changed file that CI reuses from an earlier run instead of compiling
+was checked in the run that compiled it: reused builds must match
+`build_time_limits.py`, so output compiled before the gate, or under different
+limits, is never reused.
+
 The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold.
 
 The compiler plugin enforces the 200-line proof cap during the normal build, using original

.github/workflows/lean_action_ci.yml

@@ -36,6 +36,7 @@ on:
       - 'lake-manifest.json'
       - 'LeanPool/projects/**'
       - 'LeanPool/projects.yml'
+      - 'python/lean_pool/build_time_limits.py'
       - 'python/lean_pool/quality.py'
       - 'python/lean_pool/registry.py'
       - 'python/lean_pool/indexes.py'
@@ -380,13 +381,22 @@ jobs:
 
       - name: Build project
         id: compilation
+        env:
+          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
         run: |
           set -euo pipefail
-          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
+          PYTHONPATH=python python3 -m lean_pool.build_time_limits watch -- ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
           if grep -nE '(^|: )warning:' lean-build.log; then
             echo "::error::Lean build emitted warnings; fix them before merging."
             exit 1
           fi
+          # Added or modified files must build in under 600 s; the watch wrapper
+          # above stops any Lean process that runs past 60 minutes.
+          if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
+             && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
+            PYTHONPATH=python python3 -m lean_pool.build_time_limits check \
+              --log lean-build.log --base "$BUILD_TIME_BASE"
+          fi
 
       # Main publishes the shared full build. A minimal-verifier PR publishes
       # only its own projects; the verifier overlays them on the main cache.
@@ -596,6 +606,7 @@ jobs:
       - name: Build this shard's projects
         env:
           PROJECTS: ${{ matrix.projects }}
+          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
         run: |
           set -euo pipefail
           touch "$RUNNER_TEMP/build-stamp"
@@ -609,11 +620,18 @@ jobs:
             modules="$modules $project_modules"
           done
           # shellcheck disable=SC2086 # modules is a space-separated list on purpose
-          ~/.elan/bin/lake build $modules 2>&1 | tee shard-build.log
+          PYTHONPATH=python python3 -m lean_pool.build_time_limits watch -- ~/.elan/bin/lake build $modules 2>&1 | tee shard-build.log
           if grep -nE '(^|: )warning:' shard-build.log; then
             echo "::error::Lean build emitted warnings; fix them before merging."
             exit 1
           fi
+          # Added or modified files must build in under 600 s; the watch wrapper
+          # above stops any Lean process that runs past 60 minutes.
+          if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
+             && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
+            PYTHONPATH=python python3 -m lean_pool.build_time_limits check \
+              --log shard-build.log --base "$BUILD_TIME_BASE"
+          fi
 
       # Ship only what this build produced; unchanged (cache-replayed)
       # files stay out, so `finalize` can layer the shard outputs onto the
@@ -771,13 +789,22 @@ jobs:
 
       - name: Build project
         id: compilation
+        env:
+          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
         run: |
           set -euo pipefail
-          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
+          PYTHONPATH=python python3 -m lean_pool.build_time_limits watch -- ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
           if grep -nE '(^|: )warning:' lean-build.log; then
             echo "::error::Lean build emitted warnings; fix them before merging."
             exit 1
           fi
+          # Added or modified files must build in under 600 s; the watch wrapper
+          # above stops any Lean process that runs past 60 minutes.
+          if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
+             && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
+            PYTHONPATH=python python3 -m lean_pool.build_time_limits check \
+              --log lean-build.log --base "$BUILD_TIME_BASE"
+          fi
 
       # Main publishes the shared full build. A minimal-verifier PR publishes
       # only its own projects; the verifier overlays them on the main cache.
@@ -1019,13 +1046,22 @@ jobs:
         run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index
 
       - name: Build combined Lean root
+        env:
+          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
         run: |
           set -euo pipefail
-          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
+          PYTHONPATH=python python3 -m lean_pool.build_time_limits watch -- ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
           if grep -nE '(^|: )warning:' lean-build.log; then
             echo "::error::Lean build emitted warnings; fix them before merging."
             exit 1
           fi
+          # Added or modified files must build in under 600 s; the watch wrapper
+          # above stops any Lean process that runs past 60 minutes.
+          if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
+             && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
+            PYTHONPATH=python python3 -m lean_pool.build_time_limits check \
+              --log lean-build.log --base "$BUILD_TIME_BASE"
+          fi
 
       - name: Install validation dependencies
         run: cd python && uv sync --locked

AGENTS.md

@@ -150,6 +150,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
 
+Every file has a build-time budget. Any file you add or modify must build in under 600 seconds on CI, and CI stops any single Lean process after 60 minutes. Split slow files or make their proofs cheaper; the advisory `/profile` report shows where the time goes.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines

CLAUDE.md

@@ -150,6 +150,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
 
+Every file has a build-time budget. Any file you add or modify must build in under 600 seconds on CI, and CI stops any single Lean process after 60 minutes. Split slow files or make their proofs cheaper; the advisory `/profile` report shows where the time goes.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines

CONTRIBUTING.md

@@ -51,6 +51,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
 
+Every file has a build-time budget. Any file you add or modify must build in under 600 seconds on CI, and CI stops any single Lean process after 60 minutes. Split slow files or make their proofs cheaper; the advisory `/profile` report shows where the time goes.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines