From 4f9c641e1eb82463ead862fa71c740059aec8f56 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Fri, 23 Oct 2026 18:55:18 +0200 Subject: [PATCH 1/5] Fix incorrect calculation of proof lengths --- python/lean_pool/exposition/source_text.py | 20 ++- python/lean_pool/quality.py | 106 +++++++++++--- python/tests/test_exposition_source_text.py | 21 +++ python/tests/test_quality.py | 154 ++++++++++++++++++++ 4 files changed, 272 insertions(+), 29 deletions(-) diff --git a/python/lean_pool/exposition/source_text.py b/python/lean_pool/exposition/source_text.py index e41a15cfd4..4854a42366 100644 --- a/python/lean_pool/exposition/source_text.py +++ b/python/lean_pool/exposition/source_text.py @@ -62,10 +62,14 @@ _WHERE_RE = re.compile(r"(? str: - """Return ``text`` with comments (and optionally strings) blanked. + """Return ``text`` with comments (and optionally string/character literals) blanked. Copied from ``scripts/proof-profile/statements.py``. Length and newline positions are preserved so indices computed on the result line up with @@ -94,6 +98,12 @@ def code_view(text: str, blank_strings: bool = True) -> str: state = block block_depth = 1 continue + if c == "'" and (i == 0 or not _ident_char(text[i - 1])): + if match := _CHAR_LITERAL_RE.match(text, i): + literal = match[0] + out.append(" " * len(literal) if blank_strings else literal) + i = match.end() + continue if c == '"': out.append(" " if blank_strings else '"') i += 1 @@ -126,7 +136,7 @@ def code_view(text: str, blank_strings: bool = True) -> str: else: # string literal if c == "\\": if blank_strings: - out.append(" " if i + 1 < n else " ") + out.extend("\n" if c == "\n" else " " for c in text[i : i + 2]) else: out.append(text[i : i + 2]) i += 2 @@ -222,11 +232,7 @@ def _find_boundary( while i < end: c = code[i] if depth == 0: - if code[i : i + 4] in ("let ", "let\n", "let\t") and not _ident_char( - code[i - 1] if i > start else " " - ): - pending_binders += 1 - elif code[i : i + 5] in ("have ", "have\n", "have\t") and not _ident_char( + if _TYPE_BINDER_RE.match(code, i, end) and not _ident_char( code[i - 1] if i > start else " " ): pending_binders += 1 diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 7adf1cfdd9..eba17fd5d0 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -13,6 +13,7 @@ import yaml +from lean_pool.exposition.source_text import _find_boundary, code_view from lean_pool.indexes import ( discovers_modules, project_modules, @@ -56,6 +57,43 @@ r"(?:@\[[^\n\]]+\]\s+)*" r"(?:(?:private|protected|noncomputable|scoped)\s+)*" ) +PROOF_COMMAND_KEYWORDS = ( + *DECLARATION_KEYWORDS, + "example", + "opaque", + "axiom", + "constant", + "namespace", + "section", + "end", + "open", + "export", + "variable", + "include", + "omit", + "attribute", + "initialize", + "builtin_initialize", + "syntax", + "macro", + "macro_rules", + "elab", + "elab_rules", + "notation", + "infix", + "infixl", + "infixr", + "prefix", + "postfix", + "declare_syntax_cat", + "register_option", + "register_builtin_option", + "universe", + "universes", + "set_option", + "mutual", +) + # A (possibly dotted) Lean identifier: a leading letter or `_`, then letters / # digits / `_` / `'` / `.`. `\w` and `\W` are Unicode-aware in Python 3, so # this matches names with subscripts or Greek letters (`c₀`, `α`) that an @@ -362,36 +400,60 @@ def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: return errors -def _declaration_starts(stripped: str) -> list[tuple[int, str]]: - starts: list[tuple[int, str]] = [] - pattern = re.compile(rf"^\s*{DECLARATION_PREFIX}(?:theorem|lemma)\b") - for index, line in enumerate(stripped.splitlines(), start=1): - if pattern.match(line): - starts.append((index, line)) +def _command_starts(code: str) -> list[tuple[int, int, int, str]]: + """Locate standard line-leading commands outside bracketed terms and quotations. + + Each entry is (line number, indentation, offset, keyword). This remains a + textual heuristic: indentation distinguishes outer commands from local + declarations in a theorem's `where` block. + """ + keywords = "|".join(PROOF_COMMAND_KEYWORDS) + prefix = ( + r"(?:@\[[^\n\]]+\]\s+)*" + r"(?:(?:public|private|protected|noncomputable|scoped|local|nonrec|unsafe|partial)\s+)*" + ) + pattern = re.compile(rf"^([ \t]*){prefix}({keywords})\b") + starts = [] + depth = offset = 0 + for number, line in enumerate(code.splitlines(keepends=True), start=1): + if depth == 0: + if match := pattern.match(line): + starts.append((number, len(match[1]), offset, match[2])) + elif re.match(r"\s*(?:@\[|#)", line): + indent = len(line) - len(line.lstrip()) + starts.append((number, indent, offset, "attribute")) + for character in line: + if character in "([{⟨⦃": + depth += 1 + elif character in ")]}⟩⦄": + depth = max(0, depth - 1) + offset += len(line) 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 + text = path.read_text() + code = code_view(text) + starts = _command_starts(code) + for index, (start_line, indent, start, keyword) in enumerate(starts): + if keyword not in ("theorem", "lemma"): + continue + end = next( + ( + offset + for _, column, offset, _ in starts[index + 1 :] + if column <= indent + ), + len(text), ) - 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: + body_start = _find_boundary(code, start, end) + if body_start == end: continue - body = "\n".join(block[body_start:]) - proof_lines = _non_comment_code_lines(body) + proof_lines = sum( + bool(line.strip()) for line in code[body_start:end].splitlines() + ) if proof_lines > 200: errors.append( _QualityError( diff --git a/python/tests/test_exposition_source_text.py b/python/tests/test_exposition_source_text.py index 44cbf42a7b..a93a5beaa6 100644 --- a/python/tests/test_exposition_source_text.py +++ b/python/tests/test_exposition_source_text.py @@ -4,6 +4,7 @@ from lean_pool.exposition.source_text import ( SourceFile, + code_view, module_skeleton, statement_slice, ) @@ -39,6 +40,26 @@ def _slice_full( return statement_slice(source, declaration_range, selection, fallback) +def test_code_view_preserves_string_gap_line_positions() -> None: + """Blanking escaped newlines must preserve both offsets and line numbers.""" + text = 'def s := "one\\\n two\\\n three"\ntheorem t : True := by trivial\n' + code = code_view(text) + assert len(code) == len(text) + assert [i for i, c in enumerate(code) if c == "\n"] == [ + i for i, c in enumerate(text) if c == "\n" + ] + assert code_view(text, blank_strings=False) == text + + +def test_code_view_masks_characters_without_eating_prime_names() -> None: + """Quotation and bracket characters in literals cannot affect lexical scanning.""" + text = "def x' := '('\ndef y' := '\"'\ndef z' := '\\\\'\n" + code = code_view(text) + assert len(code) == len(text) + assert code.splitlines() == ["def x' := ", "def y' := ", "def z' := "] + assert code_view(text, blank_strings=False) == text + + def test_theorem_with_assignment_boundary() -> None: """Doc comment, attribute, and modifier are skipped; body is cut at :=.""" kind, statement, statement_end = _slice_full(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16]) diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 494b696542..9ebfd9aeba 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -10,6 +10,7 @@ from lean_pool.quality import ( _axiom_audit_missing, _axiom_audit_resolved, + _check_proof_sizes, _Declaration, _parse_axiom_output, _parse_declarations, @@ -437,6 +438,159 @@ def test_quality_check_allows_extra_documented_main_results(tmp_path: Path) -> N ) +@pytest.mark.parametrize( + "following", + [ + "def later : True := by\n" + " skip\n" * 220 + " trivial\n", + "private noncomputable def later : True := by\n" + + " skip\n" * 220 + + " trivial\n", + "abbrev later : True := by\n" + " skip\n" * 220 + " trivial\n", + "scoped instance : Inhabited Nat := by\n" + " skip\n" * 220 + " exact ⟨0⟩\n", + "structure Later where\n" + "".join(f" field{i} : Nat\n" for i in range(220)), + "class Later where\n" + "".join(f" field{i} : Nat\n" for i in range(220)), + "inductive Later where\n" + + "".join(f" | constructor{i} : Later\n" for i in range(220)), + "namespace Later\n" + "variable (n : Nat)\n" * 220 + "end Later\n", + "attribute [local simp] tiny\n" * 220, + ], +) +def test_proof_size_excludes_following_commands(tmp_path: Path, following: str) -> None: + """An unrelated definition, instance or command is not part of a tiny proof.""" + _write_minimal_repo(tmp_path, "theorem tiny : True := by\n trivial\n" + following) + assert _check_proof_sizes(tmp_path) == [] + + +@pytest.mark.parametrize("lines", [199, 200]) +def test_proof_size_enforces_actual_body_limit(tmp_path: Path, lines: int) -> None: + """The assignment line counts, and unrelated following code does not.""" + _write_minimal_repo( + tmp_path, + "public theorem large : True := by\n" + + " skip\n" * (lines - 1) + + " trivial\n" + + "def later := 0\n", + ) + errors = _check_proof_sizes(tmp_path) + if lines == 199: + assert errors == [] + else: + assert len(errors) == 1 + assert errors[0].line == len(HEADER.splitlines()) + 2 + assert errors[0].message == "proof has 201 code lines; limit is 200" + + +@pytest.mark.parametrize("binder", ["let", "have", "letI", "haveI", "letI'"]) +def test_proof_size_ignores_local_binders_in_statement( + tmp_path: Path, binder: str +) -> None: + """A type-level local assignment is not the theorem's proof assignment.""" + _write_minimal_repo( + tmp_path, + f"theorem tiny : {binder} x := 0\n" + + "\n".join(" " + "/- padding -/ True ∧" for _ in range(220)) + + "\n True := by\n repeat constructor\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + +def test_proof_size_ignores_assignments_in_statement(tmp_path: Path) -> None: + """Binder defaults and comments do not start the proof body.""" + binders = "".join(f" (x{i} : Nat := 0)\n" for i in range(220)) + _write_minimal_repo( + tmp_path, + "theorem tiny\n-- := not the body\n" + + binders + + " : True := by\n trivial\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + +def test_proof_size_ignores_fake_commands_in_comments_and_strings( + tmp_path: Path, +) -> None: + """Command-looking lines in comments and multiline literals do not end a proof.""" + _write_minimal_repo( + tmp_path, + "theorem large : True := by\n" + + "/- outer /- nested -/\ndef fake := 0\n-/\n" + + ' let _ := "first line\ndef fake := 0\nlast line"\n' + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 203 code lines; limit is 200" + + +def test_proof_size_keeps_quoted_commands_in_body(tmp_path: Path) -> None: + """Bracketed syntax quotations do not introduce outer declaration boundaries.""" + _write_minimal_repo( + tmp_path, + "theorem large : True := by\n" + + " let _ := `(command|\ndef fake := 0\n)\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 205 code lines; limit is 200" + + +def test_proof_size_counts_where_helpers(tmp_path: Path) -> None: + """Local helpers remain part of the declaration rather than escaping its limit.""" + _write_minimal_repo( + tmp_path, + "theorem large : True := helper\nwhere\n helper : True := by\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 204 code lines; limit is 200" + + +def test_proof_size_excludes_following_attributes(tmp_path: Path) -> None: + """A following multiline attribute is outside the preceding proof.""" + _write_minimal_repo( + tmp_path, + "theorem tiny : True := by\n trivial\n@[\n" + + "simp,\n" * 220 + + "]\ntheorem next : True := by\n trivial\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + +def test_proof_size_reports_original_line_after_string_gaps(tmp_path: Path) -> None: + """String gaps before a theorem cannot shift its diagnostic location.""" + _write_minimal_repo( + tmp_path, + 'def s := "one\\\n two\\\n three"\n' + + "theorem large : True := by\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].line == len(HEADER.splitlines()) + 5 + + +def test_proof_size_ignores_brackets_and_quotes_in_character_literals( + tmp_path: Path, +) -> None: + """Character literals before a theorem do not hide its commands or proof.""" + _write_minimal_repo( + tmp_path, + "def opening := '('\ndef quote := '\"'\n" + + "theorem large : True := by\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + def test_quality_check_finds_prefixed_declarations(tmp_path: Path) -> None: """The axiom audit declaration parser handles common Lean prefixes.""" _write_minimal_repo( From 8e44219cf45ac4cea31cd8ef04e96aa29937ff60 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Fri, 23 Oct 2026 19:36:07 +0200 Subject: [PATCH 2/5] address review comments --- python/lean_pool/exposition/source_text.py | 16 +++- python/lean_pool/quality.py | 39 ++++----- python/tests/test_exposition_source_text.py | 9 ++ python/tests/test_quality.py | 95 ++++++++++++++++++++- 4 files changed, 136 insertions(+), 23 deletions(-) diff --git a/python/lean_pool/exposition/source_text.py b/python/lean_pool/exposition/source_text.py index 4854a42366..91b4582944 100644 --- a/python/lean_pool/exposition/source_text.py +++ b/python/lean_pool/exposition/source_text.py @@ -68,7 +68,9 @@ ) -def code_view(text: str, blank_strings: bool = True) -> str: +def code_view( + text: str, blank_strings: bool = True, *, mask_escaped_identifiers: bool = False +) -> str: """Return ``text`` with comments (and optionally string/character literals) blanked. Copied from ``scripts/proof-profile/statements.py``. Length and newline @@ -77,6 +79,8 @@ def code_view(text: str, blank_strings: bool = True) -> str: doc comments (``/-- -/``) and module docs (``/-! -/``). With ``blank_strings=False`` string literals keep their content (used when trimming trailing comments off a command without eating a final string). + With ``mask_escaped_identifiers=True``, escaped names become neutral identifier + characters, preserving code-line counts without affecting bracket/keyword scans. """ out: list[str] = [] i, n = 0, len(text) @@ -87,6 +91,16 @@ def code_view(text: str, blank_strings: bool = True) -> str: c = text[i] two = text[i : i + 2] if state == normal: + if c == "«": + end = text.find("»", i + 1) + end = n if end < 0 else end + 1 + literal = text[i:end] + if mask_escaped_identifiers: + out.extend("\n" if c == "\n" else "_" for c in literal) + else: + out.append(literal) + i = end + continue if two == "--": out.append(" ") i += 2 diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index eba17fd5d0..aba9cd58f7 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -400,28 +400,36 @@ def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: return errors -def _command_starts(code: str) -> list[tuple[int, int, int, str]]: +def _command_starts(code: str) -> list[tuple[int, int, str]]: """Locate standard line-leading commands outside bracketed terms and quotations. - Each entry is (line number, indentation, offset, keyword). This remains a - textual heuristic: indentation distinguishes outer commands from local - declarations in a theorem's `where` block. + Each entry is (line number, offset, keyword). Independent commands may + have different indentation. Local `where` helpers use declaration names + rather than command keywords, so they remain inside the enclosing proof. """ keywords = "|".join(PROOF_COMMAND_KEYWORDS) prefix = ( r"(?:@\[[^\n\]]+\]\s+)*" r"(?:(?:public|private|protected|noncomputable|scoped|local|nonrec|unsafe|partial)\s+)*" ) - pattern = re.compile(rf"^([ \t]*){prefix}({keywords})\b") + pattern = re.compile(rf"^[ \t]*{prefix}({keywords})\b") starts = [] depth = offset = 0 + attribute_start = None for number, line in enumerate(code.splitlines(keepends=True), start=1): if depth == 0: if match := pattern.match(line): - starts.append((number, len(match[1]), offset, match[2])) - elif re.match(r"\s*(?:@\[|#)", line): - indent = len(line) - len(line.lstrip()) - starts.append((number, indent, offset, "attribute")) + start = offset if attribute_start is None else attribute_start + starts.append((number, start, match[1])) + attribute_start = None + elif re.match(r"\s*@\[", line): + if attribute_start is None: + attribute_start = offset + elif re.match(r"\s*#", line): + starts.append((number, offset, "diagnostic")) + attribute_start = None + elif line.strip(): + attribute_start = None for character in line: if character in "([{⟨⦃": depth += 1 @@ -435,19 +443,12 @@ def _check_proof_sizes(root: Path) -> list[_QualityError]: errors: list[_QualityError] = [] for path in _lean_content_files(root): text = path.read_text() - code = code_view(text) + code = code_view(text, mask_escaped_identifiers=True) starts = _command_starts(code) - for index, (start_line, indent, start, keyword) in enumerate(starts): + for index, (start_line, start, keyword) in enumerate(starts): if keyword not in ("theorem", "lemma"): continue - end = next( - ( - offset - for _, column, offset, _ in starts[index + 1 :] - if column <= indent - ), - len(text), - ) + end = starts[index + 1][1] if index + 1 < len(starts) else len(text) body_start = _find_boundary(code, start, end) if body_start == end: continue diff --git a/python/tests/test_exposition_source_text.py b/python/tests/test_exposition_source_text.py index a93a5beaa6..83382ed8b2 100644 --- a/python/tests/test_exposition_source_text.py +++ b/python/tests/test_exposition_source_text.py @@ -60,6 +60,15 @@ def test_code_view_masks_characters_without_eating_prime_names() -> None: assert code_view(text, blank_strings=False) == text +def test_code_view_preserves_or_masks_escaped_identifiers() -> None: + """Escaped names are atomic even when they contain quotes or comment markers.""" + text = 'def «(/-"» := 0\ntheorem after : True := by trivial\n' + assert code_view(text) == text + masked = code_view(text, mask_escaped_identifiers=True) + assert len(masked) == len(text) + assert masked == "def ______ := 0\ntheorem after : True := by trivial\n" + + def test_theorem_with_assignment_boundary() -> None: """Doc comment, attribute, and modifier are skipped; body is cut at :=.""" kind, statement, statement_end = _slice_full(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16]) diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 9ebfd9aeba..10795c3bb4 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -480,6 +480,50 @@ def test_proof_size_enforces_actual_body_limit(tmp_path: Path, lines: int) -> No assert errors[0].message == "proof has 201 code lines; limit is 200" +@pytest.mark.parametrize("indent", [" ", " ", " "]) +def test_proof_size_separates_differently_indented_theorems( + tmp_path: Path, indent: str +) -> None: + """Independent short proofs do not merge merely because their columns differ.""" + _write_minimal_repo( + tmp_path, + "theorem first : True := by\n" + + " skip\n" * 100 + + " trivial\n" + + f"{indent}lemma second : True := by\n" + + f"{indent} skip\n" * 100 + + f"{indent} trivial\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + +def test_proof_size_checks_later_indented_theorem(tmp_path: Path) -> None: + """A later independently indented theorem must still be checked on its own.""" + _write_minimal_repo( + tmp_path, + "theorem first : True := by\n trivial\n" + + " theorem second : True := by\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].line == len(HEADER.splitlines()) + 4 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + +def test_proof_size_excludes_indented_definition(tmp_path: Path) -> None: + """Definitions also end a preceding proof regardless of their indentation.""" + _write_minimal_repo( + tmp_path, + "theorem first : True := by\n trivial\n" + + " def later : True := by\n" + + " skip\n" * 220 + + " trivial\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + @pytest.mark.parametrize("binder", ["let", "have", "letI", "haveI", "letI'"]) def test_proof_size_ignores_local_binders_in_statement( tmp_path: Path, binder: str @@ -537,17 +581,22 @@ def test_proof_size_keeps_quoted_commands_in_body(tmp_path: Path) -> None: assert errors[0].message == "proof has 205 code lines; limit is 200" -def test_proof_size_counts_where_helpers(tmp_path: Path) -> None: +@pytest.mark.parametrize("attribute", ["", " @[simp]\n", " @[\n simp\n ]\n"]) +def test_proof_size_counts_where_helpers(tmp_path: Path, attribute: str) -> None: """Local helpers remain part of the declaration rather than escaping its limit.""" _write_minimal_repo( tmp_path, - "theorem large : True := helper\nwhere\n helper : True := by\n" + "theorem large : True := helper\nwhere\n" + + attribute + + " helper : True := by\n" + " skip\n" * 200 + " trivial\n", ) errors = _check_proof_sizes(tmp_path) assert len(errors) == 1 - assert errors[0].message == "proof has 204 code lines; limit is 200" + assert errors[0].message == ( + f"proof has {204 + len(attribute.splitlines())} code lines; limit is 200" + ) def test_proof_size_excludes_following_attributes(tmp_path: Path) -> None: @@ -591,6 +640,46 @@ def test_proof_size_ignores_brackets_and_quotes_in_character_literals( assert errors[0].message == "proof has 202 code lines; limit is 200" +@pytest.mark.parametrize("identifier", ["(", ")", "[", "]", "where", '"/-[']) +def test_proof_size_ignores_syntax_in_escaped_identifiers( + tmp_path: Path, identifier: str +) -> None: + """Quoted names cannot change nesting or hide later oversized proofs.""" + _write_minimal_repo( + tmp_path, + f"def «{identifier}» := 0\n" + + "theorem large : True := by\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].line == len(HEADER.splitlines()) + 3 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + +def test_proof_size_handles_escaped_theorem_name(tmp_path: Path) -> None: + """An escaped theorem name is not mistaken for a statement/body boundary.""" + _write_minimal_repo( + tmp_path, + "theorem «where» : True := by\n" + " skip\n" * 200 + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + +def test_proof_size_counts_lines_containing_only_escaped_names(tmp_path: Path) -> None: + """Masking escaped identifiers must not remove nonblank lines from the count.""" + _write_minimal_repo( + tmp_path, + "theorem large : True := by\n" + " «skip»\n" * 200 + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + def test_quality_check_finds_prefixed_declarations(tmp_path: Path) -> None: """The axiom audit declaration parser handles common Lean prefixes.""" _write_minimal_repo( From 6c357741cb06d536abb1f6e60224de5248caa48f Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Fri, 23 Oct 2026 20:00:00 +0200 Subject: [PATCH 3/5] handle `open` inside proofs --- python/lean_pool/quality.py | 29 ++++++++++++- python/tests/test_quality.py | 79 ++++++++++++++++++++++++++++++++++++ 2 files changed, 106 insertions(+), 2 deletions(-) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index aba9cd58f7..a0fdec0c10 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -13,7 +13,7 @@ import yaml -from lean_pool.exposition.source_text import _find_boundary, code_view +from lean_pool.exposition.source_text import _find_boundary, _strip_prefixes, code_view from lean_pool.indexes import ( discovers_modules, project_modules, @@ -400,6 +400,31 @@ def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: return errors +def _resolve_open_scopes( + code: str, starts: list[tuple[int, int, str]], pattern: re.Pattern[str] +) -> list[tuple[int, int, str]]: + """Attach scoped opens to commands, but leave term/tactic opens inside proofs.""" + commands = [] + scope_start = None + for index, (line, start, keyword) in enumerate(starts): + prefix_start = start if scope_start is None else scope_start + scope_start = None + if keyword == "open": + end = starts[index + 1][1] if index + 1 < len(starts) else len(code) + position = _strip_prefixes(code, start, end) + if position == end: + scope_start = prefix_start + continue + match = pattern.match(code[position:end]) + if match is None: + # An `open ... in` followed by a term/tactic is part of the proof. + continue + line = _line_number(code, position) + keyword = match[1] + commands.append((line, prefix_start, keyword)) + return commands + + def _command_starts(code: str) -> list[tuple[int, int, str]]: """Locate standard line-leading commands outside bracketed terms and quotations. @@ -436,7 +461,7 @@ def _command_starts(code: str) -> list[tuple[int, int, str]]: elif character in ")]}⟩⦄": depth = max(0, depth - 1) offset += len(line) - return starts + return _resolve_open_scopes(code, starts, pattern) def _check_proof_sizes(root: Path) -> list[_QualityError]: diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 10795c3bb4..dd10c0ada7 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -512,6 +512,85 @@ def test_proof_size_checks_later_indented_theorem(tmp_path: Path) -> None: assert errors[0].message == "proof has 202 code lines; limit is 200" +@pytest.mark.parametrize( + "opening", + [ + " open Nat in\n", + " open scoped BigOperators in\n", + " open Nat in by\n", + " open Nat\n in\n", + " open Nat in open List in\n", + " open Nat in\n open List in\n", + ], +) +def test_proof_size_counts_proof_internal_scoped_opens( + tmp_path: Path, opening: str +) -> None: + """Term/tactic-level scoped opens cannot hide the remainder of a long proof.""" + _write_minimal_repo( + tmp_path, + "theorem large : True := by\n" + opening + " skip\n" * 200 + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == ( + f"proof has {202 + len(opening.splitlines())} code lines; limit is 200" + ) + + +@pytest.mark.parametrize( + "opening", + [ + "open Nat in\n", + " open Nat in ", + "open Nat\n in ", + "open Nat in open List in ", + "open Nat in\nopen List in\n", + "open Nat in @[simp]\n", + ], +) +def test_proof_size_attaches_scoped_opens_to_following_declarations( + tmp_path: Path, opening: str +) -> None: + """Outer scoped opens belong to the next theorem, not to the preceding proof.""" + _write_minimal_repo( + tmp_path, + "theorem first : True := by\n" + + " skip\n" * 198 + + " trivial\n" + + opening + + "theorem second : True := by\n trivial\n", + ) + assert _check_proof_sizes(tmp_path) == [] + + +def test_proof_size_checks_inline_open_scoped_theorem(tmp_path: Path) -> None: + """A theorem following `open ... in` on the same line is still checked.""" + _write_minimal_repo( + tmp_path, + "open Nat in theorem large : True := by\n" + " skip\n" * 200 + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].message == "proof has 202 code lines; limit is 200" + + +def test_proof_size_scoped_open_stops_before_next_command(tmp_path: Path) -> None: + """A later `in` inside a theorem must not turn a global open into a scope.""" + _write_minimal_repo( + tmp_path, + "theorem first : True := by\n trivial\nopen Nat\n" + + "theorem large : True := by\n" + + " let _ := (Id.run do for i in [0] do pure ())\n" + + " skip\n" * 200 + + " trivial\n", + ) + errors = _check_proof_sizes(tmp_path) + assert len(errors) == 1 + assert errors[0].line == len(HEADER.splitlines()) + 5 + assert errors[0].message == "proof has 203 code lines; limit is 200" + + def test_proof_size_excludes_indented_definition(tmp_path: Path) -> None: """Definitions also end a preceding proof regardless of their indentation.""" _write_minimal_repo( From 0dfa3edda78940253886863b8b91eed8ac91882e Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Wed, 28 Oct 2026 07:33:43 +0100 Subject: [PATCH 4/5] reimplement as Lean linter --- .github/CODE_QUALITY.md | 12 +- .github/workflows/lean_action_ci.yml | 3 + lakefile.toml | 6 + python/lean_pool/exposition/source_text.py | 36 +-- python/lean_pool/quality.py | 135 +------- python/lean_pool/validation_cache.py | 1 + python/tests/test_exposition_source_text.py | 30 -- python/tests/test_proof_length_linter.py | 107 +++++++ python/tests/test_quality.py | 322 -------------------- scripts/ci/LeanPoolLinters.lean | 187 ++++++++++++ scripts/ci/LeanPoolLintersTest.lean | 245 +++++++++++++++ scripts/ci/plan-build-shards.py | 9 +- 12 files changed, 581 insertions(+), 512 deletions(-) create mode 100644 python/tests/test_proof_length_linter.py create mode 100644 scripts/ci/LeanPoolLinters.lean create mode 100644 scripts/ci/LeanPoolLintersTest.lean 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..Imports` per project in `LeanPool.lean`. Each generated `LeanPool//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/exposition/source_text.py b/python/lean_pool/exposition/source_text.py index 91b4582944..e41a15cfd4 100644 --- a/python/lean_pool/exposition/source_text.py +++ b/python/lean_pool/exposition/source_text.py @@ -62,16 +62,10 @@ _WHERE_RE = re.compile(r"(? str: - """Return ``text`` with comments (and optionally string/character literals) blanked. +def code_view(text: str, blank_strings: bool = True) -> str: + """Return ``text`` with comments (and optionally strings) blanked. Copied from ``scripts/proof-profile/statements.py``. Length and newline positions are preserved so indices computed on the result line up with @@ -79,8 +73,6 @@ def code_view( doc comments (``/-- -/``) and module docs (``/-! -/``). With ``blank_strings=False`` string literals keep their content (used when trimming trailing comments off a command without eating a final string). - With ``mask_escaped_identifiers=True``, escaped names become neutral identifier - characters, preserving code-line counts without affecting bracket/keyword scans. """ out: list[str] = [] i, n = 0, len(text) @@ -91,16 +83,6 @@ def code_view( c = text[i] two = text[i : i + 2] if state == normal: - if c == "«": - end = text.find("»", i + 1) - end = n if end < 0 else end + 1 - literal = text[i:end] - if mask_escaped_identifiers: - out.extend("\n" if c == "\n" else "_" for c in literal) - else: - out.append(literal) - i = end - continue if two == "--": out.append(" ") i += 2 @@ -112,12 +94,6 @@ def code_view( state = block block_depth = 1 continue - if c == "'" and (i == 0 or not _ident_char(text[i - 1])): - if match := _CHAR_LITERAL_RE.match(text, i): - literal = match[0] - out.append(" " * len(literal) if blank_strings else literal) - i = match.end() - continue if c == '"': out.append(" " if blank_strings else '"') i += 1 @@ -150,7 +126,7 @@ def code_view( else: # string literal if c == "\\": if blank_strings: - out.extend("\n" if c == "\n" else " " for c in text[i : i + 2]) + out.append(" " if i + 1 < n else " ") else: out.append(text[i : i + 2]) i += 2 @@ -246,7 +222,11 @@ def _find_boundary( while i < end: c = code[i] if depth == 0: - if _TYPE_BINDER_RE.match(code, i, end) and not _ident_char( + if code[i : i + 4] in ("let ", "let\n", "let\t") and not _ident_char( + code[i - 1] if i > start else " " + ): + pending_binders += 1 + elif code[i : i + 5] in ("have ", "have\n", "have\t") and not _ident_char( code[i - 1] if i > start else " " ): pending_binders += 1 diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index a0fdec0c10..eb73e9b4fe 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -13,7 +13,6 @@ import yaml -from lean_pool.exposition.source_text import _find_boundary, _strip_prefixes, code_view from lean_pool.indexes import ( discovers_modules, project_modules, @@ -57,43 +56,6 @@ r"(?:@\[[^\n\]]+\]\s+)*" r"(?:(?:private|protected|noncomputable|scoped)\s+)*" ) -PROOF_COMMAND_KEYWORDS = ( - *DECLARATION_KEYWORDS, - "example", - "opaque", - "axiom", - "constant", - "namespace", - "section", - "end", - "open", - "export", - "variable", - "include", - "omit", - "attribute", - "initialize", - "builtin_initialize", - "syntax", - "macro", - "macro_rules", - "elab", - "elab_rules", - "notation", - "infix", - "infixl", - "infixr", - "prefix", - "postfix", - "declare_syntax_cat", - "register_option", - "register_builtin_option", - "universe", - "universes", - "set_option", - "mutual", -) - # A (possibly dotted) Lean identifier: a leading letter or `_`, then letters / # digits / `_` / `'` / `.`. `\w` and `\W` are Unicode-aware in Python 3, so # this matches names with subscripts or Greek letters (`c₀`, `α`) that an @@ -400,95 +362,13 @@ def _file_size_errors(paths: list[Path], limit: int) -> list[_QualityError]: return errors -def _resolve_open_scopes( - code: str, starts: list[tuple[int, int, str]], pattern: re.Pattern[str] -) -> list[tuple[int, int, str]]: - """Attach scoped opens to commands, but leave term/tactic opens inside proofs.""" - commands = [] - scope_start = None - for index, (line, start, keyword) in enumerate(starts): - prefix_start = start if scope_start is None else scope_start - scope_start = None - if keyword == "open": - end = starts[index + 1][1] if index + 1 < len(starts) else len(code) - position = _strip_prefixes(code, start, end) - if position == end: - scope_start = prefix_start - continue - match = pattern.match(code[position:end]) - if match is None: - # An `open ... in` followed by a term/tactic is part of the proof. - continue - line = _line_number(code, position) - keyword = match[1] - commands.append((line, prefix_start, keyword)) - return commands - - -def _command_starts(code: str) -> list[tuple[int, int, str]]: - """Locate standard line-leading commands outside bracketed terms and quotations. - - Each entry is (line number, offset, keyword). Independent commands may - have different indentation. Local `where` helpers use declaration names - rather than command keywords, so they remain inside the enclosing proof. - """ - keywords = "|".join(PROOF_COMMAND_KEYWORDS) - prefix = ( - r"(?:@\[[^\n\]]+\]\s+)*" - r"(?:(?:public|private|protected|noncomputable|scoped|local|nonrec|unsafe|partial)\s+)*" - ) - pattern = re.compile(rf"^[ \t]*{prefix}({keywords})\b") - starts = [] - depth = offset = 0 - attribute_start = None - for number, line in enumerate(code.splitlines(keepends=True), start=1): - if depth == 0: - if match := pattern.match(line): - start = offset if attribute_start is None else attribute_start - starts.append((number, start, match[1])) - attribute_start = None - elif re.match(r"\s*@\[", line): - if attribute_start is None: - attribute_start = offset - elif re.match(r"\s*#", line): - starts.append((number, offset, "diagnostic")) - attribute_start = None - elif line.strip(): - attribute_start = None - for character in line: - if character in "([{⟨⦃": - depth += 1 - elif character in ")]}⟩⦄": - depth = max(0, depth - 1) - offset += len(line) - return _resolve_open_scopes(code, starts, pattern) - - -def _check_proof_sizes(root: Path) -> list[_QualityError]: - errors: list[_QualityError] = [] - for path in _lean_content_files(root): - text = path.read_text() - code = code_view(text, mask_escaped_identifiers=True) - starts = _command_starts(code) - for index, (start_line, start, keyword) in enumerate(starts): - if keyword not in ("theorem", "lemma"): - continue - end = starts[index + 1][1] if index + 1 < len(starts) else len(text) - body_start = _find_boundary(code, start, end) - if body_start == end: - continue - proof_lines = sum( - bool(line.strip()) for line in code[body_start:end].splitlines() - ) - if proof_lines > 200: - errors.append( - _QualityError( - path, - start_line, - f"proof has {proof_lines} code lines; limit is 200", - ) - ) - return errors +def _declaration_starts(stripped: str) -> list[tuple[int, str]]: + starts: list[tuple[int, str]] = [] + pattern = re.compile(rf"^\s*{DECLARATION_PREFIX}(?:theorem|lemma)\b") + for index, line in enumerate(stripped.splitlines(), start=1): + if pattern.match(line): + starts.append((index, line)) + return starts def _parse_declarations(root: Path) -> list[_Declaration]: @@ -1578,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_exposition_source_text.py b/python/tests/test_exposition_source_text.py index 83382ed8b2..44cbf42a7b 100644 --- a/python/tests/test_exposition_source_text.py +++ b/python/tests/test_exposition_source_text.py @@ -4,7 +4,6 @@ from lean_pool.exposition.source_text import ( SourceFile, - code_view, module_skeleton, statement_slice, ) @@ -40,35 +39,6 @@ def _slice_full( return statement_slice(source, declaration_range, selection, fallback) -def test_code_view_preserves_string_gap_line_positions() -> None: - """Blanking escaped newlines must preserve both offsets and line numbers.""" - text = 'def s := "one\\\n two\\\n three"\ntheorem t : True := by trivial\n' - code = code_view(text) - assert len(code) == len(text) - assert [i for i, c in enumerate(code) if c == "\n"] == [ - i for i, c in enumerate(text) if c == "\n" - ] - assert code_view(text, blank_strings=False) == text - - -def test_code_view_masks_characters_without_eating_prime_names() -> None: - """Quotation and bracket characters in literals cannot affect lexical scanning.""" - text = "def x' := '('\ndef y' := '\"'\ndef z' := '\\\\'\n" - code = code_view(text) - assert len(code) == len(text) - assert code.splitlines() == ["def x' := ", "def y' := ", "def z' := "] - assert code_view(text, blank_strings=False) == text - - -def test_code_view_preserves_or_masks_escaped_identifiers() -> None: - """Escaped names are atomic even when they contain quotes or comment markers.""" - text = 'def «(/-"» := 0\ntheorem after : True := by trivial\n' - assert code_view(text) == text - masked = code_view(text, mask_escaped_identifiers=True) - assert len(masked) == len(text) - assert masked == "def ______ := 0\ntheorem after : True := by trivial\n" - - def test_theorem_with_assignment_boundary() -> None: """Doc comment, attribute, and modifier are skipped; body is cut at :=.""" kind, statement, statement_end = _slice_full(THEOREM_BLOCK, [1, 0, 5, 6], [3, 16]) diff --git a/python/tests/test_proof_length_linter.py b/python/tests/test_proof_length_linter.py new file mode 100644 index 0000000000..c4ef1bbdcf --- /dev/null +++ b/python/tests/test_proof_length_linter.py @@ -0,0 +1,107 @@ +"""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 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] + 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") + 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" + (tmp_path / "lean-toolchain").write_text(pin + "\n") + (tmp_path / "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 = tmp_path / "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 = tmp_path / "LeanPool.lean" + consumer.write_text( + fixtures + "\ntheorem unguardedLongProof : True := by\n" + " skip\n skip\n exact True.intro\n" + ) + # Exercise the actual production default, not just the fixtures' small bound. + # The guarded proof has 200 lines; its unguarded neighbour has 201. + (tmp_path / "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", + ] + ) + ) + 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/python/tests/test_quality.py b/python/tests/test_quality.py index dd10c0ada7..494b696542 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -10,7 +10,6 @@ from lean_pool.quality import ( _axiom_audit_missing, _axiom_audit_resolved, - _check_proof_sizes, _Declaration, _parse_axiom_output, _parse_declarations, @@ -438,327 +437,6 @@ def test_quality_check_allows_extra_documented_main_results(tmp_path: Path) -> N ) -@pytest.mark.parametrize( - "following", - [ - "def later : True := by\n" + " skip\n" * 220 + " trivial\n", - "private noncomputable def later : True := by\n" - + " skip\n" * 220 - + " trivial\n", - "abbrev later : True := by\n" + " skip\n" * 220 + " trivial\n", - "scoped instance : Inhabited Nat := by\n" + " skip\n" * 220 + " exact ⟨0⟩\n", - "structure Later where\n" + "".join(f" field{i} : Nat\n" for i in range(220)), - "class Later where\n" + "".join(f" field{i} : Nat\n" for i in range(220)), - "inductive Later where\n" - + "".join(f" | constructor{i} : Later\n" for i in range(220)), - "namespace Later\n" + "variable (n : Nat)\n" * 220 + "end Later\n", - "attribute [local simp] tiny\n" * 220, - ], -) -def test_proof_size_excludes_following_commands(tmp_path: Path, following: str) -> None: - """An unrelated definition, instance or command is not part of a tiny proof.""" - _write_minimal_repo(tmp_path, "theorem tiny : True := by\n trivial\n" + following) - assert _check_proof_sizes(tmp_path) == [] - - -@pytest.mark.parametrize("lines", [199, 200]) -def test_proof_size_enforces_actual_body_limit(tmp_path: Path, lines: int) -> None: - """The assignment line counts, and unrelated following code does not.""" - _write_minimal_repo( - tmp_path, - "public theorem large : True := by\n" - + " skip\n" * (lines - 1) - + " trivial\n" - + "def later := 0\n", - ) - errors = _check_proof_sizes(tmp_path) - if lines == 199: - assert errors == [] - else: - assert len(errors) == 1 - assert errors[0].line == len(HEADER.splitlines()) + 2 - assert errors[0].message == "proof has 201 code lines; limit is 200" - - -@pytest.mark.parametrize("indent", [" ", " ", " "]) -def test_proof_size_separates_differently_indented_theorems( - tmp_path: Path, indent: str -) -> None: - """Independent short proofs do not merge merely because their columns differ.""" - _write_minimal_repo( - tmp_path, - "theorem first : True := by\n" - + " skip\n" * 100 - + " trivial\n" - + f"{indent}lemma second : True := by\n" - + f"{indent} skip\n" * 100 - + f"{indent} trivial\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -def test_proof_size_checks_later_indented_theorem(tmp_path: Path) -> None: - """A later independently indented theorem must still be checked on its own.""" - _write_minimal_repo( - tmp_path, - "theorem first : True := by\n trivial\n" - + " theorem second : True := by\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].line == len(HEADER.splitlines()) + 4 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - -@pytest.mark.parametrize( - "opening", - [ - " open Nat in\n", - " open scoped BigOperators in\n", - " open Nat in by\n", - " open Nat\n in\n", - " open Nat in open List in\n", - " open Nat in\n open List in\n", - ], -) -def test_proof_size_counts_proof_internal_scoped_opens( - tmp_path: Path, opening: str -) -> None: - """Term/tactic-level scoped opens cannot hide the remainder of a long proof.""" - _write_minimal_repo( - tmp_path, - "theorem large : True := by\n" + opening + " skip\n" * 200 + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == ( - f"proof has {202 + len(opening.splitlines())} code lines; limit is 200" - ) - - -@pytest.mark.parametrize( - "opening", - [ - "open Nat in\n", - " open Nat in ", - "open Nat\n in ", - "open Nat in open List in ", - "open Nat in\nopen List in\n", - "open Nat in @[simp]\n", - ], -) -def test_proof_size_attaches_scoped_opens_to_following_declarations( - tmp_path: Path, opening: str -) -> None: - """Outer scoped opens belong to the next theorem, not to the preceding proof.""" - _write_minimal_repo( - tmp_path, - "theorem first : True := by\n" - + " skip\n" * 198 - + " trivial\n" - + opening - + "theorem second : True := by\n trivial\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -def test_proof_size_checks_inline_open_scoped_theorem(tmp_path: Path) -> None: - """A theorem following `open ... in` on the same line is still checked.""" - _write_minimal_repo( - tmp_path, - "open Nat in theorem large : True := by\n" + " skip\n" * 200 + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - -def test_proof_size_scoped_open_stops_before_next_command(tmp_path: Path) -> None: - """A later `in` inside a theorem must not turn a global open into a scope.""" - _write_minimal_repo( - tmp_path, - "theorem first : True := by\n trivial\nopen Nat\n" - + "theorem large : True := by\n" - + " let _ := (Id.run do for i in [0] do pure ())\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].line == len(HEADER.splitlines()) + 5 - assert errors[0].message == "proof has 203 code lines; limit is 200" - - -def test_proof_size_excludes_indented_definition(tmp_path: Path) -> None: - """Definitions also end a preceding proof regardless of their indentation.""" - _write_minimal_repo( - tmp_path, - "theorem first : True := by\n trivial\n" - + " def later : True := by\n" - + " skip\n" * 220 - + " trivial\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -@pytest.mark.parametrize("binder", ["let", "have", "letI", "haveI", "letI'"]) -def test_proof_size_ignores_local_binders_in_statement( - tmp_path: Path, binder: str -) -> None: - """A type-level local assignment is not the theorem's proof assignment.""" - _write_minimal_repo( - tmp_path, - f"theorem tiny : {binder} x := 0\n" - + "\n".join(" " + "/- padding -/ True ∧" for _ in range(220)) - + "\n True := by\n repeat constructor\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -def test_proof_size_ignores_assignments_in_statement(tmp_path: Path) -> None: - """Binder defaults and comments do not start the proof body.""" - binders = "".join(f" (x{i} : Nat := 0)\n" for i in range(220)) - _write_minimal_repo( - tmp_path, - "theorem tiny\n-- := not the body\n" - + binders - + " : True := by\n trivial\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -def test_proof_size_ignores_fake_commands_in_comments_and_strings( - tmp_path: Path, -) -> None: - """Command-looking lines in comments and multiline literals do not end a proof.""" - _write_minimal_repo( - tmp_path, - "theorem large : True := by\n" - + "/- outer /- nested -/\ndef fake := 0\n-/\n" - + ' let _ := "first line\ndef fake := 0\nlast line"\n' - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 203 code lines; limit is 200" - - -def test_proof_size_keeps_quoted_commands_in_body(tmp_path: Path) -> None: - """Bracketed syntax quotations do not introduce outer declaration boundaries.""" - _write_minimal_repo( - tmp_path, - "theorem large : True := by\n" - + " let _ := `(command|\ndef fake := 0\n)\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 205 code lines; limit is 200" - - -@pytest.mark.parametrize("attribute", ["", " @[simp]\n", " @[\n simp\n ]\n"]) -def test_proof_size_counts_where_helpers(tmp_path: Path, attribute: str) -> None: - """Local helpers remain part of the declaration rather than escaping its limit.""" - _write_minimal_repo( - tmp_path, - "theorem large : True := helper\nwhere\n" - + attribute - + " helper : True := by\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == ( - f"proof has {204 + len(attribute.splitlines())} code lines; limit is 200" - ) - - -def test_proof_size_excludes_following_attributes(tmp_path: Path) -> None: - """A following multiline attribute is outside the preceding proof.""" - _write_minimal_repo( - tmp_path, - "theorem tiny : True := by\n trivial\n@[\n" - + "simp,\n" * 220 - + "]\ntheorem next : True := by\n trivial\n", - ) - assert _check_proof_sizes(tmp_path) == [] - - -def test_proof_size_reports_original_line_after_string_gaps(tmp_path: Path) -> None: - """String gaps before a theorem cannot shift its diagnostic location.""" - _write_minimal_repo( - tmp_path, - 'def s := "one\\\n two\\\n three"\n' - + "theorem large : True := by\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].line == len(HEADER.splitlines()) + 5 - - -def test_proof_size_ignores_brackets_and_quotes_in_character_literals( - tmp_path: Path, -) -> None: - """Character literals before a theorem do not hide its commands or proof.""" - _write_minimal_repo( - tmp_path, - "def opening := '('\ndef quote := '\"'\n" - + "theorem large : True := by\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - -@pytest.mark.parametrize("identifier", ["(", ")", "[", "]", "where", '"/-[']) -def test_proof_size_ignores_syntax_in_escaped_identifiers( - tmp_path: Path, identifier: str -) -> None: - """Quoted names cannot change nesting or hide later oversized proofs.""" - _write_minimal_repo( - tmp_path, - f"def «{identifier}» := 0\n" - + "theorem large : True := by\n" - + " skip\n" * 200 - + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].line == len(HEADER.splitlines()) + 3 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - -def test_proof_size_handles_escaped_theorem_name(tmp_path: Path) -> None: - """An escaped theorem name is not mistaken for a statement/body boundary.""" - _write_minimal_repo( - tmp_path, - "theorem «where» : True := by\n" + " skip\n" * 200 + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - -def test_proof_size_counts_lines_containing_only_escaped_names(tmp_path: Path) -> None: - """Masking escaped identifiers must not remove nonblank lines from the count.""" - _write_minimal_repo( - tmp_path, - "theorem large : True := by\n" + " «skip»\n" * 200 + " trivial\n", - ) - errors = _check_proof_sizes(tmp_path) - assert len(errors) == 1 - assert errors[0].message == "proof has 202 code lines; limit is 200" - - def test_quality_check_finds_prefixed_declarations(tmp_path: Path) -> None: """The axiom audit declaration parser handles common Lean prefixes.""" _write_minimal_repo( 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: From 4cf748ef8998b66e6ec6368aacc7eb5189cdda10 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Wed, 28 Oct 2026 08:00:34 +0100 Subject: [PATCH 5/5] avoid long functions in long proof test --- python/tests/test_proof_length_linter.py | 40 +++++++++++++++++------- 1 file changed, 28 insertions(+), 12 deletions(-) diff --git a/python/tests/test_proof_length_linter.py b/python/tests/test_proof_length_linter.py index c4ef1bbdcf..bd0b32fb77 100644 --- a/python/tests/test_proof_length_linter.py +++ b/python/tests/test_proof_length_linter.py @@ -13,9 +13,8 @@ import yaml -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] +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() @@ -27,32 +26,37 @@ def test_lake_proof_length_plugin(tmp_path: Path) -> None: if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1": pytest.fail("required pinned Lean toolchain unavailable") pytest.skip("pinned Lean toolchain unavailable") - 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" - (tmp_path / "lean-toolchain").write_text(pin + "\n") - (tmp_path / "lakefile.toml").write_text( + 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 = tmp_path / "scripts/ci/LeanPoolLinters.lean" + 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 = tmp_path / "LeanPool.lean" + 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. - (tmp_path / "DefaultBoundary.lean").write_text( + (destination / "DefaultBoundary.lean").write_text( "".join( [ "module\nimport Lean.Elab.GuardMsgs\n\n#guard_msgs in\n", @@ -65,6 +69,18 @@ def test_lake_proof_length_plugin(tmp_path: Path) -> None: ] ) ) + + +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,