fix(proofs): move RTAJittered.lean imports above all comments#159
Merged
fix(proofs): move RTAJittered.lean imports above all comments#159
Conversation
The Lean compiler requires `import` statements to appear before any other top-level content (including doc-comment blocks `/- ... -/`). The original file from #148 had two stacked comment blocks (a `/-!` docstring then a `/- ... -/` overview) above the `import` lines, and Lean 4.29.0-rc6 rejects that with: error: Proofs/Scheduling/RTAJittered.lean:35:0: invalid 'import' command, it must be used in the beginning of the file Fix: merge the two blocks into a single `/-! ... -/` module docstring that sits *before* the imports — Lean treats the leading docstring as metadata, not as a top-level command, so imports following it are still "at the beginning". Same content, different framing. Discovered by the new Lean CI gate from #151 once Mathlib's precompiled cache lands fast enough to actually reach our in-tree files. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
1 task
avrabe
added a commit
that referenced
this pull request
Apr 26, 2026
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The new Lean CI gate from #151 surfaced a real syntax error in `proofs/Proofs/Scheduling/RTAJittered.lean` (landed in #148):
```
error: Proofs/Scheduling/RTAJittered.lean:35:0:
invalid 'import' command, it must be used in the beginning of the file
```
Lean 4.29.0-rc6 requires `import` to come before any other top-level content. The original file had a leading `/-!` docstring (OK) followed by a `/- ... -/` block comment (NOT OK), then the imports. Lean treats the second block as a top-level command, which makes the imports illegal.
Fix
Merged the two blocks into a single `/-! ... -/` module docstring placed before the imports. Lean's leading-docstring exception still holds, so imports remain "at the beginning".
Content unchanged — only the comment framing.
Why this slipped through
The Track A commit-3 agent (#148) couldn't run `lake build` locally (no Lean toolchain in sandbox). It explicitly flagged this risk in its report. The new `use-mathlib-cache: true` path on #151 pulls Mathlib in ~5 min instead of timing out at 60 min, finally letting CI reach our in-tree files.
Test plan
🤖 Generated with Claude Code