diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 8d6b9c9ca0..f1807d11f7 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -13,6 +13,9 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/quality.py' + - 'python/lean_pool/challenge.py' + - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'scripts/exposition/**' - '.github/workflows/docs.yml' @@ -34,11 +37,20 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/quality.py' + - 'python/lean_pool/challenge.py' + - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'scripts/exposition/**' - '.github/workflows/notice.yml' - '.github/workflows/docs.yml' workflow_dispatch: + inputs: + preview: + description: "Generate full documentation for this branch on demand" + type: boolean + required: false + default: false concurrency: group: ${{ github.workflow }}-${{ github.ref }} @@ -157,7 +169,10 @@ jobs: # Exposition consumes compiled Lean, not doc-gen's Mathlib SQLite data. # Reuse the matching CI artifact directly instead of waiting for docInfo. needs: preflight - if: needs.preflight.outputs.readme_only != 'true' + if: >- + needs.preflight.outputs.readme_only != 'true' && + ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || + (github.event_name == 'workflow_dispatch' && inputs.preview)) runs-on: ubuntu-latest name: Build exposition site steps: @@ -278,7 +293,10 @@ jobs: # can consume the remainder of GitHub's six-hour job limit. mathlib_doc_info: needs: preflight - if: needs.preflight.outputs.readme_only != 'true' + if: >- + needs.preflight.outputs.readme_only != 'true' && + ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || + (github.event_name == 'workflow_dispatch' && inputs.preview)) runs-on: ubuntu-latest name: Build Mathlib documentation data steps: @@ -368,7 +386,10 @@ jobs: needs: - preflight - mathlib_doc_info - if: needs.preflight.outputs.readme_only != 'true' + if: >- + needs.preflight.outputs.readme_only != 'true' && + ((github.ref == 'refs/heads/main' && github.event_name != 'pull_request') || + (github.event_name == 'workflow_dispatch' && inputs.preview)) runs-on: ubuntu-latest name: Build doc-gen4 site steps: diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index b65dba82c3..ac0e261afc 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -34,6 +34,7 @@ on: - 'Challenge/challenges.yml' - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' + - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/pyproject.toml' - 'python/uv.lock' @@ -61,6 +62,7 @@ on: - 'Challenge/challenges.yml' - 'python/lean_pool/challenge.py' - 'python/lean_pool/quality.py' + - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' - 'python/pyproject.toml' - 'python/uv.lock' @@ -229,9 +231,11 @@ jobs: # Publish once compilation succeeds, so docs can overlap the later # linters/quality checks without compiling the same PR a second time. - name: Package build for documentation + if: github.event_name != 'pull_request' run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack - name: Share build with documentation + if: github.event_name != 'pull_request' uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 with: name: lean-pool-build @@ -240,9 +244,24 @@ jobs: compression-level: 0 retention-days: 1 + # Actions scopes PR caches to refs/pull//merge: updates to the same + # PR can reuse receipts, while main and other PRs cannot read them. + - name: Restore project validation + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/validation-cache/v1 + key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} + restore-keys: | + LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + + - name: Install validation dependencies + run: cd python && uv sync --locked + - name: Lint run: | - ~/.elan/bin/lake exe runLinter LeanPool + cd python + uv run python -m lean_pool.validation_cache lint --repo .. + cd .. ~/.elan/bin/lake exe runLinter Challenge ~/.elan/bin/lake exe runLinter Solution @@ -255,8 +274,14 @@ jobs: - name: Repository quality checks run: | cd python - uv sync --locked - uv run python -m lean_pool.quality --repo .. + uv run python -m lean_pool.validation_cache quality --repo .. + + - name: Save project validation + # Successful receipts are tiny; retain PR results across registry rebases. + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/validation-cache/v1 + key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - name: Save Lean dependencies if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' @@ -465,9 +490,11 @@ jobs: # Publish once compilation succeeds, so docs can overlap the later # linters/quality checks without compiling the same PR a second time. - name: Package build for documentation + if: github.event_name != 'pull_request' run: PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack - name: Share build with documentation + if: github.event_name != 'pull_request' uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 with: name: lean-pool-build @@ -476,9 +503,24 @@ jobs: compression-level: 0 retention-days: 1 + # Actions scopes PR caches to refs/pull//merge: updates to the same + # PR can reuse receipts, while main and other PRs cannot read them. + - name: Restore project validation + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/validation-cache/v1 + key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} + restore-keys: | + LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}- + + - name: Install validation dependencies + run: cd python && uv sync --locked + - name: Lint run: | - ~/.elan/bin/lake exe runLinter LeanPool + cd python + uv run python -m lean_pool.validation_cache lint --repo .. + cd .. ~/.elan/bin/lake exe runLinter Challenge ~/.elan/bin/lake exe runLinter Solution @@ -491,8 +533,14 @@ jobs: - name: Repository quality checks run: | cd python - uv sync --locked - uv run python -m lean_pool.quality --repo .. + uv run python -m lean_pool.validation_cache quality --repo .. + + - name: Save project validation + # Successful receipts are tiny; retain PR results across registry rebases. + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: .lake/validation-cache/v1 + key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - name: Save Lean dependencies if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' diff --git a/.github/workflows/python_ci.yml b/.github/workflows/python_ci.yml index f3ea4ba9f2..87f2878fc8 100644 --- a/.github/workflows/python_ci.yml +++ b/.github/workflows/python_ci.yml @@ -9,6 +9,8 @@ on: - 'NOTICE' - 'NOTICE.extra.yml' - '.github/workflows/python_ci.yml' + - '.github/workflows/lean_action_ci.yml' + - '.github/workflows/docs.yml' pull_request: branches: - main @@ -23,6 +25,8 @@ on: - 'NOTICE' - 'NOTICE.extra.yml' - '.github/workflows/python_ci.yml' + - '.github/workflows/lean_action_ci.yml' + - '.github/workflows/docs.yml' workflow_dispatch: concurrency: diff --git a/python/ci-performance.md b/python/ci-performance.md index 37aa5cf8cf..5b60c20c55 100644 --- a/python/ci-performance.md +++ b/python/ci-performance.md @@ -71,3 +71,45 @@ for both output files on cold extraction, cache reuse, and forced refresh. Cache reuse took under a millisecond, versus 5–13 seconds for extraction on that machine. This is a small-project correctness check, not a whole-pool timing claim. Measure full-run savings after the main-branch extraction cache has been seeded. + +## Pull-request scheduling and project validation + +Pull requests retain the required `Documentation preflight` check, including +workspace compatibility and generated-root checks. Full exposition/doc-gen +jobs run on main; use the Documentation workflow's `preview` input to generate +branch artifacts on demand. Branch previews never deploy production Pages. +Ordinary PR builds no longer package the large documentation build artifact. + +After compilation, Lean CI partitions every pool source into project units, +including Basic, the root, nested files and unregistered modules. Declaration +lint, axiom audits and option-backdoor audits import all owned modules; each +compiled declaration is checked in its owning unit. Registry declarations use +separate per-entry receipts. Static checks (registry/card consistency, +reachability, forbidden constructs, size limits and Lake options), text style +lint, and Challenge/Solution validation still run every time. + +`.lake/validation-cache/v1/passes.json` contains successful receipts keyed by +source contents, each module's transitive compiler import inventory, toolchain, +dependency pins, build options and checker code. Missing import inventories +conservatively hash all local Lean sources. Changes to a project's registry +entry invalidate its declaration check without invalidating sibling projects. +Adding, deleting or editing modules changes the validation coverage. Failed +checks never publish receipts. A registry-only rebase can therefore reuse +proof validation while still checking the registry and generated cards. + +Actions saves the small receipt cache after all gates pass. PR cache scope is +`refs/pull//merge`, so a PR can reuse its previous validation across rebases, +but main and other PRs cannot consume its receipts. Main receipts are available +to all branches. The first run after shipping, a toolchain bump or a checker +change remains cold; subsequent runs should avoid validating unchanged projects. + +To bypass receipts for comparison, from `python/`: + +```sh +uv run python -m lean_pool.validation_cache lint --repo .. --refresh +uv run python -m lean_pool.validation_cache quality --repo .. --refresh +``` + +This does not eliminate GitHub's strict up-to-date check requirement or registry +merge conflicts. CI still runs for a new merge result, with compilation handled +by Lake's existing incremental build cache and validation reused by content. diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 114dba8df3..faf5f5d373 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -27,6 +27,7 @@ import yaml from lean_pool import challenge +from lean_pool.validation_cache import ValidationCache, pool_units # Derived from the challenge module so the pool gate and the axiom list # handed to the external comparator judge cannot drift apart. @@ -677,17 +678,19 @@ def gatedLiteral? (e : Expr) : Option String := | some (.lit (.strVal s)) => some s | _ => none -def auditEnv (env : Environment) (roots : List Name) : IO Unit := do +def auditEnv (env : Environment) (roots : List Name) + (onlyModules : List Name) : IO Unit := do let manipulators := manipulatorCandidates.filter env.contains let injectors := axiomInjectorCandidates.filter env.contains let mut visited : NameSet := NameSet.empty for (moduleName, data) in env.header.moduleNames.zip env.header.moduleData do unless roots.contains moduleName.getRoot do continue + unless onlyModules.isEmpty || onlyModules.contains moduleName do continue for declName in data.constNames do unless visited.contains declName do visited := visited.insert declName if let some info := env.find? declName then - let exprs := info.type :: info.value?.toList + let exprs := info.type :: (info.value? (allowOpaque := true)).toList let used := exprs.foldl (fun acc e => acc ++ e.getUsedConstants) #[] let mut details : List String := [] let hits := manipulators.filter used.contains @@ -713,11 +716,16 @@ def auditEnv (env : Environment) (roots : List Name) : IO Unit := do end LeanPoolQuality.OptionAudit def main (args : List String) : IO UInt32 := do - let modules := if args.isEmpty then [`LeanPool] else args.map (·.toName) + let imports := args.takeWhile (· != "--only") + let onlyModules := (args.dropWhile (· != "--only")).drop 1 |>.map (·.toName) + let modules := if imports.isEmpty then [`LeanPool] else imports.map (·.toName) Lean.initSearchPath (<- Lean.findSysroot) let imports := modules.toArray.map fun module => ({ module } : Lean.Import) let env <- Lean.importModules imports {} (trustLevel := 1024) - LeanPoolQuality.OptionAudit.auditEnv env (modules.map (·.getRoot)) + for moduleName in onlyModules do + unless env.header.moduleNames.contains moduleName do + throw <| IO.userError s!"missing module in audit environment: {moduleName}" + LeanPoolQuality.OptionAudit.auditEnv env (modules.map (·.getRoot)) onlyModules return 0 """ # Detail emitted by the audit when a declaration is a `sorry`. Tolerated @@ -743,18 +751,21 @@ def _check_option_backdoors(root: Path) -> list[_QualityError]: return errors -def _run_option_audit(root: Path, modules: list[str]) -> list[_QualityError]: +def _run_option_audit( + root: Path, modules: list[str], *, only_modules: list[str] | None = None +) -> list[_QualityError]: """Run the environment audit over one set of importable modules.""" with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: temp_path = Path(temp_file.name) temp_file.write(_OPTION_AUDIT_LEAN) temp_file.flush() - index_path = root / f"{modules[0]}.lean" + index_path = _module_to_path(root, modules[0]) try: try: process = subprocess.run( - ["lake", "env", "lean", "--run", str(temp_path), *modules], + ["lake", "env", "lean", "--run", str(temp_path), *modules] + + (["--only", *only_modules] if only_modules is not None else []), cwd=root, check=False, capture_output=True, @@ -898,15 +909,16 @@ def _check_solution_axioms(root: Path) -> list[_QualityError]: def _audit_axioms( root: Path, declarations: list[_Declaration], - import_module: str, + import_module: str | list[str], open_declarations: set[str], ) -> list[_QualityError]: """Run `#print axioms` over ``declarations`` and grade the results.""" if not declarations: return [] - index_path = root / f"{import_module}.lean" - commands = f"import {import_module}\n" + "\n".join( + modules = [import_module] if isinstance(import_module, str) else import_module + index_path = _module_to_path(root, modules[0]) + commands = "".join(f"import {module}\n" for module in modules) + "\n".join( f"#print axioms _root_.{declaration.name}" for declaration in declarations ) with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: @@ -1110,7 +1122,9 @@ def _load_projects_yaml( return data, [] -def _check_projects(root: Path) -> list[_QualityError]: +def _check_projects( + root: Path, validation_cache: ValidationCache | None = None +) -> list[_QualityError]: data, errors = _load_projects_yaml(root) if data is None: return errors @@ -1132,7 +1146,7 @@ def _check_projects(root: Path) -> list[_QualityError]: return errors for index, project in enumerate(projects, start=1): - errors.extend(_check_project(root, path, index, project)) + errors.extend(_check_project(root, path, index, project, validation_cache)) return errors @@ -1228,6 +1242,7 @@ def _check_project( path: Path, index: int, project: Any, + validation_cache: ValidationCache | None = None, ) -> list[_QualityError]: if not isinstance(project, dict): return [_QualityError(path, 1, f"project #{index} must be a mapping")] @@ -1238,7 +1253,17 @@ def _check_project( return errors entry_path = _module_to_path(root, project["entry_module"]) - errors.extend(_check_project_declarations(root, path, project)) + if validation_cache is None: + errors.extend(_check_project_declarations(root, path, project)) + else: + errors.extend( + validation_cache.check( + "declarations", + [project["entry_module"]], + lambda: _check_project_declarations(root, path, project), + metadata=project, + ) + ) errors.extend(_check_project_card(entry_path, path, project)) return errors @@ -1830,7 +1855,12 @@ def _write_project_card(path: Path, card: str) -> None: path.write_text(new_text) -def run_checks(root: Path, *, skip_lean_axioms: bool = False) -> list[_QualityError]: +def run_checks( + root: Path, + *, + skip_lean_axioms: bool = False, + validation_cache: ValidationCache | None = None, +) -> list[_QualityError]: """Run all deterministic quality checks.""" checks = [ _check_reachability, @@ -1840,20 +1870,48 @@ def run_checks(root: Path, *, skip_lean_axioms: bool = False) -> list[_QualityEr _check_style_nolints, _check_file_sizes, _check_proof_sizes, - _check_projects, _check_challenges, ] errors = [error for check in checks for error in check(root)] + errors.extend(_check_projects(root, validation_cache)) if not skip_lean_axioms: - errors.extend(_check_axioms(root)) + if validation_cache is None: + errors.extend(_check_axioms(root)) + errors.extend(_check_option_backdoors(root)) + else: + errors.extend(_cached_pool_audits(root, validation_cache)) + for library in (challenge.LIBRARY_NAME, challenge.SOLUTION_LIBRARY_NAME): + if (root / f"{library}.lean").exists(): + errors.extend(_run_option_audit(root, [library])) errors.extend(_check_challenge_axioms(root)) errors.extend(_check_solution_axioms(root)) - errors.extend(_check_option_backdoors(root)) return sorted( errors, key=lambda error: (str(error.path), error.line, error.message) ) +def _cached_pool_audits(root: Path, cache: ValidationCache) -> list[_QualityError]: + """Cover all pool declarations, with current static reachability checked above.""" + errors: list[_QualityError] = [] + for modules in pool_units(root): + paths = [_module_to_path(root, module) for module in modules] + errors.extend( + cache.check( + "axioms", + modules, + lambda: _audit_axioms(root, _declarations_in(paths), modules, set()), + ) + ) + errors.extend( + cache.check( + "backdoors", + modules, + lambda: _run_option_audit(root, modules, only_modules=modules), + ) + ) + return errors + + def _parse_args(argv: list[str]) -> argparse.Namespace: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument( diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py new file mode 100644 index 0000000000..b9fe844067 --- /dev/null +++ b/python/lean_pool/validation_cache.py @@ -0,0 +1,210 @@ +"""Reuse successful project validation after compiling the current checkout. + +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. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import logging +import subprocess +from collections.abc import Callable +from pathlib import Path +from typing import Any + +LOGGER = logging.getLogger(__name__) +GLOBAL_INPUTS = ( + "lean-toolchain", + "lake-manifest.json", + "lakefile.toml", + "lakefile.lean", + "scripts/nolints.json", + "scripts/nolints-style.txt", + "scripts/ci/lint-project.lean", + "python/lean_pool/quality.py", + "python/lean_pool/challenge.py", + "python/lean_pool/validation_cache.py", + "python/pyproject.toml", + "python/uv.lock", + ".github/workflows/lean_action_ci.yml", +) + + +def pool_units(root: Path) -> list[list[str]]: + """Partition every pool source, including the root and unregistered modules.""" + units: dict[str, list[str]] = {} + for path in sorted((root / "LeanPool").rglob("*.lean")): + relative = path.relative_to(root).with_suffix("") + unit = relative.parts[1] + units.setdefault(unit, []).append(".".join(relative.parts)) + if (root / "LeanPool.lean").exists(): + units["__root__"] = ["LeanPool"] + return [sorted(modules) for _, modules in sorted(units.items())] + + +def source_inventory(root: Path, modules: list[str]) -> set[Path]: + """Use every module's compiler inventory; fall back to all local Lean sources.""" + paths = {root / (module.replace(".", "/") + ".lean") for module in modules} + try: + for module in modules: + setup = root / ( + ".lake/build/ir/" + module.replace(".", "/") + ".setup.json" + ) + inventory = json.loads(setup.read_text()) + if inventory["name"] != module or not isinstance( + inventory["importArts"], dict + ): + raise ValueError("invalid compiler inventory") + for imported in inventory["importArts"]: + path = root / (imported.replace(".", "/") + ".lean") + if path.is_file(): + paths.add(path) + elif imported.split(".")[0] in {"LeanPool", "Challenge", "Solution"}: + raise ValueError(f"missing imported source: {imported}") + except (OSError, ValueError, KeyError, TypeError): + LOGGER.warning( + "%s: missing import inventory; hashing all local sources", modules[0] + ) + for library in ("LeanPool", "Challenge", "Solution"): + paths.update((root / library).rglob("*.lean")) + index = root / f"{library}.lean" + if index.exists(): + paths.add(index) + return paths + + +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.""" + self.root = root + self.directory = directory + self.refresh = refresh + self.digests: dict[Path, str] = {} + self.receipts: dict[str, dict[str, Any]] = {} + 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 + + def fingerprint(self, modules: list[str], metadata: Any = None) -> str: + """Hash all checked inputs, retaining missing optional files in the key.""" + paths = source_inventory(self.root, modules) + paths.update(self.root / name for name in GLOBAL_INPUTS) + inputs = {} + for path in sorted(paths): + if path not in self.digests: + self.digests[path] = ( + hashlib.sha256(path.read_bytes()).hexdigest() + if path.is_file() + else "missing" + ) + inputs[path.relative_to(self.root).as_posix()] = self.digests[path] + payload = {"inputs": inputs, "modules": modules, "metadata": metadata} + return hashlib.sha256(json.dumps(payload, sort_keys=True).encode()).hexdigest() + + def check[T]( + self, + kind: str, + modules: list[str], + validate: Callable[[], list[T]], + metadata: Any = None, + ) -> list[T]: + """Run on a miss and retain only passes; failures never create receipts.""" + digest = self.fingerprint(modules, metadata) + key = f"{kind}:{modules[0]}" + expected = {"fingerprint": digest, "modules": modules, "passed": True} + if not self.refresh and self.receipts.get(key) == expected: + self.hits += 1 + self.used[key] = expected + LOGGER.info("%s: cache hit", key) + return [] + self.misses += 1 + LOGGER.info("%s: validating", key) + errors = validate() + if not errors: + self.used[key] = expected + return errors + + 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") + 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.""" + for modules in pool_units(root): + + def validate() -> list[str]: + subprocess.run( + [ + "lake", + "env", + "lean", + "--run", + "scripts/ci/lint-project.lean", + *modules, + ], + cwd=root, + check=True, + ) + return [] + + cache.check("lint", modules, validate) + + +def main() -> int: + """Run the cached declaration linter or repository quality checker.""" + from lean_pool.quality import run_checks + + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("check", choices=("lint", "quality")) + 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") + arguments = parser.parse_args() + logging.basicConfig(level=logging.INFO, format="validation: %(message)s") + root = arguments.repo.resolve() + cache = ValidationCache(root, root / arguments.cache, refresh=arguments.refresh) + if arguments.check == "lint": + lint_pool(root, cache) + # Keep quality receipts for the subsequent step. + cache.used = { + key: receipt + for key, receipt in cache.receipts.items() + if not key.startswith("lint:") + } | cache.used + errors = [] + else: + errors = run_checks(root, validation_cache=cache) + cache.used |= { + key: receipt + for key, receipt in cache.receipts.items() + if key.startswith("lint:") + } + for error in errors: + print(error.format(root)) + if errors: + return 1 + cache.save() + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 76a9e99387..3a754ae900 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -39,3 +39,80 @@ def test_shared_cache_paths_and_keys_match() -> None: assert set(producers) == set(contracts) == {"dependencies", "build"} assert contracts["dependencies"][1] == ("~/.elan", ".lake/packages") assert contracts["build"][1] == (".lake/build",) + + +def _docs_condition(condition: str, event: str, ref: str, preview: bool, readme: bool): + """Evaluate the small event predicate used by docs job allocation.""" + expression = condition + values = { + "needs.preflight.outputs.readme_only": repr(str(readme).lower()), + "github.event_name": repr(event), + "github.ref": repr(ref), + "inputs.preview": repr(preview), + } + for name, value in values.items(): + expression = expression.replace(name, value) + return eval( + expression.replace("&&", " and ").replace("||", " or "), + {"__builtins__": {}}, + {}, + ) + + +def test_docs_generate_on_main_and_explicit_preview_only() -> None: + """A PR runs its protected preflight without allocating heavy docs runners.""" + jobs = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())["jobs"] + assert jobs["preflight"]["name"] == "Documentation preflight" + assert "if" not in jobs["preflight"] + scenarios = [ + ("pull_request", "refs/pull/123/merge", False, False, False), + ("push", "refs/heads/main", False, False, True), + ("workflow_dispatch", "refs/heads/main", False, False, True), + ("workflow_dispatch", "refs/heads/topic", False, False, False), + ("workflow_dispatch", "refs/heads/topic", True, False, True), + ("pull_request", "refs/pull/123/merge", True, False, False), + ("push", "refs/heads/main", False, True, False), + ] + for name in ("exposition", "mathlib_doc_info", "build"): + for event, ref, preview, readme, expected in scenarios: + assert ( + _docs_condition(jobs[name]["if"], event, ref, preview, readme) + == expected + ) + # Branch previews produce artifacts but cannot replace production Pages. + assert not _docs_condition( + jobs["deployment_freshness"]["if"], + "workflow_dispatch", + "refs/heads/topic", + True, + False, + ) + + +def test_single_and_sharded_builds_use_validation_cache() -> None: + """Both execution paths validate before saving receipts and keep the same gate.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + assert jobs["gate"]["name"] == "Build project" + contracts = [] + for job in ("build", "finalize"): + steps = jobs[job]["steps"] + names = [step.get("name") for step in steps] + assert names.index("Restore project validation") < names.index("Lint") + assert names.index("Repository quality checks") < names.index( + "Save project validation" + ) + restore = steps[names.index("Restore project validation")] + save = steps[names.index("Save project validation")] + assert restore["with"]["key"] == save["with"]["key"] + assert ( + restore["with"]["path"] + == save["with"]["path"] + == ".lake/validation-cache/v1" + ) + assert "if" not in save # normal success guard, including PR updates + contracts.append(restore["with"]) + assert "validation_cache lint" in steps[names.index("Lint")]["run"] + assert "runLinter Challenge" in steps[names.index("Lint")]["run"] + assert "runLinter Solution" in steps[names.index("Lint")]["run"] + assert "lint-style LeanPool" in steps[names.index("Text style lint")]["run"] + assert contracts[0] == contracts[1] diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py new file mode 100644 index 0000000000..8443354c1d --- /dev/null +++ b/python/tests/test_validation_cache.py @@ -0,0 +1,158 @@ +"""Check validation coverage, dependency invalidation, and pass-only cache reuse.""" + +from __future__ import annotations + +import json +from pathlib import Path +from unittest.mock import patch + +import pytest + +from lean_pool.quality import _cached_pool_audits +from lean_pool.validation_cache import GLOBAL_INPUTS, ValidationCache, pool_units + + +def _inventory(root: Path, module: str, imports: tuple[str, ...] = ()) -> None: + path = root / (".lake/build/ir/" + module.replace(".", "/") + ".setup.json") + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps({"name": module, "importArts": dict.fromkeys(imports)})) + + +@pytest.fixture +def repository(tmp_path: Path) -> Path: + """Create independent units, a nested module, and compiler import inventories.""" + for module in ("LeanPool", "LeanPool.A", "LeanPool.A.Detail", "LeanPool.B"): + path = tmp_path / (module.replace(".", "/") + ".lean") + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(f"-- {module}\n") + _inventory(tmp_path, module) + _inventory(tmp_path, "LeanPool", ("LeanPool.A", "LeanPool.A.Detail", "LeanPool.B")) + for name in GLOBAL_INPUTS: + if name in {"lakefile.lean", "scripts/nolints.json"}: + continue + path = tmp_path / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text("configuration\n") + return tmp_path + + +def _run(root: Path, *, refresh: bool = False) -> tuple[ValidationCache, list[str]]: + cache = ValidationCache(root, root / ".lake/validation-cache/v1", refresh=refresh) + calls: list[str] = [] + for modules in pool_units(root): + cache.check("lint", modules, lambda: calls.append(modules[0]) or []) + cache.save() + return cache, calls + + +def test_coverage_and_warm_reuse(repository: Path) -> None: + """Every file belongs to a unit, even without a registry or umbrella import.""" + units = pool_units(repository) + covered = [module for modules in units for module in modules] + assert sorted(covered) == [ + "LeanPool", + "LeanPool.A", + "LeanPool.A.Detail", + "LeanPool.B", + ] + assert len(_run(repository)[1]) == 3 + assert _run(repository)[1] == [] + assert len(_run(repository, refresh=True)[1]) == 3 + + +def test_project_edit_leaves_sibling_cached(repository: Path) -> None: + """A rebase reuses identical sources regardless of commit SHA or registry order.""" + _run(repository) + (repository / "LeanPool/projects.yml").write_text("projects: []\n") + assert _run(repository)[1] == [] + (repository / "LeanPool/A/Detail.lean").write_text("-- edited nested source\n") + assert _run(repository)[1] == ["LeanPool.A", "LeanPool"] + + +def test_transitive_import_of_nested_module_invalidates_consumer( + repository: Path, +) -> None: + """Dependencies of each nested module count, not just umbrella dependencies.""" + _inventory(repository, "LeanPool.A.Detail", ("LeanPool.B",)) + _run(repository) + (repository / "LeanPool/B.lean").write_text("-- dependency edit\n") + assert len(_run(repository)[1]) == 3 + + +@pytest.mark.parametrize("name", GLOBAL_INPUTS) +def test_checker_and_dependency_changes_invalidate_all( + repository: Path, name: str +) -> None: + """Toolchain, dependencies, lint options, and checker implementations are inputs.""" + _run(repository) + (repository / name).write_text("changed\n") + assert len(_run(repository)[1]) == 3 + + +@pytest.mark.parametrize("contents", [None, "{", "{}", '{"name": "wrong"}']) +def test_missing_inventory_falls_back_conservatively( + repository: Path, contents +) -> None: + """A missing/broken nested inventory must not produce a false cache hit.""" + path = repository / ".lake/build/ir/LeanPool/A/Detail.setup.json" + if contents is None: + path.unlink() + else: + path.write_text(contents) + _run(repository) + (repository / "LeanPool/B.lean").write_text("-- changed\n") + assert len(_run(repository)[1]) == 3 + + +def test_metadata_is_scoped_to_one_project(repository: Path) -> None: + """Changing one card's declaration list invalidates that check only.""" + modules = ["LeanPool.A"] + cache = ValidationCache(repository, repository / ".lake/validation-cache/v1") + cache.check("declarations", modules, lambda: [], {"main_declarations": ["a"]}) + cache.save() + cache = ValidationCache(repository, cache.directory) + assert cache.check( + "declarations", modules, lambda: ["error"], {"main_declarations": ["b"]} + ) == ["error"] + + +def test_failures_and_corrupt_receipts_are_rechecked(repository: Path) -> None: + """Failed validators and malformed saved data cannot create successful hits.""" + cache = ValidationCache(repository, repository / ".lake/validation-cache/v1") + assert cache.check("lint", ["LeanPool.A"], lambda: ["bad proof"]) == ["bad proof"] + cache.save() + assert _run(repository)[0].misses == 3 + (cache.directory / "passes.json").write_text("broken") + assert _run(repository)[0].misses == 3 + + +def test_added_deleted_sources_change_coverage(repository: Path) -> None: + """New files are checked and deleted units are removed from the cache.""" + _run(repository) + (repository / "LeanPool/B.lean").unlink() + (repository / "LeanPool/C.lean").write_text("-- new project\n") + _inventory(repository, "LeanPool.C") + _inventory(repository, "LeanPool", ("LeanPool.A", "LeanPool.C")) + cache, calls = _run(repository) + assert calls == ["LeanPool.C", "LeanPool"] + assert "lint:LeanPool.B" not in cache.used + + +def test_quality_audits_cover_every_owned_module(repository: Path) -> None: + """Cold and warm checks preserve complete axiom/backdoor coverage.""" + cache = ValidationCache(repository, repository / ".lake/validation-cache/v1") + with ( + patch("lean_pool.quality._audit_axioms", return_value=[]) as axioms, + patch("lean_pool.quality._run_option_audit", return_value=[]) as backdoors, + ): + assert _cached_pool_audits(repository, cache) == [] + assert [call.args[2] for call in axioms.call_args_list] == pool_units( + repository + ) + assert [ + call.kwargs["only_modules"] for call in backdoors.call_args_list + ] == pool_units(repository) + cache.save() + cache = ValidationCache(repository, cache.directory) + assert _cached_pool_audits(repository, cache) == [] + assert axioms.call_count == backdoors.call_count == 3 diff --git a/scripts/ci/lint-project.lean b/scripts/ci/lint-project.lean new file mode 100644 index 0000000000..ef11d023dc --- /dev/null +++ b/scripts/ci/lint-project.lean @@ -0,0 +1,43 @@ +import Batteries.Tactic.Lint + +/- Run the same slow declaration linters as Batteries' runLinter, importing +all owned modules together. Filter by module identity so each declaration +is covered exactly once even when one project imports another. -/ +open Lean Core Batteries.Tactic.Lint + +unsafe def main (args : List String) : IO UInt32 := do + if args.isEmpty then throw <| IO.userError "no modules to lint" + let modules := args.toArray.map String.toName + Lean.initSearchPath (← Lean.findSysroot) + Lean.enableInitializersExecution + let imports := (modules.push `Batteries.Tactic.Lint).map fun module => + ({ module } : Lean.Import) + let env ← Lean.importModules imports {} (trustLevel := 1024) (loadExts := true) + for module in modules do + unless env.header.moduleNames.contains module do + throw <| IO.userError s!"missing module in lint environment: {module}" + let nolintsFile : System.FilePath := "scripts/nolints.json" + let nolints : Array (Name × Name) ← if ← nolintsFile.pathExists then do + let json ← IO.ofExcept (Json.parse (← IO.FS.readFile nolintsFile)) + IO.ofExcept (fromJson? json) + else pure #[] + let (failed, _) ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) + (s := { env }) do + let indices := env.header.moduleNames.map modules.contains + let decls := env.constants.map₁.fold (init := #[]) fun decls name _ => + if indices[env.const2ModIdx[name]?.get!]! then decls.push name else decls + let linters ← getChecks (slow := true) (runAlways := none) (runOnly := none) + let results ← lintCore decls linters (inIO := true) (currentModule := modules[0]!) + let results := results.map fun (linter, findings) => + (linter, nolints.foldl (init := findings) fun findings (linter', declaration) => + if linter.name == linter' then findings.erase declaration else findings) + if results.any (!·.2.isEmpty) then + let message ← formatLinterResults results decls + (groupByFilename := true) (useErrorFormat := true) + s!"in {modules[0]!}" (runSlowLinters := true) .medium linters.size + IO.println (← message.toString) + return true + IO.println s!"Lint passed for {modules.size} modules ({decls.size} declarations)." + return false + -- Match runLinter's exit shortcut around Lean IO finalizer races. + IO.Process.exit (if failed then 1 else 0)