[Vilin97]

Summary

• keep the required Documentation preflight on pull requests while running full exposition and doc-gen only on main or an explicit dispatch preview
• cache successful lint, declaration, axiom, and option-backdoor validation per owned project unit using source, transitive import, dependency, and checker fingerprints
• keep global static checks, text style checks, and Challenge/Solution validation unconditional
• avoid packaging the large documentation artifact on ordinary pull requests

Validation

• uv sync --locked --group dev --group test
• ruff check .
• ruff format --check .
• pytest — 476 passed
• Actionlint 1.7.7 on all three edited workflows
• prior post-rebase macOS validation: real Lean CramerWold and Basic builds; cold/warm cache smoke; negative lint, axiom, and backdoor tests

This is an infrastructure-only change. The exact tested head is efd08b6064b0b82908f18c559c6bc4936722cb6c.

[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 risk] Adds validation caching to CI and changes documentation job scheduling.

The PR should not merge until the workflow-condition test stops evaluating PR-controlled text as Python code.

Findings

1.   PR-controlled condition reaches eval ▶
2.  Replacement linter lacks integration coverage ▶

Summary

The PR defers full documentation generation on ordinary pull requests and adds per-unit cached Lean validation while retaining static, style, and Challenge/Solution checks.

• Full documentation can be requested through a dispatch preview; PRs retain documentation preflight.
• Successful lint and quality receipts are fingerprinted and reused after compilation.
• The new workflow-condition test evaluates PR-controlled text as Python code.

_{Reviews (1) · Last reviewed commit: "Reuse project validation and generate fu..."}

[greptile-apps]

PR-controlled condition reaches eval
A pull request that edits docs.yml triggers Python CI, where this test reads the PR's job condition and passes it to eval. Replacing four names and clearing __builtins__ does not make that expression safe: a crafted condition can execute code on the test runner before an assertion fails. Parse the limited condition syntax instead.

How this was verified: The test passes if: text from the checked-out docs.yml to eval, and edits to that workflow trigger the pytest job.

[greptile-apps]

Replacement linter lacks integration coverage
These cache tests mock the axiom and backdoor audits but never run the new Lean declaration linter, which CI now uses instead of runLinter LeanPool. A regression in declaration selection or linter invocation could leave lint coverage missing while the Python tests stay green. Add a small compiled Lean fixture that exercises both a passing declaration and a rejected finding through the new command.

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!