docs(formal): remove the duplicated Set Printing Width comment (9 modules) - #205
Conversation
…ules) #202 landed the same three-line explanatory comment twice in every module — once above `Set Printing Width 400.` where it belongs, and once orphaned immediately below it. My fault: I ran the insertion, then deleted only the `Set Printing Width 400.` line to A/B-test whether the ~78-column wrap was actually hiding any axiom from the guard, then re-ran the insertion. The sed that undid the test matched only the directive, not its comment, so the second pass stacked a fresh copy on top of the leftover. Comment-only; no directive, no proof and no guard changes. `formal/Justfile` is untouched. To be accurate about scope, since the obvious worry is that a text edit near the imports clipped something: it did not. `Import ListNotations.` and every `Require Import` are intact in all nine modules — verified before and after. (A *different* cleanup attempt of mine did briefly eat that import by skipping a fixed three lines past the marker, which in `Planner.v` overran the comment. That version was reset and never committed; it is mentioned only so the next person knows the offset-based approach is the wrong tool here. This commit removes the second matched block specifically, keyed on occurrence count.) Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub coqc -> exit 127, so the gate from #202 still fails when it should; `Normalizer.out` still prints at 157 columns, so the wrap fix is unaffected; `reuse lint` compliant.
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedRemoves duplicated three-line explanatory comments below Set Printing Width directives across nine formal modules. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
1 participant
docs(formal): remove the duplicated Set Printing Width comment (9 modules)
#202 landed the same three-line explanatory comment twice in every module —
once above
Set Printing Width 400.where it belongs, and once orphanedimmediately below it. My fault: I ran the insertion, then deleted only the
Set Printing Width 400.line to A/B-test whether the ~78-column wrap wasactually hiding any axiom from the guard, then re-ran the insertion. The sed
that undid the test matched only the directive, not its comment, so the second
pass stacked a fresh copy on top of the leftover.
Comment-only; no directive, no proof and no guard changes.
formal/Justfileis untouched.
To be accurate about scope, since the obvious worry is that a text edit near
the imports clipped something: it did not.
Import ListNotations.and everyRequire Importare intact in all nine modules — verified before and after.(A different cleanup attempt of mine did briefly eat that import by skipping
a fixed three lines past the marker, which in
Planner.voverran the comment.That version was reset and never committed; it is mentioned only so the next
person knows the offset-based approach is the wrong tool here. This commit
removes the second matched block specifically, keyed on occurrence count.)
Verified: real coqc 8.20.1 ->
check-assumptionsexits 0, 9/9 OK; stub coqc-> exit 127, so the gate from #202 still fails when it should;
Normalizer.outstill prints at 157 columns, so the wrap fix is unaffected;
reuse lintcompliant.