Make every Lean warning a compile error (warningAsError, like Tau Ceti)

.github/CODE_QUALITY.md

@@ -15,6 +15,10 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for
 - `lake exe lint-style` on `LeanPool`
 - `python -m lean_pool.quality --repo ..`
 
+With `warningAsError = true` in `lakefile.toml`, every Lean warning is a
+compile error (locally too). The warning scan over the build log remains for
+warnings Lake itself prints.
+
 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.
 
 Lean Pool uses one `public import LeanPool.<Project>.Imports` per project in

AGENTS.md

@@ -148,6 +148,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines

CLAUDE.md

@@ -148,6 +148,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines

CONTRIBUTING.md

@@ -49,6 +49,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines

lakefile.toml

@@ -9,6 +9,10 @@ pp.unicode.fun = true # pretty-prints `fun a ↦ b`
 relaxedAutoImplicit = false
 weak.linter.mathlibStandardSet = true
 maxSynthPendingDepth = 3
+# Every warning is a compile error, so local builds fail exactly like CI and a
+# cached build can never hide one. Pool files cannot override it: option changes
+# are banned by the quality gate.
+warningAsError = true
 
 [[require]]
 name = "TauCeti"