From 3d0638357be5982a188c4fc5140e03822bfa554e Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 6 Nov 2026 21:03:26 -0800 Subject: [PATCH 1/2] Limit each Lean file's build time in CI Every CI `lake build` now runs under a watchdog that stops any Lean process still running after 60 minutes. After the build, CI reads Lake's per-module times from the log and fails when a file the PR adds or modifies took more than 600 seconds. Existing files are checked only once a PR changes them. Co-Authored-By: Claude Opus 5.5 --- .github/CODE_QUALITY.md | 11 +- .github/workflows/lean_action_ci.yml | 44 +++- AGENTS.md | 2 + CLAUDE.md | 2 + CONTRIBUTING.md | 2 + python/lean_pool/build_time_limits.py | 284 +++++++++++++++++++++++++ python/tests/test_build_time_limits.py | 134 ++++++++++++ 7 files changed, 474 insertions(+), 5 deletions(-) create mode 100644 python/lean_pool/build_time_limits.py create mode 100644 python/tests/test_build_time_limits.py diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index 26b70e009c..7fcd6c2099 100644 --- a/.github/CODE_QUALITY.md +++ b/.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,14 @@ 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. + 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 diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 50ea670779..126db30073 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.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 diff --git a/AGENTS.md b/AGENTS.md index 2f18b3ee51..934a9f2a5e 100644 --- a/AGENTS.md +++ b/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 diff --git a/CLAUDE.md b/CLAUDE.md index 2f18b3ee51..934a9f2a5e 100644 --- a/CLAUDE.md +++ b/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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2cb4e6e4d0..e8b2fcd23d 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/python/lean_pool/build_time_limits.py b/python/lean_pool/build_time_limits.py new file mode 100644 index 0000000000..f3773ab7b0 --- /dev/null +++ b/python/lean_pool/build_time_limits.py @@ -0,0 +1,284 @@ +"""Enforce Lean Pool's per-file build-time limits in CI. + +Two limits apply, following Tau Ceti's CI performance gate: + +* ``watch`` runs a build command and kills any Lean process it spawns that runs + longer than the hard limit (60 minutes), so no single file can stall CI. +* ``check`` reads a Lake build log and fails when an added or modified pool file + took longer than the per-file limit (600 seconds) to build. + +Existing files are only checked once a PR changes them. Times are the wall-clock +times Lake reports for each module on the CI runner. Standard library only, so CI +can run it with the runner's ``python3`` before ``uv`` is installed. +""" + +from __future__ import annotations + +import argparse +import logging +import os +import re +import signal +import subprocess +import sys +import time +from dataclasses import dataclass +from pathlib import Path + +LOGGER = logging.getLogger(__name__) + +PROCESS_LIMIT_SECONDS = 3600 +FILE_LIMIT_SECONDS = 600 +POLL_SECONDS = 15 +TERMINATE_GRACE_SECONDS = 30 + +_BUILT_LINE = re.compile( + r"Built (?PLeanPool(?:\.[^\s:()]+)+) " + r"\((?P\d+(?:\.\d+)?)(?Pms|s)\)" +) +_ELAPSED = re.compile( + r"^(?:(?:(?P\d+)-)?(?P\d+):)?(?P\d+):(?P\d+)$" +) + + +@dataclass(frozen=True) +class Process: + """One row of the process table.""" + + pid: int + parent: int + elapsed: int + arguments: str + + +def parse_elapsed(text: str) -> int: + """Convert ``ps`` elapsed time (``[[dd-]hh:]mm:ss``) to seconds.""" + match = _ELAPSED.match(text.strip()) + if match is None: + raise ValueError(f"unrecognized elapsed time: {text!r}") + parts = {key: int(value or 0) for key, value in match.groupdict().items()} + return ( + parts["days"] * 86400 + + parts["hours"] * 3600 + + parts["minutes"] * 60 + + parts["seconds"] + ) + + +def parse_process_table(output: str) -> list[Process]: + """Parse ``ps -A -o pid=,ppid=,etime=,args=`` output.""" + processes = [] + for line in output.splitlines(): + fields = line.split(None, 3) + if len(fields) < 3: + continue + try: + processes.append( + Process( + pid=int(fields[0]), + parent=int(fields[1]), + elapsed=parse_elapsed(fields[2]), + arguments=fields[3] if len(fields) > 3 else "", + ) + ) + except ValueError: + continue + return processes + + +def read_process_table() -> list[Process]: + """Read the current process table portably (Linux and macOS).""" + output = subprocess.run( + ["ps", "-A", "-o", "pid=,ppid=,etime=,args="], + capture_output=True, + text=True, + check=False, + ).stdout + return parse_process_table(output) + + +def is_lean_process(process: Process) -> bool: + """Whether a process is a Lean compiler run (not Lake or a shell).""" + if not process.arguments: + return False + return Path(process.arguments.split()[0]).name == "lean" + + +def source_of(process: Process) -> str: + """The ``.lean`` file a Lean process is compiling, or its command line.""" + for argument in process.arguments.split(): + if argument.endswith(".lean"): + return argument + return process.arguments + + +def overdue_lean_processes( + processes: list[Process], root: int, limit: int +) -> list[Process]: + """Lean processes descended from ``root`` that have run longer than ``limit``.""" + children: dict[int, list[Process]] = {} + for process in processes: + children.setdefault(process.parent, []).append(process) + overdue = [] + pending = [root] + seen = {root} + while pending: + for child in children.get(pending.pop(), []): + if child.pid in seen: + continue + seen.add(child.pid) + pending.append(child.pid) + if is_lean_process(child) and child.elapsed > limit: + overdue.append(child) + return overdue + + +def _signal(pid: int, number: int) -> None: + try: + os.kill(pid, number) + except ProcessLookupError: + pass + + +def _stop(process: Process, limit: int) -> None: + source = source_of(process) + print( + f"::error file={source}::{source} was still compiling after {limit // 60} " + f"minutes and was stopped. Lean Pool's hard limit for one file is " + f"{limit // 60} minutes; split the file or make its proofs cheaper.", + flush=True, + ) + _signal(process.pid, signal.SIGTERM) + + +def watch(command: list[str], limit: int, poll: float = POLL_SECONDS) -> int: + """Run ``command``, stopping any Lean process that exceeds ``limit`` seconds.""" + child = subprocess.Popen(command) + stopped: dict[int, float] = {} + while child.poll() is None: + now = time.monotonic() + for process in overdue_lean_processes(read_process_table(), child.pid, limit): + if process.pid not in stopped: + _stop(process, limit) + stopped[process.pid] = now + elif now - stopped[process.pid] > TERMINATE_GRACE_SECONDS: + _signal(process.pid, signal.SIGKILL) + try: + child.wait(timeout=poll) + except subprocess.TimeoutExpired: + pass + if stopped: + return 124 + return child.returncode + + +def module_times(log: str) -> dict[str, float]: + """Build seconds per pool module from Lake's ``Built (