From 98e1f0f8e15000b2592755e7d9b5e88a906d8c05 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 18:36:55 -0400 Subject: [PATCH] fix(hygiene): accept the heartbeat reason where Mathlib's linter wants it Mathlib's linter.style.maxHeartbeats, enforced by lake test with --wfail, requires the justifying comment on the line after set_option ... in, while check_hygiene.py only looked at the preceding lines. A file could not satisfy both; #567 was ejected from the merge queue for following the linter. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/check_hygiene.py | 9 +++++++-- scripts/test_check_hygiene.py | 12 ++++++++++++ 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/scripts/check_hygiene.py b/scripts/check_hygiene.py index fca55669d..e121a5dd4 100755 --- a/scripts/check_hygiene.py +++ b/scripts/check_hygiene.py @@ -6,7 +6,8 @@ 2. No `sorry`, custom `axiom`, or `native_decide` in Complexity/, ComplexityTests/ or the dedicated abstract library. 3. Every `set_option maxHeartbeats` or `set_option maxRecDepth` has an explanatory comment - on the same line or within the preceding 3 lines. + on the same line, within the preceding 3 lines, or (for `set_option ... in`) on the next + line, where Mathlib's `linter.style.maxHeartbeats` expects it. Opt-in heuristic checks: 4. (`--check-simp`) Flag non-terminal bare `simp` tactics in `-- upstream: candidate` modules @@ -50,7 +51,11 @@ def is_candidate_module(text: str) -> bool: def has_nearby_comment(raw_lines: list[str], code_lines: list[str], idx_0based: int) -> bool: start = max(0, idx_0based - 3) - for j in range(start, idx_0based + 1): + end = idx_0based + 1 + # Mathlib's `linter.style.maxHeartbeats` wants the reason right after `set_option ... in`. + if code_lines[idx_0based].rstrip().endswith(" in") and idx_0based + 1 < len(code_lines): + end = idx_0based + 2 + for j in range(start, end): # If masking comments changed the line, a comment is present on line j. if raw_lines[j] != code_lines[j]: return True diff --git a/scripts/test_check_hygiene.py b/scripts/test_check_hygiene.py index d1f6f0e23..a7b9600bf 100644 --- a/scripts/test_check_hygiene.py +++ b/scripts/test_check_hygiene.py @@ -61,6 +61,18 @@ def test_unjustified_set_option_fails(self) -> None: self.assertEqual(len(errors), 1) self.assertIn("requires a justifying comment", errors[0]) + def test_set_option_justified_on_the_next_line_passes(self) -> None: + p = self.write( + "Complexity/MathlibStyleOption.lean", + "module\n" + "-- upstream: candidate\n\n" + "\n\n\n" + "set_option maxHeartbeats 400000 in\n" + "-- Mathlib's maxHeartbeats linter expects the reason on this line.\n" + "theorem demo : True := trivial\n", + ) + self.assertEqual(check_hygiene.check_file(p, root=self.root), []) + def test_forbidden_tokens_and_nonterminal_simp(self) -> None: p = self.write( "Complexity/BadProof.lean",