[Vilin97]

Summary

• Sets warningAsError = true in lakefile.toml [leanOptions], matching Tau Ceti.
• Documents the rule in CONTRIBUTING.md (and the generated CLAUDE.md/AGENTS.md) and .github/CODE_QUALITY.md.

Why

CI already rejects warnings by grepping the build log. Putting the rule in the compiler adds:

• Local builds match CI. lake build LeanPool.<Project> fails on a warning on the contributor's machine, not only after a CI round-trip.
• Caches can't hide warnings. A module that warns produces no .olean, so an incremental or cache-restored build can't skip past it. Before, a clean rebuild could turn up warnings an incremental build never showed.
• No opt-out. Pool sources can't set warningAsError false, because the quality gate bans set_option.

The log grep stays, to catch warnings that Lake itself prints.

Effects

• Changing leanOptions changes every module's build trace, so this PR's CI and the first main build after merge rebuild the whole pool. Main is already warning-free under the grep gate, so the rebuild should succeed.
• mathlib-bump.yml: a project that only warns after a bump now fails to build, so triage sends it to the repair fan-out. That is intended, since repairs already fix warnings.

Test plan

• A local canary module with an unused variable fails lake build with error: … Variable name \h` is not explicitly referenced. With _h` it builds.
• lake build LeanPool.FiveEighthsTheorem LeanPool.Apportionment mk_all builds with no warnings or errors under the new option.
• CI: full-pool build plus the gates

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

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

[Medium impact] The PR appears safe to merge; no blocking issue remains.

Summary

The PR sets warningAsError = true in lakefile.toml and documents the rule.

• Lean warnings now stop module compilation as errors.

_{Reviews (3) · Last reviewed commit: "Keep warning policy compatible with proo..." · Reviewed by Greptile}

[Vilin97]

Technical source review at a5c83b04a269efa2d1e65aa7d419c3ed88e871e9: the comment issue is fixed. I checked the complete five-file change and the published repair; the repair changes only the lakefile comment, leaving parsed TOML and all other source objects unchanged. The exact existing _check_lake_options now returns no errors for that lakefile. No further technical source finding remains.

The inspected Lean/Lake 4.35 paths support the warning behavior and include strong options in module/cache traces. This review does not reproduce the author’s builds or qualify full-pool CI.

Changing [leanOptions] and .github/CODE_QUALITY.md still needs the separate direct scoped authorization required by CONTRIBUTING.md. That policy decision remains pending; this technical review grants no gate-change authority. Required current-head validation and normal protected integration also remain separate. No branch edit, queue admission, auto-merge or merge was made.

[Vilin97]

Maintainer authorization: @Vilin97 directly authorized merging this PR, including its gate changes, in a Claude Code session on 2026-11-05. This is recorded for the permanent reviewer in Vilin97/lean-pool-automation#11. Merge it through the normal protected queue only, with no waivers.

🤖 Posted by Claude Code

[Vilin97]

Technical source review at 63a15b5b8dd7fe9753e30a408fce0c2210bea8b1: the native conflict with #712 is fixed by moving the existing warning-policy explanation into a separate paragraph below the gate list. The repair changes only .github/CODE_QUALITY.md; it preserves every accepted claim, the parsed warningAsError = true setting, and all other authored files. Ordinary three-way merges of all five PR files now succeed against the current #712 queue base, retaining its compiler plugin and proof-length policy.

The earlier head’s CI does not qualify this revision. This head requires its own applicable checks and normal protected integration before queue re-entry. The direct scoped authorization for #751 remains in force.