From 8e2afafc664cb07dba1fcf06f7ea184eac57ce90 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 4 Nov 2026 22:26:06 -0800 Subject: [PATCH 1/3] Make every Lean warning a compile error Set `warningAsError = true` in the package's leanOptions, as Tau Ceti does. CI already rejected warnings by scanning the build log; this moves the rule into the compiler, so local `lake build` fails the same way and a cached build can no longer hide a warning (a warning now means no .olean). Pool files cannot opt out because `set_option` is banned by the quality gate. The log scan stays for warnings Lake itself prints. Co-Authored-By: Claude Opus 5.5 --- .github/CODE_QUALITY.md | 4 ++-- AGENTS.md | 2 ++ CLAUDE.md | 2 ++ CONTRIBUTING.md | 2 ++ lakefile.toml | 4 ++++ 5 files changed, 12 insertions(+), 2 deletions(-) diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index 2ad6c96c8a..99e0de7eac 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -9,8 +9,8 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for [`lean_action_ci.yml`](workflows/lean_action_ci.yml) currently runs: - `lake exe mk_all --module --check` (the pool and project indexes must use `module` and `public import`) -- `lake build LeanPool` -- a warning scan over the build log +- `lake build LeanPool`, with `warningAsError = true` in `lakefile.toml`, so every Lean warning is a compile error (locally too) +- a warning scan over the build log, for warnings Lake itself prints - `lake exe runLinter` on `LeanPool` - `lake exe lint-style` on `LeanPool` - `python -m lean_pool.quality --repo ..` diff --git a/AGENTS.md b/AGENTS.md index 3c2bf66ec8..2f18b3ee51 100644 --- a/AGENTS.md +++ b/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 diff --git a/CLAUDE.md b/CLAUDE.md index 3c2bf66ec8..2f18b3ee51 100644 --- a/CLAUDE.md +++ b/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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 1f2f7e212c..2cb4e6e4d0 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/lakefile.toml b/lakefile.toml index b1ca063e71..d393e4978b 100644 --- a/lakefile.toml +++ b/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: `set_option` +# is banned by the quality gate. +warningAsError = true [[require]] name = "TauCeti" From a5c83b04a269efa2d1e65aa7d419c3ed88e871e9 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 4 Nov 2026 22:32:12 -0800 Subject: [PATCH 2/3] Keep the banned option token out of the lakefile comment The lake-options quality check scans the raw lakefile text, comments included. Co-Authored-By: Claude Opus 5.5 --- lakefile.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.toml b/lakefile.toml index d393e4978b..c602afbc90 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,8 +10,8 @@ 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: `set_option` -# is banned by the quality gate. +# cached build can never hide one. Pool files cannot override it: option changes +# are banned by the quality gate. warningAsError = true [[require]] From 63a15b5b8dd7fe9753e30a408fce0c2210bea8b1 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Thu, 5 Nov 2026 21:01:21 -0800 Subject: [PATCH 3/3] Keep warning policy compatible with proof-length documentation --- .github/CODE_QUALITY.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index 99e0de7eac..dc83c7ac81 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -9,12 +9,16 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for [`lean_action_ci.yml`](workflows/lean_action_ci.yml) currently runs: - `lake exe mk_all --module --check` (the pool and project indexes must use `module` and `public import`) -- `lake build LeanPool`, with `warningAsError = true` in `lakefile.toml`, so every Lean warning is a compile error (locally too) -- a warning scan over the build log, for warnings Lake itself prints +- `lake build LeanPool` +- a warning scan over the build log - `lake exe runLinter` on `LeanPool` - `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..Imports` per project in