Skip to content

fix(hygiene): accept the heartbeat reason where Mathlib's linter wants it #586

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 23, 2026
Merged

fix(hygiene): accept the heartbeat reason where Mathlib's linter wants it #586

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 7 additions & 2 deletions scripts/check_hygiene.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
12 changes: 12 additions & 0 deletions scripts/test_check_hygiene.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
Loading