diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md
index 2ad6c96c8a..fffa6a4b13 100644
--- a/.github/CODE_QUALITY.md
+++ b/.github/CODE_QUALITY.md
@@ -11,12 +11,22 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for
 - `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
+- the `LeanPoolLinters` compiler plugin, loaded by Lake for every LeanPool module
 - `lake exe runLinter` on `LeanPool`
 - `lake exe lint-style` on `LeanPool`
 - `python -m lean_pool.quality --repo ..`
 
 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.
 
+The compiler plugin enforces the 200-line proof cap during the normal build, using original
+source syntax and elaborated types rather than a Python text heuristic. Both tactic and term
+proofs are checked, including proofs embedded in definitions, instances, and examples; tactic
+blocks constructing data are not proofs. Declaration headers and comment-only lines are
+excluded. Blank lines count, except inside block comments. Only the outermost overlong proof
+is reported when proof ranges overlap. The existing build-warning gate rejects these warnings.
+The plugin is build tooling under `scripts/ci/`, not a mathematical import of project modules.
+Its pinned-Lean regression test runs in all three compiled-artifact CI test steps.
+
 Lean Pool uses one `public import LeanPool.<Project>.Imports` per project in
 `LeanPool.lean`. Each generated `LeanPool/<Project>/Imports.lean` publicly imports
 the original project entry module and every source under that project, exactly
@@ -41,7 +51,6 @@ Current checks:
 - Lake configuration does not pass forbidden option overrides, trace options, linter disables, or heartbeat / recursion-depth overrides
 - the style-linter allowlist `scripts/nolints-style.txt` has no active entries
 - no Lean content file exceeds 10000 non-blank, non-comment code lines
-- no theorem/lemma proof body exceeds 200 non-blank, non-comment code lines, using the current text heuristic
 - `LeanPool/projects/` contains one valid YAML mapping per project, with its filename matching the unique slug; duplicate fields, nested cards, and mixed old/new registries fail validation
 - project entries have required fields: `slug`, `title`, `entry_module`, `authors`, `source`, `status`, `provenance`, `main_declarations`, and `tags`
 - project entries also carry documentation metadata: `summary`, `branch`, `main_results`, and `msc`
@@ -156,5 +165,4 @@ The following items are documented goals but are not fully implemented or enforc
 - controlled tag vocabulary for `LeanPool/projects/*.yaml`; tags are currently only checked as nonempty strings
 - generated domain/status indexes
 - directory index-file policy: every directory under `LeanPool/` containing Lean files should have an import-only index file with a module docstring
-- AST-aware proof-size measurement; the current 200-line proof cap uses a text heuristic
 - repository-wide slowest-proof reports and persisted performance trend artifacts
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 9911b4185a..fda102b82b 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -258,6 +258,7 @@ jobs:
         run: >-
           uv run --project python --group test pytest -q
           python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          python/tests/test_proof_length_linter.py
           -k 'test_lake_'
 
       - name: Install Mathlib cache
@@ -608,6 +609,7 @@ jobs:
         run: >-
           uv run --project python --group test pytest -q
           python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          python/tests/test_proof_length_linter.py
           -k 'test_lake_'
 
       - name: Install Mathlib cache
@@ -882,6 +884,7 @@ jobs:
         run: >-
           uv run --project python --group test pytest -q
           python/tests/test_ci_pr_build.py python/tests/test_indexes.py
+          python/tests/test_proof_length_linter.py
           -k 'test_lake_'
 
       - name: Install Mathlib cache
diff --git a/lakefile.toml b/lakefile.toml
index c128046ea4..76a686cd5f 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -24,6 +24,12 @@ rev = "v4.35.0-rc3"
 [[lean_lib]]
 name = "LeanPool"
 globs = ["LeanPool.*"]
+plugins = ["LeanPoolLinters:shared"]
+
+[[lean_lib]]
+name = "LeanPoolLinters"
+srcDir = "scripts/ci"
+roots = ["LeanPoolLinters"]
 
 [[lean_exe]]
 name = "mk_all"
diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py
index 7adf1cfdd9..eb73e9b4fe 100644
--- a/python/lean_pool/quality.py
+++ b/python/lean_pool/quality.py
@@ -371,38 +371,6 @@ def _declaration_starts(stripped: str) -> list[tuple[int, str]]:
     return starts
 
 
-def _check_proof_sizes(root: Path) -> list[_QualityError]:
-    errors: list[_QualityError] = []
-    for path in _lean_content_files(root):
-        original_lines = path.read_text().splitlines()
-        stripped = _strip_lean_comments("\n".join(original_lines))
-        starts = _declaration_starts(stripped)
-        for index, (start_line, _) in enumerate(starts):
-            end_line = (
-                starts[index + 1][0]
-                if index + 1 < len(starts)
-                else len(original_lines) + 1
-            )
-            block = original_lines[start_line - 1 : end_line - 1]
-            try:
-                body_start = next(
-                    offset for offset, line in enumerate(block) if ":=" in line
-                )
-            except StopIteration:
-                continue
-            body = "\n".join(block[body_start:])
-            proof_lines = _non_comment_code_lines(body)
-            if proof_lines > 200:
-                errors.append(
-                    _QualityError(
-                        path,
-                        start_line,
-                        f"proof has {proof_lines} code lines; limit is 200",
-                    )
-                )
-    return errors
-
-
 def _parse_declarations(root: Path) -> list[_Declaration]:
     return _declarations_in(_lean_content_files(root))
 
@@ -1490,7 +1458,6 @@ def run_checks(
         _check_lake_options,
         _check_style_nolints,
         _check_file_sizes,
-        _check_proof_sizes,
     ]
     errors = [error for check in checks for error in check(root)]
     errors.extend(
diff --git a/python/lean_pool/validation_cache.py b/python/lean_pool/validation_cache.py
index 6f838557a1..4c6dfb9c7d 100644
--- a/python/lean_pool/validation_cache.py
+++ b/python/lean_pool/validation_cache.py
@@ -22,6 +22,7 @@
     "lake-manifest.json",
     "lakefile.toml",
     "lakefile.lean",
+    "scripts/ci/LeanPoolLinters.lean",
     "python/lean_pool/validation_cache.py",
     "python/pyproject.toml",
     "python/uv.lock",
diff --git a/python/tests/test_proof_length_linter.py b/python/tests/test_proof_length_linter.py
new file mode 100644
index 0000000000..bd0b32fb77
--- /dev/null
+++ b/python/tests/test_proof_length_linter.py
@@ -0,0 +1,123 @@
+"""Exercise the proof-length plugin through Lake with the pinned Lean compiler."""
+
+from __future__ import annotations
+
+import os
+import runpy
+import shutil
+import subprocess
+import tomllib
+from pathlib import Path
+
+import pytest
+import yaml
+
+
+def _pinned_lake(root: Path) -> Path:
+    """Find the pinned Lake executable, failing in CI if it is unavailable."""
+    pin = (root / "lean-toolchain").read_text().strip()
+    lake = (
+        Path.home()
+        / ".elan/toolchains"
+        / pin.replace("/", "--").replace(":", "---")
+        / "bin/lake"
+    )
+    if not lake.is_file():
+        if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1":
+            pytest.fail("required pinned Lean toolchain unavailable")
+        pytest.skip("pinned Lean toolchain unavailable")
+    return lake
+
+
+def _write_test_project(root: Path, destination: Path) -> None:
+    """Create a dependency-free project that loads the plugin without imports."""
+    shutil.copyfile(root / "lean-toolchain", destination / "lean-toolchain")
+    (destination / "lakefile.toml").write_text(
+        'name = "proof_length_test"\n'
+        '[[lean_lib]]\nname = "LeanPoolLinters"\nsrcDir = "scripts/ci"\n'
+        '[[lean_lib]]\nname = "LeanPool"\n'
+        'roots = ["LeanPool", "DefaultBoundary"]\n'
+        'plugins = ["LeanPoolLinters:shared"]\n'
+    )
+    plugin = destination / "scripts/ci/LeanPoolLinters.lean"
+    plugin.parent.mkdir(parents=True)
+    shutil.copyfile(root / "scripts/ci/LeanPoolLinters.lean", plugin)
+    fixtures = (root / "scripts/ci/LeanPoolLintersTest.lean").read_text()
+    assert "import LeanPoolLinters" not in fixtures
+    # Also emit a real, unguarded warning so CI's ordinary warning gate can see it.
+    consumer = destination / "LeanPool.lean"
+    consumer.write_text(
+        fixtures + "\ntheorem unguardedLongProof : True := by\n"
+        "  skip\n  skip\n  exact True.intro\n"
+    )
+
+
+def _write_default_boundary_fixture(destination: Path) -> None:
+    """Generate proofs exactly at and one line above the production limit."""
+    # Exercise the actual production default, not just the fixtures' small bound.
+    # The guarded proof has 200 lines; its unguarded neighbour has 201.
+    (destination / "DefaultBoundary.lean").write_text(
+        "".join(
+            [
+                "module\nimport Lean.Elab.GuardMsgs\n\n#guard_msgs in\n",
+                "theorem exactlyAtDefaultLimit : True := by\n",
+                "  skip\n" * 198,
+                "  exact True.intro\n\n",
+                "theorem exceedingDefaultLimit : True := by\n",
+                "  skip\n" * 199,
+                "  exact True.intro\n",
+            ]
+        )
+    )
+
+
+def test_lake_proof_length_plugin(tmp_path: Path) -> None:
+    """Load the plugin without source imports and check its source-range fixtures."""
+    root = Path(__file__).resolve().parents[2]
+    lake = _pinned_lake(root)
+    configuration = tomllib.loads((root / "lakefile.toml").read_text())
+    libraries = {library["name"]: library for library in configuration["lean_lib"]}
+    assert libraries["LeanPool"]["plugins"] == ["LeanPoolLinters:shared"]
+    assert libraries["LeanPoolLinters"]["srcDir"] == "scripts/ci"
+    _write_test_project(root, tmp_path)
+    _write_default_boundary_fixture(tmp_path)
+    result = subprocess.run(
+        [str(lake), "build", "LeanPool"],
+        cwd=tmp_path,
+        capture_output=True,
+        text=True,
+        timeout=180,
+    )
+    output = result.stdout + result.stderr
+    assert result.returncode == 0, output
+    assert "warning: LeanPool.lean:" in output, output
+    assert output.count("This proof contains 4 non-comment lines") == 1, output
+    assert "exceeding the limit of 3" in output, output
+    assert output.count("This proof contains 201 non-comment lines") == 1, output
+    assert "exceeding the limit of 200" in output, output
+    assert "error:" not in output, output
+
+
+def test_proof_length_plugin_invalidates_build_shards() -> None:
+    """A plugin-only edit must rebuild all projects, not just reuse old results."""
+    root = Path(__file__).resolve().parents[2]
+    planner = runpy.run_path(str(root / "scripts/ci/plan-build-shards.py"))
+    assert "scripts/ci/LeanPoolLinters.lean" in planner["GLOBAL_BUILD_INPUTS"]
+
+
+def test_proof_length_plugin_has_pinned_ci_coverage() -> None:
+    """Run the fixture in Lean-equipped CI, rather than skipping it in Python CI."""
+    root = Path(__file__).resolve().parents[2]
+    workflow = yaml.safe_load(
+        (root / ".github/workflows/lean_action_ci.yml").read_text()
+    )
+    steps = [
+        step
+        for job in workflow["jobs"].values()
+        for step in job.get("steps", [])
+        if "python/tests/test_proof_length_linter.py" in step.get("run", "")
+    ]
+    assert len(steps) == 3
+    for step in steps:
+        assert step["env"]["LEAN_POOL_REQUIRE_TEST_TOOLCHAIN"] == "1"
+        assert "-k 'test_lake_'" in step["run"]
diff --git a/scripts/ci/LeanPoolLinters.lean b/scripts/ci/LeanPoolLinters.lean
new file mode 100644
index 0000000000..16bff8ae56
--- /dev/null
+++ b/scripts/ci/LeanPoolLinters.lean
@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2026 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+
+module
+
+public meta import Lean.Elab.Command
+meta import Lean.Elab.InfoTree.Util
+meta import Lean.Linter.Basic
+public import Lean.Linter.Init
+
+/-!
+# A linter for long proofs
+
+Load this module as a compiler plugin to enable `linter.longProof`. It warns when a proof term
+contains more than 200 non-comment source lines. The bound is configurable with
+`linter.longProof.maxLines`.
+
+Length is the inclusive span from the proof's first token (usually `by`) to its last token.
+Lines consisting entirely of comments are excluded. Blank lines still count, except inside block
+comments. Declaration headers and trailing comments do not count.
+Both tactic and term proofs are checked, including proofs in definitions, instances and examples.
+Elaborated types distinguish proofs from computations returning data.
+
+Only original source terms are checked. Nested overlong proofs produce a single warning on the
+outermost overlong proof, rather than repeated warnings on its subproofs. Like other info-tree
+linters, this requires elaboration information to be enabled. Commands with errors are skipped.
+-/
+
+meta section
+
+/-- Enable warnings for proofs exceeding the non-comment source-line limit. -/
+public register_option linter.longProof : Bool := {
+  defValue := true
+  descr := "warn when a proof exceeds the source-line limit"
+}
+
+/-- Maximum number of non-comment source lines allowed in a proof. -/
+public register_option linter.longProof.maxLines : Nat := {
+  defValue := 200
+  descr := "maximum number of non-comment source lines in a proof"
+}
+
+namespace LeanPool.CI.Linter
+
+open Lean Elab Command
+
+/-- Update the nesting depth of block comments after scanning one line of token trivia.
+
+The input must consist only of whitespace and comments, as supplied by a token's leading or
+trailing source slice. Comment markers inside strings and quoted identifiers therefore never
+reach this scanner. -/
+private def commentDepthAfter (depth : Nat) : List Char → Nat
+  | '/' :: '-' :: cs => commentDepthAfter (depth + 1) cs
+  | '-' :: '/' :: cs => commentDepthAfter (depth - 1) cs
+  -- Outside a block comment, `--` consumes the rest of the line. Inside one, consume only
+  -- the first hyphen so that `--/` still closes the block at its second hyphen.
+  | '-' :: '-' :: cs => if depth == 0 then 0 else commentDepthAfter depth ('-' :: cs)
+  | _ :: cs => commentDepthAfter depth cs
+  | [] => depth
+
+/-- Add the source lines containing comments in a leading or trailing token slice to `lines`.
+Blank lines inside block comments are included; blank lines between comments are not. -/
+private def addCommentLines (fileMap : FileMap) (str : Substring.Raw)
+    (lines : Std.HashSet Nat) : Std.HashSet Nat := Id.run do
+  let mut lines := lines
+  let mut depth := 0
+  let mut lineNumber := (fileMap.toPosition str.startPos).line
+  for line in str.toString.splitOn "\n" do
+    -- Every non-whitespace character in this slice belongs to a comment. A line that begins
+    -- inside a block comment also belongs to that comment, even if it contains only whitespace.
+    if depth > 0 || line.toList.any (!·.isWhitespace) then
+      lines := lines.insert lineNumber
+    depth := commentDepthAfter depth line.toList
+    lineNumber := lineNumber + 1
+  return lines
+
+/-- Add every source line touched by the half-open range `range` to `lines`. -/
+private def addSourceLines (fileMap : FileMap) (range : Syntax.Range)
+    (lines : Std.HashSet Nat) : Std.HashSet Nat := Id.run do
+  let first := (fileMap.toPosition range.start).line
+  let last := fileMap.toPosition range.stop
+  -- A range ending at the start of a line does not include that line.
+  let stop := last.line + if last.column == 0 then 0 else 1
+  let mut lines := lines
+  for line in [first:stop] do
+    lines := lines.insert line
+  return lines
+
+/-- Collect the lines containing original code tokens and comments in `stx`.
+
+The two sets may overlap: a line containing both code and a comment must still count toward
+the proof length. Multiline tokens, including string literals, contribute all their lines as code.
+-/
+private partial def sourceLines (fileMap : FileMap) (stx : Syntax)
+    (code comments : Std.HashSet Nat) : Std.HashSet Nat × Std.HashSet Nat := Id.run do
+  match stx with
+  | .node _ kind args =>
+    -- Documentation comments are syntax nodes rather than token trivia. Treat the whole node
+    -- as a comment instead of recursively classifying its contents as code.
+    if kind == ``Parser.Command.docComment || kind == ``Parser.Command.moduleDoc then
+      if let some range := stx.getRange? then
+        return (code, addSourceLines fileMap range comments)
+    let mut code := code
+    let mut comments := comments
+    for arg in args do
+      (code, comments) := sourceLines fileMap arg code comments
+    return (code, comments)
+  | .atom (.original leading pos trailing endPos) _
+  | .ident (.original leading pos trailing endPos) .. =>
+    return (addSourceLines fileMap ⟨pos, endPos⟩ code,
+      addCommentLines fileMap trailing (addCommentLines fileMap leading comments))
+  -- Synthetic and missing tokens do not describe code written in the source file.
+  | _ => return (code, comments)
+
+/-- Count the source lines touched by `range`, excluding those in `commentOnly`. -/
+private def proofLineCount (fileMap : FileMap) (commentOnly : Std.HashSet Nat)
+    (range : Syntax.Range) : Nat :=
+  let first := fileMap.toPosition range.start
+  let last := fileMap.toPosition range.stop
+  -- Source ranges have exclusive ends, so an end at column zero belongs to the preceding line.
+  let stop := last.line + if last.column == 0 then 0 else 1
+  stop - first.line - commentOnly.fold (fun n line ↦
+    if first.line ≤ line && line < stop then n + 1 else n) 0
+
+/-- Whether the half-open source range `inner` is contained in `outer`, including equality. -/
+private def containsRange (outer inner : Syntax.Range) : Bool :=
+  outer.start ≤ inner.start && inner.stop ≤ outer.stop
+
+/-- Find the outermost original proof ranges exceeding `limit` in an elaboration info tree.
+Proofs are identified by their elaborated types, so tactic blocks returning data are excluded. -/
+private def longProofs (tree : InfoTree) (fileMap : FileMap) (commentOnly : Std.HashSet Nat)
+    (limit : Nat) : CommandElabM (Array Syntax.Range) :=
+  tree.foldInfoM (init := #[]) fun context info ranges => do
+    let (stx, isProof) ← match info with
+      | .ofTermInfo term =>
+        -- A bound proof variable is not a proof body supplied by the author.
+        if term.isBinder then return ranges
+        pure (term.stx, context.runMetaM term.lctx (Meta.isProof term.expr))
+      | .ofTacticInfo tactic =>
+        -- Inspect a whole `by` block, rather than each individual tactic. Its initial goal
+        -- determines whether the block constructs a proof or data.
+        unless tactic.stx.isOfKind ``Parser.Term.byTactic do return ranges
+        let goal :: _ := tactic.goalsBefore | return ranges
+        -- Restore the goal's original metavariable and local contexts before checking its type.
+        let context := { context with mctx := tactic.mctxBefore }
+        pure (tactic.stx, context.runMetaM {} (goal.withContext (Meta.isProof (.mvar goal))))
+      | _ => return ranges
+    unless stx.getHeadInfo matches .original .. do return ranges
+    let some range := stx.getRange? | return ranges
+    -- Delay the semantic proof check until the cheaper source-length and containment tests pass.
+    unless proofLineCount fileMap commentOnly range > limit do return ranges
+    if ranges.any (containsRange · range) then return ranges
+    unless ← isProof do return ranges
+    -- Info-tree traversal can discover an enclosing proof after its subproofs. Replace those
+    -- smaller ranges, and also deduplicate identical ranges from different info nodes.
+    return (ranges.filter fun inner => !containsRange range inner).push range
+
+/-- Run the long-proof linter for a command, respecting command-local option overrides.
+Commands with errors or without elaboration information are skipped. -/
+private def checkLongProofs : Syntax → CommandElabM Unit := withSetOptionIn fun stx => do
+  unless Lean.Linter.getLinterValue linter.longProof (← Lean.Linter.getLinterOptions) do return
+  if (← get).messages.hasErrors || !(← getInfoState).enabled then return
+  let fileMap ← getFileMap
+  let limit := linter.longProof.maxLines.get (← getOptions)
+  let (code, comments) := sourceLines fileMap stx {} {}
+  -- Only lines with comments and no code are free; an inline comment does not exempt its line.
+  let commentOnly := comments.filter (!code.contains ·)
+  let mut ranges : Array Syntax.Range := #[]
+  -- A command can produce several info trees. Enforce the same outermost-range policy across
+  -- trees as within each tree, so that each long proof produces just one warning.
+  for tree in ← getInfoTrees do
+    for range in ← longProofs tree fileMap commentOnly limit do
+      unless ranges.any (containsRange · range) do
+        ranges := (ranges.filter fun inner => !containsRange range inner).push range
+  for range in ranges do
+    Lean.Linter.logLint linter.longProof (.ofRange range)
+      m!"This proof contains {proofLineCount fileMap commentOnly range} non-comment lines, \
+        exceeding the limit of {limit}. \
+        Consider extracting intermediate results into separate lemmas."
+
+-- Register the callback when this module is imported; its option controls whether it runs.
+initialize addLinter { name := `LeanPool.CI.Linter.longProof, run := checkLongProofs }
+
+end LeanPool.CI.Linter
diff --git a/scripts/ci/LeanPoolLintersTest.lean b/scripts/ci/LeanPoolLintersTest.lean
new file mode 100644
index 0000000000..3459e0aacf
--- /dev/null
+++ b/scripts/ci/LeanPoolLintersTest.lean
@@ -0,0 +1,245 @@
+/-
+Copyright (c) 2026 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+
+module
+
+import Lean.Elab.GuardMsgs
+
+/-! # Regression tests for the long-proof compiler plugin
+
+This file deliberately does not import the plugin. Lake must load it through the consumer
+library configuration. Small bounds keep the regression fixtures readable.
+-/
+
+-- Use a small bound to keep the boundary tests readable.
+set_option linter.longProof.maxLines 3
+
+-- Exactly the limit is permitted.
+#guard_msgs in
+example : True := by
+  skip
+  exact True.intro
+
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+theorem longProofTest : True := by
+  skip
+  skip
+  exact True.intro
+
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+theorem longLemmaTest : True := by
+  skip
+  skip
+  exact True.intro
+
+-- Term proofs are checked too; UTF-8 before the proof must not affect the positions.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example (_α : Type) : True :=
+  id (
+    id (
+      id (
+        True.intro)))
+
+-- The declaration header does not contribute to the proof length.
+#guard_msgs in
+example
+    (α : Type)
+    (_x : α)
+    (h : True) :
+    True := by
+  exact h
+
+-- A long tactic block constructing data is not a proof.
+#guard_msgs in
+example : Nat := by
+  skip
+  skip
+  exact 1
+
+-- Goal classification must use the goal's local context.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example (P : Prop) (h : P) : P := by
+  skip
+  skip
+  exact h
+
+-- Only the outer proof should be reported, even when a subproof is also too long.
+/--
+warning: This proof contains 6 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  have h : True := by
+    skip
+    skip
+    exact True.intro
+  exact h
+
+-- Proofs inside data-returning definitions are still checked.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+def longEmbeddedProofTest : {n : Nat // n = 0} := ⟨0, by
+  skip
+  skip
+  rfl⟩
+
+-- Comment-only lines do not count, but blank lines outside comments still count.
+#guard_msgs in
+example : True := by
+  -- This comment is free.
+
+  exact True.intro
+
+-- Nested block comments, including blank lines inside them, do not count.
+#guard_msgs in
+example : True := by
+  /- Outer comment
+
+     /- Nested comment -/
+     -- These are still block-comment contents.
+  -/
+  skip
+  exact True.intro
+
+-- Code before or after a block comment still counts, as do lines with trailing comments.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by -- A trailing comment.
+  skip /- A block comment starting after code.
+    This line does not count.
+-/skip
+  exact True.intro
+
+-- A blank line between separate comments still counts.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  -- First comment.
+
+  -- Second comment.
+  skip
+  exact True.intro
+
+-- Comment markers in strings and quoted identifiers are code.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  let «/- identifier -/» := "-- /- string -/"
+  skip
+  exact True.intro
+
+#guard_msgs in
+example : True := by
+  exact True.intro
+-- Trailing comments do not count.
+-- Nor do blank lines after the last token.
+
+-- Command-local overrides must be respected.
+#guard_msgs in
+set_option linter.longProof false in
+example : True := by
+  skip
+  skip
+  exact True.intro
+
+#guard_msgs in
+set_option linter.longProof.maxLines 4 in
+example : True := by
+  skip
+  skip
+  exact True.intro
+
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  skip
+  skip
+  exact True.intro
+
+-- Documentation comments in term proofs are excluded too.
+#guard_msgs in
+example : True :=
+  let rec
+    /-- A local definition.
+        Its documentation is not proof code.
+    -/
+    x : Nat := 0
+  True.intro
+
+-- A line-comment marker cannot start a block comment.
+#guard_msgs in
+example : True := by
+  -- /- This does not open a block comment.
+
+  exact True.intro
+
+-- A closing block-comment marker can overlap a pair of hyphens.
+/--
+warning: This proof contains 4 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  /- A block comment ending with an extra hyphen. --/
+
+  skip
+  exact True.intro
+
+-- Lines of a multiline string remain code, even when they look like comments.
+/--
+warning: This proof contains 5 non-comment lines, exceeding the limit of 3. Consider extracting intermediate results into separate lemmas.
+
+Note: This linter can be disabled with `set_option linter.longProof false`
+-/
+#guard_msgs in
+example : True := by
+  let _ := "first line
+-- This is string content.
+/- This is also string content. -/"
+  exact True.intro
diff --git a/scripts/ci/plan-build-shards.py b/scripts/ci/plan-build-shards.py
index 53a54564c7..b6a337f284 100644
--- a/scripts/ci/plan-build-shards.py
+++ b/scripts/ci/plan-build-shards.py
@@ -42,7 +42,12 @@
 SHARD_MIN_PROJECTS = 4
 SHARD_MIN_FILES = 500
 # Changes to any of these invalidate the whole pool's build.
-GLOBAL_BUILD_INPUTS = {"lean-toolchain", "lake-manifest.json", "lakefile.toml"}
+GLOBAL_BUILD_INPUTS = {
+    "lean-toolchain",
+    "lake-manifest.json",
+    "lakefile.toml",
+    "scripts/ci/LeanPoolLinters.lean",
+}
 
 
 def project_weights() -> dict[str, int]:
@@ -120,7 +125,7 @@ def main() -> None:
         elif cold:
             reason = "no warm build cache"
         elif global_change:
-            reason = "toolchain/manifest/lakefile changed"
+            reason = "shared compiler or build inputs changed"
         else:
             reason = "no diff available for this event"
     else: