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..eeae274f49 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,31 @@ jobs: echo "Mathlib already present from cache" fi + - name: Install uv + if: github.event_name == 'pull_request' + 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 +665,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 @@ -817,15 +852,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 @@ -1092,12 +1128,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..0f49dfb9c0 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -37,6 +37,25 @@ 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. + 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/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..fc6bf67e50 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -267,11 +267,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):