Keep routine PR CI focused on correctness

[Vilin97]

Ordinary proof and project-card PRs currently run duplicate documentation preflight, workflow lint, and dependency-tracking tests, while opening a ready PR automatically starts advisory profiling. Scope these jobs to the changes they validate so routine content CI spends its time on builds, linters, and repository quality checks.

• Run documentation preflight for documentation tooling and dependency changes, main publishing, and manual requests.
• Run actionlint and Action pin checks for .github/** changes, including merge-queue commits.
• Run pinned Lean dependency-tracking tests for tooling, extractor, toolchain, and Lake configuration changes, unknown diffs, and explicit full rebuilds.
• Make proof profiling opt-in through /profile or manual dispatch.
• Move cache pruning from Lean and documentation builds to hourly maintenance. Keep the newest completed main cache record per supported family and operating system, across cache versions; preserve PR and unrelated caches.

Keep all protected check names and existing PR/merge-queue triggers. Scoped jobs fail if change classification fails and include both sides of renames and Git-quoted filenames, so moving a configuration outside its directory or using Unicode/control characters cannot bypass validation. Scheduled maintenance skips empty uploads and entries with incomplete metadata. Lean compilation, warning rejection, generated-index checks, linters, quality gates, and build/validation reuse remain in place. Partial-port and metadata advisories remain outside the required checks.

Validation: actionlint 1.7.12; repository-wide Ruff lint and format checks; compiled-build reuse, rebase, and index regressions including real pinned Lean tests; 118 targeted cache, workflow, and compiled-build reuse tests including failed classification, renames, quoted filenames, large diffs, main publishing, manual requests, duplicate cache keys across versions, helper/extractor changes, and incomplete cache metadata. A read-only audit against the live cache API confirmed PR caches are excluded from scheduled pruning. All required GitHub checks passed on the final commit and in the merge queue.

[Vilin97]

Reviewed cb483c207ee02d6ec7ce805cba89576746370079. Two small fixes are needed before this draft is ready.

1. Make cache retention operate on the selected cache record, rather than finding the replacement again by key. obsolete_main_caches chooses the newest record but passes only its key to obsolete_caches, which takes the first matching record and excludes every record with that key. GitHub supports multiple cache versions sharing a key. For main records A/v1 @ t0, B/v1 @ t1, A/v2 @ t2 in one family/OS, that ordering retains B; reversing the list deletes B. Both orders retain the old A version. Carry the chosen ID/timestamp through, define retention across versions explicitly, and add a regression with duplicate keys in both list orders.

2. Reconcile the docs classifier with #624: add python/lean_pool/documentation.py and python/lean_pool/indexes.py to the new scope expression, preserve #624's push paths, and test helper-only PR and merge-group diffs. The current expression marks both paths irrelevant, so those diffs skip Documentation preflight after the two changes are combined. #624 consumes the helper for preparation, checkpointing, rendering, and validation. This finding concerns the cheap preflight; the main/manual rendering and site-validation requirements remain in place.

The reviewed workflow changes preserve Lean compilation, warning rejection, generated-index checks, linters, quality checks, build reuse, and the named aggregate gate. Failed, canceled, or missing classifications reject at the guarded jobs; valid irrelevant diffs intentionally skip them. Profiling remains available on demand. Current GitHub checks show pytest, Ruff, actionlint, Action pins, and documentation preflight successful; the full pool build is still running.

Disposition: small changes requested. I am honoring the explicit draft/do-not-merge instruction and am not editing the workflow gates.

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: cb483c207ee02d6ec7ce805cba89576746370079

Verdict: 🛑 request_changes

This infrastructure refactor scopes routine CI checks, makes profiling opt-in, and centralizes cache pruning. It reduces duplicate work but skips a dedicated exposition regression test when its inputs change. All 72 targeted cache/workflow tests and the pinned Lean embedded-name regression passed locally; hosted workflows and full-pool compilation were not exercised.

Aspect	Value
Scope	CI scoping and cache maintenance
Introduces tech debt	🛑 yes
Maintainability	🛑 regressed
Brittleness	🛑 more_brittle
Risk	🟡 medium

The dependency-test scope needs to cover the exposition extractor and its Lean regression fixture before merging.

Findings (1)

• validation-gap — .github/workflows/lean_action_ci.yml:175
  The scoped suite includes test_lake_exposition_embedded_names_preserve_semantics_without_dag_replay, which compiles scripts/exposition/Extract.lean and runs scripts/exposition/tests/EmbeddedNames.lean, but neither input matches this classifier. Executing the classifiers confirmed that changes to either file produce dependency_tests=false and skip Python CI; Exposition Verify does not execute this semantic and shared-expression performance oracle. Include scripts/exposition/ in the dependency-test scope and add classification regression cases for both inputs.

---

Tokens: 1,020,489 in / 8,993 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $4.2169 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High impact] The reviewed changes appear safe to merge; no blocking issue remains.

Summary

This PR scopes advisory and supporting CI work while keeping required check names.

• Documentation preflight runs for documentation-related changes.
• Workflow lint checks run for changes under .github/.
• Pinned Lean dependency tests run for changes that can affect dependency tracking.
• Proof profiling starts only when someone asks for it.
• Hourly cache maintenance keeps the newest completed main cache for each family and operating system.

_{Reviews (3) · Last reviewed commit: "Address cache-version retention and pres..." · Reviewed by Greptile}

[Vilin97]

Reviewed 90b9f43. The revised retention policy now explicitly protects the newest completed main-branch cache across versions, and the helper implements that policy independently of API row order. The previously reported cache-selection counterexample is resolved.

I reviewed all nine changed files and the complete changes from the previous reviewed head. The isolated cache-helper and relevant workflow-contract tests passed: 91 tests, including removed/renamed paths, quoted filenames, failed Git diffs, large diffs, reversed cache row order, and opt-in profiling.

I found no new blocker in the reviewed changes. Merge remains held for the running pool build and the full documentation-renderer result and integration with PR #624.