Skip to content

fix(proofs): use /- block comment for RTAJittered.lean (matches RTA.lean style)#165

Merged
avrabe merged 1 commit intomainfrom
fix/rtajittered-doc-style
Apr 26, 2026
Merged

fix(proofs): use /- block comment for RTAJittered.lean (matches RTA.lean style)#165
avrabe merged 1 commit intomainfrom
fix/rtajittered-doc-style

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Apr 25, 2026

Summary

The new Lean CI gate from #151 surfaced that `/-! ... -/` module-docstring before `import` is rejected by Lean 4.29.0-rc6 in this file's pattern, despite #159 having structurally moved imports above all comment blocks. The other working proof files (RTA.lean, RMBound.lean, EDF.lean) use `/- ... -/` regular block comments with closing `-/` on its own line — adopting that pattern resolves the rejection.

Format-only change. Comment body unchanged.

Test plan

🤖 Generated with Claude Code

Lean 4.29.0-rc6 rejects `import` after a `/-! ... -/` module-docstring
in this file's pattern, even though Mathlib uses module docstrings
throughout — likely an interaction with the closing `-/` being on the
same line as content text. The other working files in this directory
(RTA.lean, RMBound.lean, EDF.lean) all use a regular `/- ... -/`
block comment with the closing `-/` on its own line, so we match that
style.

#159 (the previous import-order fix) addressed the structural ordering
but introduced the `/-!` form. CI surfaced that in #151's first run
that actually reached our in-tree files via mathlib-cache.

Body unchanged. Format-only edit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@temper-pulseengine
Copy link
Copy Markdown

AI Code Review for PR #165

pulseengine/spar:fix/rtajittered-doc-style → pulseengine/spar:main

Summary

The PR changes the module-docstring comment block in RTAJittered.lean from a /! block comment to a regular block comment with closing -/. This change is intended to match the style used in other proof files, such as RTA.lean, RMBound.lean, and EDF.lean.

Potential Bugs or Issues

  1. Compatibility: The PR does not specify whether this change will break compatibility with existing Lean 4.29.0-rc6 installations that rely on the previous module-docstring format.
  2. Documentation Consistency: While the style is now consistent, it might be worth reviewing other files to ensure consistency across the project.

Security Concerns

There are no security concerns associated with this change as it only involves modifying comments and does not affect any logic or data processing in the file.

Suggestions for Improvement

  1. Documentation Update: Ensure that all relevant documentation is updated to reflect the new comment style.
  2. Testing: Conduct thorough testing to ensure that the PR does not introduce any unintended behavior or errors.
  3. Review by Maintainers: Have a second reviewer review the change to catch any potential issues that might have been missed.

Overall Assessment

The change is a straightforward format-only update and should be relatively safe to merge. However, it's important to ensure compatibility with existing installations and review other files for consistency.


This review was generated by a local AI model. It is advisory only and may contain inaccuracies.

Reviewed at f952d4c

@codecov
Copy link
Copy Markdown

codecov Bot commented Apr 26, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe avrabe merged commit 3bed345 into main Apr 26, 2026
14 checks passed
@avrabe avrabe deleted the fix/rtajittered-doc-style branch April 26, 2026 06:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant