Fix proof-length counter including unrelated declarations

.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

.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

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"

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(

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",

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"]