fix: measure Format.align at the column the renderer uses - #14693
Open
jcreinhold wants to merge 4 commits into
Open
fix: measure Format.align at the column the renderer uses#14693jcreinhold wants to merge 4 commits into
jcreinhold wants to merge 4 commits into
Conversation
jcreinhold
force-pushed
the
fix/pp-trailing-whitespace-sepByIndent
branch
from
August 5, 2026 19:08
d829102 to
4c8cc87
Compare
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
jcreinhold
force-pushed
the
fix/pp-trailing-whitespace-sepByIndent
branch
from
August 5, 2026 19:46
4c8cc87 to
1ec0b5f
Compare
…` arguments This PR fixes the pretty printer emitting a trailing space before a multi-tactic indented `tacticSeq` argument, as in `iterate 1␣` followed by an indented sequence, and the whitespace-only blank line produced when the separator broke at narrow widths. A multi-tactic `tacticSeq` begins with a forced `align` (a hard line break) emitted by `sepByIndent.formatter`. When a flattenable separator such as `ppSpace` precedes the sequence, the enclosing group could flatten the separator into a space even though the `align` then broke immediately, stranding the space at the end of the row. The renderer now tracks whether the current row is still fresh (no output since the last line break): a `line` immediately followed by a forced `align` that will break is broken instead of flattened, and an `align` already at its indentation level on a fresh row is a no-op rather than emitting a second, whitespace-only line.
jcreinhold
force-pushed
the
fix/pp-trailing-whitespace-sepByIndent
branch
from
August 5, 2026 21:23
1ec0b5f to
a48d2b5
Compare
`Format.align (force := true)` pads to the current indentation level when the column is before it, and breaks to it otherwise. `be`, which renders, and `spaceUptoLine`, which decides whether a group flattens, must agree on which one happens. They did not: `spaceUptoLine` measures in budget coordinates (`w = width - column`, `m = width - indent`), but its `align` case was written as though those were the column and the indentation level, so it computed the inverse of `be`'s test. `spaceUptoLine'` had the same encoding fail a second way, recomputing the indentation budget from the column a group started at after `w` had already advanced. Measure in the coordinates `be` compares instead, leaving one shared predicate, `alignPads`, for the question both parts ask. `fill` reserves the column for its separating space through a new `colOffset` argument to `pushGroup` rather than by shrinking `w`, which under column coordinates would also move the `merge` short-circuit bound. Two further disagreements between the lookahead and the renderer: extend `nextForcedAlign?` past groups, empty text, and unforced `align`s, and into the enclosing groups, since the next item to render is often the first item of one of those. And re-decide a group after every break that is not its own flattening decision -- a hard newline already did this, but a breaking `align` and a vetoed `line` did not, so the group could render a row it had never measured.
Five cases in `formatHardLineBreaks.lean` for the corrected measure: a
group flattening as soon as its flattened form fits, the column being
followed across work items rather than only within the first, a forced
`align` at the head of a group, and the two re-decision cases, which are
invisible except as a row wider than the target width.
The three regenerated expectations all join a line that the old measure
broke: `def foo : ... where`, `frobnicate {`, `let x := {`, `by try`, and
`. grind =>`.
jcreinhold
changed the title
tacticSeq argumentsInline `alignPads`. Once the measurer is in column coordinates its test is literally `be`'s, `col < indent`, so wrapping it in a predicate gained nothing -- the name had to be read to learn which way round "pads" was, and it turned `be`'s line into a diff hunk where inlining leaves it identical to master. The invariant it carried is now a comment at the measurer's `align` case, which is the site that was wrong. Shorten the docstrings added to the private helpers, which the rest of this file does not carry, and drop three test cases that discriminate against nothing: `formatTacticSeq`'s user-defined `myiter` syntax and its narrow-width repeat, both of which restate the `iterate` case one layer above a `Format` fix, and `formatHardLineBreaks`'s width-23 rendering, already bracketed by widths 10 and 22.
jcreinhold
added a commit
to jcreinhold/lean-fmt
that referenced
this pull request
Aug 12, 2026
`sepByIndent` opens each item's row with a forced `align` for the first and a `text "\n"` for the rest, then spells the item itself as `ppGroup`, whose leading soft `line` fits and flattens to a space. So every multi-item `where` body sat one column right of the column the list picked -- right of its own docstring, and right of where `docs/style.md` says it goes. Not an edge case: it is every `where` clause with more than one binding, in every project, at every width. This tree had four of them and `lake lint` called them clean. The column is `checkColGe`'s reference, so it is not only cosmetic. The fix is the mirror of `dropTrailingBreak`, which the file's own docstring recorded as tried and unsafe. The objection was measured and correct, and it was an objection to *half* the rule: the earlier attempt covered `text "\n"` only, so it fired on items 2..n and left item 1 a column to their right, moving the reference column away from the block. Covering `align force` too moves every item together. Safety is not empirical here -- `be`'s forced-align case is `if k < indent then pad (indent - k) else pushNewline indent`, so it emits at least one space or starts a row, and a break dropped behind either cannot join two tokens. `Mathlib/Util/Superscript.lean:312`, the file the recorded failure was measured on, reparses. It is a correction on the append rather than an entry in `boundaryStarts` because no boundary can reach the offending leaf: `constrainBoundary` applies a collected layout to the first boundary leaf at a terminal, which here is the `align`, and the break is the one behind it -- inside the `ppGroup`'s `nest 2`, where `.hard` would land the item at the nest's column rather than the list's. `native-layout`'s three-space assertion was the defect written down; it moves to two. `Families.lean` gains a two-item clause beside the one-item one, whose row-hugging is what makes the two-item column a claim about `sepByIndent`'s `align` rather than about `where` clauses generally. Also here, because it instructs the next maintainer to delete working code: the note scheduling the align-compensation collectors for removal at the 4.34 bump said leanprover/lean4#14693 landed there. It did not. `Init/Data/Format/ Basic.lean` and `Lean/Parser/Extra.lean` are byte-identical between v4.33.0 and the pinned v4.34.0-rc1, and the shattering reproduces on the pin. And `docs/style.md`'s flat `decl.signature` example, which only holds under `declaration-body = "same-line"` and contradicted the documented default.
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
2 participants
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.
This PR fixes the layout of
Format.align (force := true), whichsepByIndentemits before the first item of every newline-separated indented sequence, so it reaches tactic blocks,whereclauses, source-parsed structure instances,conv,grind, and the Lake DSL.A forced
alignpads to the current indentation level when the column is before it, and breaks to it otherwise. Two parts of the engine must agree on which one happens:be, which renders, andspaceUptoLine, which decides whether a group flattens. They did not.spaceUptoLinemeasures in budget coordinates (w = width - column,m = width - indent), but itsaligncase was written as though those were the column and the indentation level, so it computed the inverse ofbe's test and charged the width of a break as padding. A group whose flattened form is 10 columns wide was not flattened until width 23, anddef foo (a : Nat) : Packet whereputwhereon a line of its own at every width below 71 (#14715).spaceUptoLine'had the same encoding fail a second way, recomputing the indentation budget from the column a group started at afterwhad already advanced past it. Measuring in the coordinatesbecompares fixes both and leaves one shared predicate,alignPads, for the question the two parts ask.On top of that: a
lineflattened into a space immediately before a forcedalignnow breaks rather than stranding the space, and a forcedalignon a row that is still blank and already at its indentation level no longer emits an empty row (#14692); the lookahead that decides the first of those now also sees past groups, empty text, and unforcedaligns, and into the enclosing groups; and every break that is not a group's own flattening decision — a hard newline, a breakingalign, a vetoedline— re-decides that group from the column it actually reached, so a group can no longer render a row it never measured.Over 600 random
align-bearing documents at four widths, rows carrying trailing whitespace go from 559 to 0 and rows wider than the target from 92 to 1, with no rendering acquiring one. Over 400align-free documents at widths 0–30 the output is unchanged.Closes #14692, closes #14715.