diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index d34c4517e0..1e0b1b5dd0 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -32,20 +32,29 @@ After the build, it reads Lake's per-module times from the log and fails when a 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. -After all cache and artifact restores, `prepare` removes the compiled outputs -of the added or modified modules that job is responsible for timing. This happens -even for a cache produced under the same policy: an untouched file in that cache -need not have passed the changed-file limit. Each changed module must emit a -fresh successful build timing in its responsible job; missing timings and cache -replays fail that check. +`check` records each changed module's time in a receipt next to its compiled +output (`.timing.json`), bound to a hash of that output's `.olean` files. +After all cache and artifact restores, `prepare` removes the compiled outputs of +every added or modified module the job is responsible for whose output has no +matching receipt. So output that was compiled without being timed is always +rebuilt, even from a cache produced under the same policy: an untouched file in +that cache need not have passed the changed-file limit. Each changed module must +then have either a fresh successful build timing from its responsible job or the +recorded time of the exact output being reused; that time is checked against the +limit either way, and a module with neither fails the check. Shards check their assigned modules. Assembly excludes projects listed in the same run's shard matrix and checks all remaining changed modules; the canonical gate requires every shard and assembly to succeed. Single and rebased root builds check all changed modules. Untouched modules can still reuse compiled output. +"Changed" is measured from the main commit the run is tested against: the tested +merge commit's first parent for a PR, not the event's `base.sha`, which can trail +main and would count projects merged since as the PR's own. + +A later push to a PR restores the outputs of modules whose own source is unchanged +from that PR's newest successful run; Lake's traces decide which are still valid. Reused PR, rebase and queue artifacts must still match `build_time_limits.py`. -That match does not replace the fresh timing required for a changed module. 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. diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 798622b5f0..7096aa7d75 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -97,6 +97,7 @@ jobs: reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} previous_head: ${{ steps.plan.outputs.previous_head }} queue_build: ${{ steps.plan.outputs.queue_build }} + diff_base: ${{ steps.plan.outputs.diff_base }} steps: - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -162,14 +163,24 @@ jobs: # exceeds the kernel's 128 KiB limit on a single environment string. changed_files="$RUNNER_TEMP/changed-files.txt" : > "$changed_files" + # The revision this run's own changes are measured from, for the plan + # and for every job's build-time gate. + diff_base="$BASE_SHA" case "$EVENT_NAME" in merge_group) git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files" ;; pull_request) - git diff --name-only --no-renames "$BASE_SHA"...HEAD > "$changed_files" + # The event's base.sha can trail main by days, which would count + # everything main merged since as this PR's change. The tested + # merge commit's first parent is the main tip it merges into. + if [ "$(git rev-parse -q --verify 'HEAD^2' || true)" = "$PR_HEAD" ]; then + diff_base=$(git rev-parse 'HEAD^1') + fi + git diff --name-only --no-renames "$diff_base"...HEAD > "$changed_files" ;; push) + diff_base="$BEFORE_SHA" if [ -n "$BEFORE_SHA" ] \ && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \ && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then @@ -182,6 +193,7 @@ jobs: diff_available=false ;; esac + echo "diff_base=$diff_base" >> "$GITHUB_OUTPUT" minimal_build=false if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then minimal_build=true @@ -382,12 +394,13 @@ 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 }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -615,10 +628,30 @@ jobs: echo "Mathlib already present from cache" fi + - name: Install uv + uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Reuse compiled files from this PR's successful runs + if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true' + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ github.event.pull_request.number }} + PR_BRANCH: ${{ github.head_ref }} + PR_HEAD: ${{ github.event.pull_request.head.sha }} + PR_BASE: ${{ github.event.pull_request.base.sha }} + CURRENT_RUN: ${{ github.run_id }} + run: >- + PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build + --number "$PR_NUMBER" --branch "$PR_BRANCH" + --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN" + - 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 }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail touch "$RUNNER_TEMP/build-stamp" @@ -631,9 +664,10 @@ jobs: | tr '\n' ' ') modules="$modules $project_modules" done - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -683,6 +717,44 @@ jobs: if-no-files-found: ignore retention-days: 1 + # Lint and audit this shard's projects here, in parallel with the other + # shards, instead of one after another in `finalize`. Only passes are + # handed on: `finalize` recomputes every fingerprint and runs whatever + # has no matching pass, so a failure here is reported there. + - 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 + continue-on-error: true + run: cd python && uv sync --locked + + - name: Lint and audit this shard's projects + id: shard-validation + continue-on-error: true + env: + PROJECTS: ${{ matrix.projects }} + run: | + cd python + # shellcheck disable=SC2086 # word-split the project list on purpose + uv run python -m lean_pool.shard_validation --repo .. --units $PROJECTS + + - name: Upload validation passes + if: always() && steps.shard-validation.outcome != 'skipped' + continue-on-error: true + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: ci-validation-${{ matrix.shard }} + path: .lake/validation-cache/v1/passes.json + include-hidden-files: true + if-no-files-found: ignore + compression-level: 1 + retention-days: 1 + finalize: needs: [plan, shard] # Run even when a shard failed: merging what succeeded and building the @@ -817,15 +889,16 @@ 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 }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} # This run's shards already compiled and timed these projects' # changed files, so assembly neither rebuilds nor re-times them. SHARD_PROJECTS: ${{ join(fromJSON(needs.plan.outputs.matrix).include.*.projects, ' ') }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then @@ -911,6 +984,21 @@ jobs: PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build --base "$BASE_SHA" --head "$HEAD_SHA" --receipts + - name: Download shard validation passes + continue-on-error: true + uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 + with: + pattern: ci-validation-* + path: ${{ runner.temp }}/shard-validation + + - name: Merge shard validation passes + continue-on-error: true + env: + FRAGMENTS: ${{ runner.temp }}/shard-validation + run: >- + PYTHONPATH=python python3 -m lean_pool.validation_cache merge + "$FRAGMENTS" + - name: Lint run: | cd python @@ -1092,12 +1180,13 @@ jobs: - name: Build combined Lean root env: - BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }} + BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }} run: | set -euo pipefail - # Always rebuild this job's changed files after every cache/artifact - # restore. A same-policy cache need not have timed them while changed. - # `check` requires fresh timings; `watch` retains the 60-minute limit. + # After every cache/artifact restore, `prepare` forces a rebuild of + # each changed file whose restored output has no recorded build time, + # so `check` judges a time measured in CI for every changed file. + # `watch` retains the 60-minute limit. time_base="" if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \ && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then diff --git a/python/ci-performance.md b/python/ci-performance.md index 2d0b8455af..35aeb818e1 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -37,6 +37,45 @@ checkout, never the artifact paths. So every CI build step is followed by artifact lists, and preserves modification times, so shard packaging still ships only fresh files. +### Incremental PR pushes + +Until November 2026 every run recompiled every file a PR changed relative to +main, to time it against the 600 s limit. A PR that adds a 1,300-file project +therefore recompiled all of it (about 38 minutes on a 4-vCPU runner) on each +push, in the merge queue, and again on main, even when a push edited a handful +of files. + +Now `build_time_limits check` writes a `.timing.json` receipt beside each +changed module's output, bound to a hash of its `.olean` files, and `prepare` +only invalidates changed modules without a matching receipt. Receipts travel +with every artifact that carries the outputs themselves. `ci_pr_build` restores +the unchanged-source modules of the PR's newest successful run, so a later push +compiles only what it edited and whatever Lake's traces say depends on it. + +The plan and the build-time gate also measure a PR's changes from the tested +merge commit's first parent. The event's `base.sha` can trail main by days, +which made every project merged since look changed and be rebuilt. + +### Validation in shards + +Lint and the quality audits reuse per-project pass receipts, so an ordinary PR +validates only the project it touches. A change to any checker input (the +workflow, `validation_cache.py`, `quality.py`, the no-lint lists, the pins) +invalidates every receipt. One job then linted the pool for about 36 minutes and +audited it for about 68, one project at a time. + +In-job concurrency does not fix that: PR #785 measured that a single lint +process already saturates a 4-vCPU runner. Instead the planner now shards the +whole pool when checker inputs change, even with a warm build cache, and every +shard job lints and audits the projects it built +(`python -m lean_pool.shard_validation --units ...`). Shards upload only their pass receipts. +`finalize` merges them (`validation_cache merge`) and then runs the unchanged +Lint and quality steps, which recompute every fingerprint, reuse matching passes, +and run anything a shard did not pass. A shard's validation step can therefore +neither fail nor pass the run by itself. + +`MAX_SHARDS` is 14: beyond that the costliest project fills a shard alone. + Documentation retains its separate, integrity-checked SQLite checkpoints. They still depend on available cache capacity; this change reduces duplicate data instead of changing the repository's paid storage limit. diff --git a/python/lean_pool/build_time_limits.py b/python/lean_pool/build_time_limits.py index 43be062b24..661d86a60b 100644 --- a/python/lean_pool/build_time_limits.py +++ b/python/lean_pool/build_time_limits.py @@ -8,13 +8,21 @@ 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. +times Lake reports for each module on the CI runner. + +``check`` records each changed module's time in a receipt beside its compiled +output, bound to the hash of that output. ``prepare`` forces a rebuild of every +changed module whose output carries no matching receipt, so a file compiled +without being timed can never pass; a later run that restores the same output +reuses the recorded time instead of compiling the file again. Standard library +only, so CI can run it with the runner's ``python3`` before ``uv`` is installed. """ from __future__ import annotations import argparse +import hashlib +import json import logging import os import re @@ -32,6 +40,10 @@ FILE_LIMIT_SECONDS = 600 POLL_SECONDS = 15 TERMINATE_GRACE_SECONDS = 30 +RECEIPT_VERSION = 1 +RECEIPT_SUFFIX = ".timing.json" +# Every compiled output Lean loads for a module; a rebuild rewrites them all. +TIMED_OUTPUT_SUFFIXES = (".olean", ".olean.private", ".olean.server") _BUILT_LINE = re.compile( r"Built (?PLeanPool(?:\.[^\s:()]+)+) " r"\((?P\d+(?:\.\d+)?)(?Pms|s)\)" @@ -507,34 +519,116 @@ def _selected_changed_modules( } +def _output_stem(root: Path, path: str) -> Path: + """``LeanPool/A/B.lean`` -> ``/.lake/build/lib/lean/LeanPool/A/B``.""" + return root / ".lake/build/lib/lean" / Path(path).with_suffix("") + + +def output_digest(root: Path, path: str) -> str | None: + """Hash a module's compiled outputs; ``None`` when it has not been compiled.""" + stem = _output_stem(root, path) + digest = hashlib.sha256() + for suffix in TIMED_OUTPUT_SUFFIXES: + output = stem.with_name(stem.name + suffix) + try: + content = output.read_bytes() + except OSError: + if suffix == ".olean": + return None + continue + digest.update(f"{suffix}:{len(content)}:".encode()) + digest.update(content) + return digest.hexdigest() + + +def recorded_seconds(root: Path, path: str) -> float | None: + """The build time recorded for the module's current outputs, if any.""" + stem = _output_stem(root, path) + try: + receipt = json.loads(stem.with_name(stem.name + RECEIPT_SUFFIX).read_text()) + seconds = receipt["seconds"] + valid = ( + receipt["version"] == RECEIPT_VERSION + and isinstance(seconds, int | float) + and not isinstance(seconds, bool) + and seconds >= 0 + and receipt["outputs"] == output_digest(root, path) + ) + except (OSError, ValueError, KeyError, TypeError): + return None + return float(seconds) if valid else None + + +def record_seconds(root: Path, path: str, seconds: float) -> None: + """Bind a freshly measured build time to the outputs that build produced.""" + digest = output_digest(root, path) + if digest is None: + return + stem = _output_stem(root, path) + receipt = {"version": RECEIPT_VERSION, "seconds": seconds, "outputs": digest} + temporary = stem.with_name(stem.name + RECEIPT_SUFFIX + ".tmp") + temporary.write_text(json.dumps(receipt, sort_keys=True) + "\n") + temporary.replace(stem.with_name(stem.name + RECEIPT_SUFFIX)) + + +def _invalidate(root: Path, path: str) -> int: + """Remove every artifact of one module, including its timing receipt.""" + stem = Path(path).with_suffix("") + removed = 0 + for directory in ("lib/lean", "ir"): + target = root / ".lake/build" / directory / stem + if not target.parent.is_dir(): + continue + for artifact in target.parent.iterdir(): + if artifact.name.startswith(target.name + ".") and ( + artifact.is_file() or artifact.is_symlink() + ): + artifact.unlink() + removed += 1 + return removed + + def prepare( base: str, root: Path, modules: list[str] | None = None, exclude_projects: list[str] | None = None, ) -> int: - """Invalidate changed-module artifacts so their build must record new timings.""" + """Invalidate changed modules whose compiled outputs have no recorded time.""" changed = _selected_changed_modules(base, root, modules, exclude_projects) - removed = 0 - for path in changed.values(): - stem = Path(path).with_suffix("") - for directory in ("lib/lean", "ir"): - target = root / ".lake/build" / directory / stem - if not target.parent.is_dir(): - continue - for artifact in target.parent.iterdir(): - if artifact.name.startswith(target.name + ".") and ( - artifact.is_file() or artifact.is_symlink() - ): - artifact.unlink() - removed += 1 + untimed = [ + path for path in changed.values() if recorded_seconds(root, path) is None + ] + removed = sum(_invalidate(root, path) for path in untimed) print( - f"Fresh build timings: invalidated {removed} artifacts for " - f"{len(changed)} added or modified pool files." + f"Build timings: {len(changed)} added or modified pool files, " + f"{len(changed) - len(untimed)} with a recorded time for their compiled " + f"output; invalidated {removed} artifacts of the other {len(untimed)}." ) return 0 +def changed_times( + times: dict[str, float], changed: dict[str, str], root: Path +) -> tuple[dict[str, float], int]: + """Each changed module's time: measured in this job, else recorded earlier. + + Returns the times and how many came from this job's build. + """ + result = {} + fresh = 0 + for module, path in changed.items(): + if module in times: + record_seconds(root, path, times[module]) + result[module] = times[module] + fresh += 1 + continue + seconds = recorded_seconds(root, path) + if seconds is not None: + result[module] = seconds + return result, fresh + + def check( log_path: Path, base: str, @@ -545,21 +639,23 @@ def check( exclude_projects: list[str] | None = None, ) -> int: """Report changed files over the per-file limit; return the exit status.""" - times = module_times(log_path.read_text(errors="replace")) + built = module_times(log_path.read_text(errors="replace")) changed = _selected_changed_modules(base, root, modules, exclude_projects) - built = [module for module in changed if module in times] + times, fresh = changed_times(built, changed, root) print( f"Per-file build-time limit {limit} s: {len(changed)} added or modified " - f"pool files, {len(built)} compiled in this job." + f"pool files, {fresh} compiled in this job, {len(times) - fresh} with a " + "time recorded when their current output was compiled." ) - for module in sorted(built, key=lambda name: -times[name])[:10]: + for module in sorted(times, key=lambda name: -times[name])[:10]: print(f" {times[module]:8.1f} s {changed[module]}") found = violations(times, changed, limit) missing = sorted(set(changed) - times.keys()) for module in missing: print( - f"::error file={changed[module]}::No fresh successful build timing for " - f"{changed[module]}; added or modified files must compile in this job." + f"::error file={changed[module]}::No successful build timing for " + f"{changed[module]}; added or modified files must be compiled and " + "timed in CI." ) for violation in found: print( @@ -579,7 +675,7 @@ def main(arguments: list[str] | None = None) -> int: watch_parser.add_argument("--limit", type=int, default=PROCESS_LIMIT_SECONDS) watch_parser.add_argument("build", nargs=argparse.REMAINDER) prepare_parser = commands.add_parser( - "prepare", help="force changed files to rebuild" + "prepare", help="force untimed changed files to rebuild" ) prepare_parser.add_argument("--base", required=True) prepare_parser.add_argument("--root", type=Path, default=Path.cwd()) diff --git a/python/lean_pool/ci_pr_build.py b/python/lean_pool/ci_pr_build.py index c6894ebf80..27703822f4 100644 --- a/python/lean_pool/ci_pr_build.py +++ b/python/lean_pool/ci_pr_build.py @@ -88,6 +88,18 @@ def sources_match(root: Path, previous: str, base: str) -> bool: ) +def inputs_match(root: Path, previous: str) -> bool: + """Avoid downloading artifacts compiled under other pinned build inputs.""" + return ( + subprocess.run( + ["git", "diff", "--quiet", previous, "--", *rebase_fastpath.PINNED_INPUTS], + cwd=root, + check=False, + ).returncode + == 0 + ) + + def restore_prior_build( root: Path, repository: str, @@ -97,7 +109,12 @@ def restore_prior_build( base: str, current_run: int = 0, ) -> bool: - """Restore matching compiled files; Lake and every normal check still run.""" + """Restore the newest earlier build of this PR; Lake and every check still run. + + The PR's sources may have changed since that build. Only modules whose own + source is unchanged are restored; Lake recompiles the rest and any restored + module whose imports changed, and the build-time gate times what it compiles. + """ if not all(rebase_fastpath.SHA.fullmatch(value) for value in (head, base)): raise ValueError("invalid PR revisions") candidates = ( @@ -114,17 +131,19 @@ def restore_prior_build( except RECOVERY_ERRORS: LOGGER.info("Merged project reuse unavailable; checking the PR's build") for run in chain(() if history is None else (history,), candidates): - if not sources_match(root, run["head_sha"], base): + if not inputs_match(root, run["head_sha"]): continue try: - rebase_fastpath.restore(root, repository, run["id"], run["head_sha"]) - LOGGER.info("Restored matching PR build from run %s", run["id"]) + rebase_fastpath.restore( + root, repository, run["id"], run["head_sha"], changed_sources=True + ) + LOGGER.info("Restored unchanged modules from PR run %s", run["id"]) return True except RECOVERY_ERRORS: LOGGER.info( "PR build %s unavailable or changed; trying older run", run["id"] ) - LOGGER.info("No matching PR build; Lake will compile the current sources") + LOGGER.info("No earlier PR build; Lake will compile the current sources") return False diff --git a/python/lean_pool/rebase_fastpath.py b/python/lean_pool/rebase_fastpath.py index 7a20f0e383..352ab28d1c 100644 --- a/python/lean_pool/rebase_fastpath.py +++ b/python/lean_pool/rebase_fastpath.py @@ -348,8 +348,46 @@ def _restore_build_files( os.replace(staging / entry.name, destination) -def restore(root: Path, repository: str, run_id: int, previous_head: str) -> None: - """Download a prior green run's project artifacts and validate before overlay.""" +def _member_source(relative: PurePosixPath) -> str: + """The Lean source whose compilation produced a packed build file.""" + skip = 3 if relative.parts[2] == "ir" else 4 + return "/".join((*relative.parts[skip:-1], relative.name.split(".")[0] + ".lean")) + + +def _unchanged_members( + root: Path, members: list[tarfile.TarInfo], sources: dict[str, str] +) -> list[tarfile.TarInfo]: + """Keep the outputs of modules whose own source is the one that was compiled.""" + current = {} + kept = [] + for entry in members: + source = _member_source(PurePosixPath(entry.name)) + if source not in current: + path = root / source + current[source] = ( + hashlib.sha256(path.read_bytes()).hexdigest() + if path.is_file() + else None + ) + if current[source] is not None and sources.get(source) == current[source]: + kept.append(entry) + return kept + + +def restore( + root: Path, + repository: str, + run_id: int, + previous_head: str, + *, + changed_sources: bool = False, +) -> None: + """Download a prior green run's project artifacts and validate before overlay. + + With ``changed_sources``, project sources may differ from the packed build: + only modules whose own source is unchanged are restored, and Lake's traces + still decide which of those are reusable after their imports changed. + """ endpoint = f"repos/{repository}/actions/runs/{run_id}/artifacts?per_page=100" artifacts = [ artifact @@ -390,10 +428,12 @@ def restore(root: Path, repository: str, run_id: int, previous_head: str) -> Non for project in projects ): raise ValueError("invalid project build manifest") + sources = manifest.get("sources") if ( manifest.get("version") != 1 or manifest.get("head") != previous_head - or manifest.get("sources") != _source_hashes(root, projects) + or not isinstance(sources, dict) + or (not changed_sources and sources != _source_hashes(root, projects)) or manifest.get("inputs") != { name: hashlib.sha256((root / name).read_bytes()).hexdigest() @@ -412,6 +452,8 @@ def restore(root: Path, repository: str, run_id: int, previous_head: str) -> Non or not _build_file_for_project(relative, set(projects)) ): raise ValueError(f"unexpected project artifact: {entry.name}") + if changed_sources: + members = _unchanged_members(root, members, sources) _restore_build_files(root, archive, members) diff --git a/python/lean_pool/shard_validation.py b/python/lean_pool/shard_validation.py new file mode 100644 index 0000000000..645c63a97f --- /dev/null +++ b/python/lean_pool/shard_validation.py @@ -0,0 +1,49 @@ +"""Lint and audit one build shard's projects, keeping every pass they earn. + +A shard job runs this for the projects it built, in parallel with the other +shards, and uploads the resulting pass receipts. It runs the per-project checks +of the whole-pool run through the same functions. Repository-wide invariants, +and the decision itself, stay with the assembling job: it merges the receipts +(``validation_cache merge``), recomputes every fingerprint, and runs whatever +has no matching pass. +""" + +from __future__ import annotations + +import argparse +import logging +from pathlib import Path + +from lean_pool.quality import _cached_pool_audits, _check_projects +from lean_pool.validation_cache import ValidationCache, lint_pool + +LOGGER = logging.getLogger(__name__) + + +def validate_shard(root: Path, cache: ValidationCache) -> bool: + """Lint and audit only the cache's units; save their passes either way.""" + failed = lint_pool(root, cache, keep_going=True) + for unit in failed: + print(f"lint failed: {unit}") + errors = _check_projects(root, cache) + _cached_pool_audits(root, cache) + for error in errors: + print(error.format(root)) + cache.save() + return not (failed or errors) + + +def main(arguments: list[str] | None = None) -> int: + """Validate the named units and report whether all of them passed.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=Path.cwd()) + parser.add_argument("--cache", type=Path, default=Path(".lake/validation-cache/v1")) + parser.add_argument("--units", nargs="*", default=[]) + options = parser.parse_args(arguments) + logging.basicConfig(level=logging.INFO, format="validation: %(message)s") + root = options.repo.resolve() + cache = ValidationCache(root, root / options.cache, units=frozenset(options.units)) + return 0 if validate_shard(root, cache) else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py index 4c6dfb9c7d..47a17acc12 100644 --- a/python/lean_pool/validation_cache.py +++ b/python/lean_pool/validation_cache.py @@ -3,6 +3,11 @@ CI restores receipts from main or earlier runs of the same PR. Every receipt covers module inventories, transitive local imports, dependency pins, and code. Static repository invariants and text style lint still run on every checkout. + +Build shards can validate their own projects in parallel +(``lean_pool.shard_validation``) and hand their pass receipts to the assembling +job (``merge``). That job still recomputes every fingerprint and runs whatever a +shard did not pass, so it alone decides. """ from __future__ import annotations @@ -24,6 +29,7 @@ "lakefile.lean", "scripts/ci/LeanPoolLinters.lean", "python/lean_pool/validation_cache.py", + "python/lean_pool/shard_validation.py", "python/pyproject.toml", "python/uv.lock", ".github/workflows/lean_action_ci.yml", @@ -47,6 +53,12 @@ def checker_inputs(kind: str | None) -> tuple[str, ...]: return GLOBAL_INPUTS +def unit_name(module: str) -> str: + """The pool unit that owns a module; the root index is its own unit.""" + parts = module.split(".") + return parts[1] if len(parts) > 1 else "__root__" + + def pool_units(root: Path) -> list[list[str]]: """Partition every pool source, including the root and unregistered modules.""" units: dict[str, list[str]] = {} @@ -115,14 +127,44 @@ def source_inventory( return paths +def read_receipts(path: Path) -> dict[str, dict[str, Any]]: + """Read a receipts file; a missing or corrupt one holds no receipts.""" + try: + data = json.loads(path.read_text()) + if data["version"] == 1 and isinstance(data["receipts"], dict): + return data["receipts"] + except (OSError, ValueError, KeyError, TypeError): + pass + return {} + + +def write_receipts(directory: Path, receipts: dict[str, dict[str, Any]]) -> None: + """Publish a receipts file atomically.""" + directory.mkdir(parents=True, exist_ok=True) + temporary = directory / "passes.tmp" + temporary.write_text(json.dumps({"version": 1, "receipts": receipts}) + "\n") + temporary.replace(directory / "passes.json") + + class ValidationCache: """Store pass receipts only, with content fingerprints and atomic publication.""" - def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> None: - """Load optional receipts; a missing or corrupt cache is a cold run.""" + def __init__( + self, + root: Path, + directory: Path, + *, + refresh: bool = False, + units: frozenset[str] | None = None, + ) -> None: + """Load optional receipts; a missing or corrupt cache is a cold run. + + With ``units``, checks of every other unit are skipped without a receipt. + """ self.root = root self.directory = directory self.refresh = refresh + self.units = units self.digests: dict[Path, str] = {} # Compilation finishes before validation; reuse inventories and path # lookups only within this immutable checkout, never across CI runs. @@ -135,12 +177,7 @@ def __init__(self, root: Path, directory: Path, *, refresh: bool = False) -> Non self.used: dict[str, dict[str, Any]] = {} self.hits = 0 self.misses = 0 - try: - data = json.loads((directory / "passes.json").read_text()) - if data["version"] == 1 and isinstance(data["receipts"], dict): - self.receipts = data["receipts"] - except (OSError, ValueError, KeyError, TypeError): - pass + self.receipts = read_receipts(directory / "passes.json") def fingerprint( self, modules: list[str], metadata: Any = None, *, kind: str | None = None @@ -188,6 +225,8 @@ def check[T]( metadata: Any = None, ) -> list[T]: """Run on a miss and retain only passes; failures never create receipts.""" + if self.units is not None and unit_name(modules[0]) not in self.units: + return [] digest = self.fingerprint(modules, metadata, kind=kind) key = f"{kind}:{modules[0]}" expected = {"fingerprint": digest, "modules": modules, "passed": True} @@ -205,21 +244,24 @@ def check[T]( def save(self) -> None: """Publish only receipts used in this run, pruning deleted/changed projects.""" - self.directory.mkdir(parents=True, exist_ok=True) - temporary = self.directory / "passes.tmp" - temporary.write_text(json.dumps({"version": 1, "receipts": self.used}) + "\n") - temporary.replace(self.directory / "passes.json") + write_receipts(self.directory, self.used) LOGGER.info( "Validation: %d cached checks, %d fresh checks", self.hits, self.misses ) -def lint_pool(root: Path, cache: ValidationCache) -> None: - """Lint owned declarations once per unit, importing every owned module.""" +def lint_pool( + root: Path, cache: ValidationCache, *, keep_going: bool = False +) -> list[str]: + """Lint owned declarations once per unit, importing every owned module. + + A failing unit raises, unless ``keep_going`` asks for its name instead. + """ + failed = [] for modules in pool_units(root): def validate() -> list[str]: - subprocess.run( + process = subprocess.run( [ "lake", "env", @@ -229,23 +271,55 @@ def validate() -> list[str]: *modules, ], cwd=root, - check=True, + check=not keep_going, ) - return [] + return [modules[0]] if process.returncode else [] + + failed.extend(cache.check("lint", modules, validate)) + return failed - cache.check("lint", modules, validate) + +def merge_receipts(directory: Path, fragments: list[Path]) -> int: + """Add shards' pass receipts to the cache; return how many were added. + + Each fragment is a receipts file or a directory of downloaded ones. + + A receipt only counts where the assembling job computes the same + fingerprint for the same modules, so merging cannot certify other inputs. + """ + receipts = read_receipts(directory / "passes.json") + added = 0 + files = [ + file + for fragment in fragments + for file in ( + sorted(fragment.rglob("passes.json")) if fragment.is_dir() else [fragment] + ) + ] + for fragment in files: + for key, receipt in read_receipts(fragment).items(): + if isinstance(receipt, dict) and receipts.get(key) != receipt: + receipts[key] = receipt + added += 1 + write_receipts(directory, receipts) + return added def main() -> int: """Run the cached declaration linter or repository quality checker.""" parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("check", choices=("lint", "quality")) + parser.add_argument("check", choices=("lint", "quality", "merge")) parser.add_argument("--repo", type=Path, default=Path.cwd()) parser.add_argument("--cache", type=Path, default=Path(".lake/validation-cache/v1")) parser.add_argument("--refresh", action="store_true") + parser.add_argument("fragments", nargs="*", type=Path) arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="validation: %(message)s") root = arguments.repo.resolve() + if arguments.check == "merge": + added = merge_receipts(root / arguments.cache, arguments.fragments) + LOGGER.info("Merged %d shard receipts", added) + return 0 cache = ValidationCache(root, root / arguments.cache, refresh=arguments.refresh) if arguments.check == "lint": lint_pool(root, cache) diff --git a/python/tests/test_build_shard_planner.py b/python/tests/test_build_shard_planner.py index 3d4e26d0d3..d770d166ec 100644 --- a/python/tests/test_build_shard_planner.py +++ b/python/tests/test_build_shard_planner.py @@ -8,6 +8,8 @@ import pytest +from lean_pool.validation_cache import GLOBAL_INPUTS + ROOT = Path(__file__).resolve().parents[2] PLANNER = runpy.run_path(str(ROOT / "scripts/ci/plan-build-shards.py")) MEASURER = runpy.run_path(str(ROOT / "scripts/ci/measure-build-costs.py")) @@ -177,6 +179,31 @@ def test_cold_plan_covers_pool_in_balanced_shards( assert max(loads) <= 1.25 * sum(loads) / len(loads) +def test_checker_input_change_fans_validation_out_over_the_pool( + monkeypatch: pytest.MonkeyPatch, + capsys: pytest.CaptureFixture[str], + tmp_path: Path, +) -> None: + """Every project must be validated again, so each shard takes its share.""" + listing = str(tmp_path / "changed.txt") + for changed in (".github/workflows/lean_action_ci.yml", "scripts/nolints.json"): + plan = _plan(monkeypatch, capsys, [changed], CHANGED_FILES_PATH=listing) + shards = plan["matrix"]["include"] + assert plan["mode"] == "sharded" + assert "lint or quality checker inputs changed" in plan["reason"] + projects = [name for shard in shards for name in shard["projects"].split()] + assert sorted(projects) == sorted(PLANNER["unit_sources"]()) + plan = _plan( + monkeypatch, capsys, ["python/lean_pool/stats.py"], CHANGED_FILES_PATH=listing + ) + assert plan["mode"] == "single" + + +def test_validation_inputs_match_the_receipt_fingerprints() -> None: + """The planner reads the checker inputs from the validation cache itself.""" + assert PLANNER["validation_inputs"]() == set(GLOBAL_INPUTS) + + def test_dirty_projects_are_sharded_by_cost_only_when_large( monkeypatch: pytest.MonkeyPatch, capsys: pytest.CaptureFixture[str], diff --git a/python/tests/test_build_time_limits.py b/python/tests/test_build_time_limits.py index 227c492a87..8f27d3caf7 100644 --- a/python/tests/test_build_time_limits.py +++ b/python/tests/test_build_time_limits.py @@ -95,7 +95,7 @@ def test_violations_cover_changed_files_only( # At900s no observed module is too slow; Cached still lacks a fresh timing. assert limits.check(log, "base", tmp_path, limit=900) == 1 output = capsys.readouterr().out - assert "No fresh successful build timing for LeanPool/Quick/Cached.lean" in output + assert "No successful build timing for LeanPool/Quick/Cached.lean" in output def _git(root: Path, *arguments: str) -> str: @@ -254,9 +254,6 @@ def test_prepare_rebuilds_even_with_a_matching_legacy_policy_marker( """A global marker cannot certify a changed file on a later source reversion.""" root, base = _repository(tmp_path) changed = _outputs(root, BUNDLE_MODULE) - log = tmp_path / "build.log" - log.write_text(f"✔ [1/1] Built {BUNDLE_MODULE} (300s)\n") - assert limits.check(log, base, root, limit=600) == 0 marker = root / ".lake/build/lean-pool-build-time-policy" marker.write_text(hashlib.sha256(Path(limits.__file__).read_bytes()).hexdigest()) assert limits.prepare(base, root) == 0 @@ -576,7 +573,7 @@ def test_check_rejects_missing_or_replayed_changed_file_timing( log = tmp_path / "build.log" log.write_text(log_text) assert limits.check(log, base, root, 600) == 1 - assert "No fresh successful build timing" in capsys.readouterr().out + assert "No successful build timing" in capsys.readouterr().out def test_same_policy_source_revert_rebuilds_and_checks_slow_file(tmp_path: Path): @@ -603,6 +600,115 @@ def test_same_policy_source_revert_rebuilds_and_checks_slow_file(tmp_path: Path) assert limits.check(log, base, root, 600) == 0 +def _timed(root: Path, base: str, tmp_path: Path, seconds: int = 300) -> Path: + """Compile outputs for the changed bundle and record their build time.""" + artifact = _artifact(root, BUNDLE_MODULE, ".olean") + log = tmp_path / "timed.log" + log.write_text(f"Built {BUNDLE_MODULE} ({seconds}s)\n") + assert limits.check(log, base, root, 900) == 0 + return artifact + + +def test_recorded_time_spares_the_rebuild_of_unchanged_output(tmp_path: Path, capsys): + """Output timed by an earlier run is kept and passes without a fresh build.""" + root, base = _repository(tmp_path) + artifact = _timed(root, base, tmp_path) + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + assert limits.prepare(base, root) == 0 + assert artifact.exists() + log = tmp_path / "build.log" + log.write_text(f"Replayed {BUNDLE_MODULE}\n") + capsys.readouterr() + assert limits.check(log, base, root, 600) == 0 + assert "0 compiled in this job, 1 with a time recorded" in capsys.readouterr().out + + +def test_recorded_time_over_the_limit_still_fails(tmp_path: Path, capsys): + """Reusing output never launders a slow file: its recorded time is checked.""" + root, base = _repository(tmp_path) + _timed(root, base, tmp_path, seconds=865) + log = tmp_path / "build.log" + log.write_text("") + assert limits.check(log, base, root, 600) == 1 + assert "took 865 s to build" in capsys.readouterr().out + + +@pytest.mark.parametrize("suffix", [".olean", ".olean.private", ".olean.server"]) +def test_recorded_time_does_not_cover_different_output(tmp_path: Path, suffix: str): + """A receipt certifies only the exact compiled files it was measured for.""" + root, base = _repository(tmp_path) + artifact = _timed(root, base, tmp_path) + _artifact(root, BUNDLE_MODULE, suffix).write_text("compiled by an untimed build\n") + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.prepare(base, root) == 0 + assert not artifact.exists() + stem = artifact.with_suffix("") + assert not stem.with_name(stem.name + limits.RECEIPT_SUFFIX).exists() + log = tmp_path / "build.log" + log.write_text("") + assert limits.check(log, base, root, 600) == 1 + + +@pytest.mark.parametrize( + "receipt", + [ + "{", + "[]", + '{"version": 0, "seconds": 1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": true, "outputs": "DIGEST"}', + '{"version": 1, "seconds": -1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": "1", "outputs": "DIGEST"}', + '{"version": 1, "outputs": "DIGEST"}', + '{"version": 1, "seconds": 1}', + ], +) +def test_malformed_receipts_certify_nothing(tmp_path: Path, receipt: str): + """Anything but a well-formed receipt for the current output forces a rebuild.""" + root, base = _repository(tmp_path) + artifact = _artifact(root, BUNDLE_MODULE, ".olean") + digest = limits.output_digest(root, BUNDLE) + stem = artifact.with_suffix("") + stem.with_name(stem.name + limits.RECEIPT_SUFFIX).write_text( + receipt.replace("DIGEST", digest) + ) + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.prepare(base, root) == 0 + assert not artifact.exists() + + +def test_fresh_build_replaces_the_recorded_time(tmp_path: Path): + """A module compiled in this job is judged by this job's measurement.""" + root, base = _repository(tmp_path) + _timed(root, base, tmp_path, seconds=865) + log = tmp_path / "build.log" + log.write_text(f"Built {BUNDLE_MODULE} (300s)\n") + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + + +def test_only_changed_modules_get_receipts(tmp_path: Path): + """Untouched files are outside the limit, so their builds record nothing.""" + root, base = _repository(tmp_path) + unchanged = "LeanPool/MovingSofa/Certificates/Bundle023.lean" + _artifact(root, BUNDLE_MODULE, ".olean") + _artifact(root, "LeanPool.MovingSofa.Certificates.Bundle023", ".olean") + log = tmp_path / "build.log" + log.write_text(LAKE_LOG.replace("(865s)", "(300s)")) + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) == 300.0 + assert limits.recorded_seconds(root, unchanged) is None + + +def test_missing_output_records_nothing(tmp_path: Path): + """A timing without compiled output cannot certify a later restore.""" + root, base = _repository(tmp_path) + log = tmp_path / "build.log" + log.write_text(f"Built {BUNDLE_MODULE} (300s)\n") + assert limits.check(log, base, root, 600) == 0 + assert limits.recorded_seconds(root, BUNDLE) is None + assert limits.output_digest(root, BUNDLE) is None + + def test_prepare_and_check_scope_other_shard_and_explicit_empty(tmp_path: Path): """A shard checks only changed modules it builds; an empty scope checks none.""" root, base = _repository(tmp_path) @@ -749,8 +855,13 @@ def test_workflow_rebuilds_changed_modules_after_all_compiled_restores() -> None "build_time_limits check" ) assert script.count('--base "$time_base"') == 2 + assert steps[index]["env"]["BUILD_TIME_BASE"] == ( + "${{ needs.plan.outputs.diff_base }}" + ) assert 'git cat-file -e "$BUILD_TIME_BASE"' in script assert 'time_base=""' in script + if name != "rebase": + assert any("-m lean_pool.ci_pr_build" in s.get("run", "") for s in steps) if name == "shard": assert ( 'git ls-files -- "LeanPool/$project.lean" "LeanPool/$project/"' diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 0d3b53fe70..e96c0e3dc7 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -106,6 +106,36 @@ def test_single_and_sharded_builds_use_validation_cache() -> None: assert contracts[0] == contracts[1] +def test_shards_validate_their_projects_and_assembly_decides() -> None: + """Shard validation only hands passes on; it can never fail or pass the run.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + steps = jobs["shard"]["steps"] + names = [step.get("name") for step in steps] + validate = steps[names.index("Lint and audit this shard's projects")] + assert "lean_pool.shard_validation --repo .. --units $PROJECTS" in validate["run"] + assert validate["continue-on-error"] is True + assert names.index("Upload build outputs") < names.index( + "Lint and audit this shard's projects" + ) + upload = steps[names.index("Upload validation passes")] + assert upload["with"]["name"] == "ci-validation-${{ matrix.shard }}" + assert upload["continue-on-error"] is True + assert not any( + step.get("uses", "").startswith("actions/cache/save@") for step in steps + ) + final = jobs["finalize"]["steps"] + final_names = [step.get("name") for step in final] + merge = final[final_names.index("Merge shard validation passes")] + assert "validation_cache merge" in merge["run"] + assert ( + final_names.index("Restore project validation") + < final_names.index("Download shard validation passes") + < final_names.index("Merge shard validation passes") + < final_names.index("Lint") + < final_names.index("Repository quality checks") + ) + + def test_merge_queue_reports_all_required_gates_without_path_filtered_workflows() -> ( None ): @@ -267,11 +297,16 @@ def test_minimal_verifier_pr_has_an_explicit_project_build_producer(tmp_path): def test_assembly_restores_projects_once_and_main_owns_full_cache(): - """Assembly recovers PR outputs once before fresh shard files are applied.""" + """Shards and assembly recover PR outputs before fresh shard files are applied.""" jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + shard = [step.get("name") for step in jobs["shard"]["steps"]] + # A shard compiles only what a later push edited, so it needs the PR's + # earlier outputs (and their recorded build times) before it builds. + assert shard.index( + "Reuse compiled files from this PR's successful runs" + ) < shard.index("Build this shard's projects") assert not any( - "lean_pool.ci_pr_build" in step.get("run", "") - or "lean_pool.queue_build" in step.get("run", "") + "lean_pool.queue_build" in step.get("run", "") for step in jobs["shard"]["steps"] ) steps = jobs["finalize"]["steps"] diff --git a/python/tests/test_ci_pr_build.py b/python/tests/test_ci_pr_build.py index a833cd4bfe..e0abe6c92f 100644 --- a/python/tests/test_ci_pr_build.py +++ b/python/tests/test_ci_pr_build.py @@ -13,7 +13,13 @@ import pytest -from lean_pool import ci_artifacts, ci_pr_build, rebase_fastpath, slim_setup +from lean_pool import ( + build_time_limits, + ci_artifacts, + ci_pr_build, + rebase_fastpath, + slim_setup, +) TOOLCHAIN = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() @@ -175,19 +181,54 @@ def test_metadata_edit_reuses_build_without_skipping_validation( assert not (root / ".lake/validation-cache").exists() +@pytest.mark.parametrize( + ("path", "reused"), + [("LeanPool/B.lean", False), ("LeanPool/B/Added.lean", True)], +) +def test_changed_sources_restore_only_unchanged_modules( + repository, monkeypatch, path, reused +): + """An edited module is left for Lake to compile; untouched ones are restored.""" + root, base, previous = repository + archive, compiled = _archive(root, base, previous) + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("module\n-- edited\n") + head = _commit(root, "edit source") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert compiled.exists() == reused + + +def test_deleted_module_output_is_not_restored(repository, monkeypatch): + """Compiled output of a module the PR has since removed stays out of the build.""" + root, base, previous = repository + (root / "LeanPool/B").mkdir() + (root / "LeanPool/B/Extra.lean").write_text("module\n") + previous = _commit(root, "add Extra") + extra = root / ".lake/build/lib/lean/LeanPool/B/Extra.olean" + extra.parent.mkdir(parents=True) + extra.write_text("prior compiled Extra") + archive, compiled = _archive(root, base, previous) + extra.unlink() + _git(root, "rm", "-q", "LeanPool/B/Extra.lean") + head = _commit(root, "remove Extra") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + assert compiled.exists() and not extra.exists() + + @pytest.mark.parametrize( "path", [ - "LeanPool/B.lean", - "LeanPool/B/Added.lean", "lean-toolchain", "lake-manifest.json", "lakefile.toml", "python/lean_pool/build_time_limits.py", ], ) -def test_changed_source_or_settings_avoid_download(repository, monkeypatch, path): - """Changed sources and build settings fall back before any artifact download.""" +def test_changed_settings_avoid_download(repository, monkeypatch, path): + """Changed build settings fall back before any artifact download.""" root, base, previous = repository archive, compiled = _archive(root, base, previous) target = root / path @@ -359,6 +400,63 @@ def test_lake_replays_and_rebuilds_after_setup_files_are_slimmed(repository): assert "rfl" in result.stdout + result.stderr +def _timed_build(lake: Path, root: Path, base: str) -> tuple[int, str]: + """Run the workflow's prepare, build and check sequence on both PR modules.""" + assert build_time_limits.prepare(base, root) == 0 + result = subprocess.run( + [str(lake), "build", "LeanPool.B", "LeanPool.C"], + cwd=root, + capture_output=True, + text=True, + ) + assert result.returncode == 0, result.stdout + result.stderr + log = root / "lean-build.log" + log.write_text(result.stdout + result.stderr) + return build_time_limits.check(log, base, root, 600), log.read_text() + + +def test_lake_recompiles_only_the_edited_module_of_an_earlier_pr_build( + repository, monkeypatch +): + """A later push compiles and times its edit; untouched modules keep their times.""" + root, base, _ = repository + lake = _lake() + (root / "LeanPool/C.lean").write_text("module\npublic def other : Nat := 3\n") + previous = _commit(root, "add C") + status, log = _timed_build(lake, root, base) + assert status == 0 and "Built LeanPool.B" in log and "Built LeanPool.C" in log + archive = root / "build.tar.gz" + rebase_fastpath.pack(root, base, previous, archive) + shutil.rmtree(root / ".lake/build") + (root / "LeanPool/C.lean").write_text("module\npublic def other : Nat := 4\n") + head = _commit(root, "edit C") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", head, base) + status, log = _timed_build(lake, root, base) + assert status == 0 + assert "Built LeanPool.C" in log and "Built LeanPool.B" not in log + assert build_time_limits.recorded_seconds(root, "LeanPool/B.lean") is not None + + +def test_lake_output_restored_without_a_recorded_time_is_recompiled( + repository, monkeypatch +): + """Restored output that no CI run timed cannot satisfy the build-time gate.""" + root, base, previous = repository + lake = _lake() + subprocess.run( + [str(lake), "build", "LeanPool.B"], cwd=root, check=True, capture_output=True + ) + archive = root / "build.tar.gz" + rebase_fastpath.pack(root, base, previous, archive) + shutil.rmtree(root / ".lake/build") + _download(monkeypatch, archive, previous) + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", previous, base) + assert (root / ".lake/build/lib/lean/LeanPool/B.olean").is_file() + assert build_time_limits.prepare(base, root) == 0 + assert not (root / ".lake/build/lib/lean/LeanPool/B.olean").exists() + + def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch): """Lake accepts matching artifacts without recompiling unchanged proofs.""" root, base, previous = repository @@ -382,18 +480,17 @@ def test_lake_keeps_unchanged_proof_after_metadata_edit(repository, monkeypatch) assert compiled.stat().st_mtime_ns == before -def test_untracked_source_inventory_rejected_before_overlay(repository, monkeypatch): - """The archive's full inventory also rejects an untracked added source.""" +def test_untracked_added_source_gets_no_restored_output(repository, monkeypatch): + """An added source has no earlier output; its unchanged neighbours are reused.""" root, base, previous = repository archive, compiled = _archive(root, base, previous) added = root / "LeanPool/B/Added.lean" added.parent.mkdir() added.write_text("module\n") _download(monkeypatch, archive, previous) - assert not ci_pr_build.restore_prior_build( - root, "owner/repo", 42, "pr", previous, base - ) - assert not compiled.exists() + assert ci_pr_build.restore_prior_build(root, "owner/repo", 42, "pr", previous, base) + assert compiled.read_text() == "prior compiled B" + assert not list((root / ".lake/build").rglob("Added.*")) def test_broken_archive_preserves_existing_build(repository, monkeypatch): diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py index aa0f4df530..a0d2719dee 100644 --- a/python/tests/test_validation_cache.py +++ b/python/tests/test_validation_cache.py @@ -9,12 +9,18 @@ import pytest from lean_pool.quality import _cached_pool_audits +from lean_pool.shard_validation import main as shard_main +from lean_pool.shard_validation import validate_shard from lean_pool.validation_cache import ( GLOBAL_INPUTS, ValidationCache, _module_sources, + lint_pool, + merge_receipts, pool_units, + read_receipts, source_inventory, + unit_name, ) @@ -292,3 +298,115 @@ def test_inventory_fallback_preserves_discovered_external_dependencies( assert cache.check(kind, modules, lambda: ["changed dependency"]) == [ "changed dependency" ] + + +def _shard(root: Path, *units: str) -> ValidationCache: + return ValidationCache( + root, root / ".lake/validation-cache/v1", units=frozenset(units) + ) + + +def test_units_belong_to_their_project_and_the_root_to_itself() -> None: + """Shard project names select the same units the pool is partitioned into.""" + assert unit_name("LeanPool.A.Detail") == unit_name("LeanPool.A") == "A" + assert unit_name("LeanPool") == "__root__" + + +def test_shard_cache_validates_only_its_units(repository: Path) -> None: + """Other shards' units are neither run nor given a receipt.""" + cache = _shard(repository, "A") + calls: list[str] = [] + for modules in pool_units(repository): + cache.check("lint", modules, lambda: calls.append(modules[0]) or []) + assert calls == ["LeanPool.A"] + assert list(cache.used) == ["lint:LeanPool.A"] + + +def test_shard_passes_satisfy_the_whole_pool_run_only_while_inputs_match( + repository: Path, +) -> None: + """Merged passes are reused by fingerprint; an edited project is checked again.""" + with ( + patch("lean_pool.validation_cache.subprocess.run") as lint, + patch("lean_pool.shard_validation._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + lint.return_value.returncode = 0 + fragment = repository / "fragments/ci-validation-00" + shard = ValidationCache(repository, fragment, units=frozenset({"A"})) + assert validate_shard(repository, shard) + assert sorted(read_receipts(fragment / "passes.json")) == [ + "axioms:LeanPool.A", + "backdoors:LeanPool.A", + "lint:LeanPool.A", + ] + directory = repository / ".lake/validation-cache/v1" + assert merge_receipts(directory, [fragment.parent]) == 3 + assert merge_receipts(directory, [fragment / "passes.json"]) == 0 + assert _run(repository)[1] == ["LeanPool.B", "LeanPool"] + (repository / "LeanPool/A.lean").write_text("-- edited after the shard ran\n") + merge_receipts(directory, [fragment.parent]) + assert _run(repository)[1] == ["LeanPool.A", "LeanPool"] + + +def test_shard_keeps_passes_and_reports_a_failing_unit(repository: Path) -> None: + """One failing project costs the assembling job only that project's checks.""" + + def lint(command, **kwargs): + assert kwargs["check"] is False + failed = "LeanPool.A" in command + return type("Process", (), {"returncode": int(failed)})() + + with ( + patch("lean_pool.validation_cache.subprocess.run", side_effect=lint), + patch("lean_pool.shard_validation._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + shard = _shard(repository, "A", "B") + assert not validate_shard(repository, shard) + saved = read_receipts(repository / ".lake/validation-cache/v1/passes.json") + assert "lint:LeanPool.B" in saved and "lint:LeanPool.A" not in saved + assert "axioms:LeanPool.A" in saved + + +def test_whole_pool_lint_still_stops_at_a_failing_unit(repository: Path) -> None: + """Outside a shard the linter's failure remains a hard error.""" + cache = ValidationCache(repository, repository / ".lake/validation-cache/v1") + with patch("lean_pool.validation_cache.subprocess.run") as lint: + lint_pool(repository, cache) + assert all(call.kwargs["check"] is True for call in lint.call_args_list) + + +def test_corrupt_fragments_merge_nothing(repository: Path) -> None: + """Unreadable or malformed shard output leaves the cache as it was.""" + directory = repository / ".lake/validation-cache/v1" + _run(repository) + before = read_receipts(directory / "passes.json") + bad = repository / "fragments" + bad.mkdir() + (bad / "passes.json").write_text("{") + listed = bad / "list" + listed.mkdir() + (listed / "passes.json").write_text('{"version": 1, "receipts": {"lint:X": 1}}') + assert merge_receipts(directory, [bad, repository / "missing.json"]) == 0 + assert read_receipts(directory / "passes.json") == before + + +def test_shard_command_validates_the_named_units(repository: Path) -> None: + """The workflow's entry point scopes the cache to its project list.""" + with ( + patch("lean_pool.validation_cache.subprocess.run") as lint, + patch("lean_pool.shard_validation._check_projects", return_value=[]), + patch("lean_pool.quality._audit_axioms", return_value=[]), + patch("lean_pool.quality._run_option_audit", return_value=[]), + ): + lint.return_value.returncode = 0 + assert shard_main(["--repo", str(repository), "--units", "B"]) == 0 + saved = read_receipts(repository / ".lake/validation-cache/v1/passes.json") + assert sorted(saved) == [ + "axioms:LeanPool.B", + "backdoors:LeanPool.B", + "lint:LeanPool.B", + ] diff --git a/scripts/ci/plan-build-shards.py b/scripts/ci/plan-build-shards.py index 55d22c511d..9514b8b0a0 100644 --- a/scripts/ci/plan-build-shards.py +++ b/scripts/ci/plan-build-shards.py @@ -12,7 +12,10 @@ classic one-job pipeline — the fast path for a typical PR that adds or edits one project. `sharded` splits the build across parallel jobs for the cases that take hours serially: a cold cache, a -toolchain/manifest bump, or a refactor touching many projects. +toolchain/manifest bump, a refactor touching many projects, or a change to +the lint and quality checkers' own inputs. That last case replays the build +from the warm cache, but every project must be linted and audited again +(about 100 minutes in one job), which each shard does for its own projects. Everything is computed at run time from the repository tree and the diff, so there is no static shard assignment to maintain as the pool grows. @@ -37,13 +40,17 @@ FORCE_FULL "true" to shard-build the whole pool regardless. """ +import ast import json import math import os import sys from pathlib import Path -MAX_SHARDS = 10 +# Shards also validate their projects, so a whole-pool run is bounded by its +# slowest shard. Beyond this the costliest project (MovingSofa, about 350 +# CPU-minutes cold) fills a shard alone and more shards stop helping. +MAX_SHARDS = 14 FILES_PER_SHARD = 250 # Below either threshold a serial build is already fast; sharding would # only add scheduling and artifact overhead to the common import PR. @@ -57,6 +64,25 @@ "scripts/ci/LeanPoolLinters.lean", } BUILD_COSTS_PATH = Path(__file__).with_name("build-costs.json") +VALIDATION_CACHE_PATH = ( + Path(__file__).resolve().parents[2] / "python/lean_pool/validation_cache.py" +) + + +def validation_inputs(path: Path = VALIDATION_CACHE_PATH) -> set[str]: + """Files whose change invalidates every project's lint and quality receipt. + + Read from the validation cache itself, without importing the package, so + this list cannot drift from the fingerprints it predicts. + """ + module = ast.parse(path.read_text()) + values: dict[str, tuple[str, ...]] = {} + for node in module.body: + if isinstance(node, ast.Assign) and isinstance(node.targets[0], ast.Name): + name = node.targets[0].id + if name in {"SHARED_INPUTS", "LINT_INPUTS", "QUALITY_INPUTS"}: + values[name] = tuple(ast.literal_eval(node.value)) + return {name for names in values.values() for name in names} def unit_sources() -> dict[str, list[Path]]: @@ -215,7 +241,10 @@ def main() -> None: sources = unit_sources() file_counts = {name: len(paths) for name, paths in sources.items()} global_change = bool(GLOBAL_BUILD_INPUTS.intersection(changed_files)) - full = cold or force_full or global_change or not diff_available + validation_change = bool(validation_inputs().intersection(changed_files)) + full = ( + cold or force_full or global_change or validation_change or not diff_available + ) if full: targets = set(file_counts) @@ -225,6 +254,8 @@ def main() -> None: reason = "no warm build cache" elif global_change: reason = "shared compiler or build inputs changed" + elif validation_change: + reason = "lint or quality checker inputs changed" else: reason = "no diff available for this event" else: