Repository navigation
dev: refinement on rendering performance and docs - #20
Merged
Merged
Conversation
`Render::write_str_all` sliced the string at whatever byte count a sink returned, so a count that split a character panicked, and a sink reporting `Ok(0)` spun forever. Both are reachable from outside the crate: `Render` is public and `render_raw` accepts any implementor. - reject zero, oversized and off-boundary counts through the new `Render::write_fault`, which defaults to `fail_doc` - document the `write_str` contract; `IoWrite` now says why it overrides `write_str_all` with a byte-oriented `write_all`
A speculative branch kept rendering after a text had already landed past the width, although `Doc::Union` accepts a branch only on `Ok(true)` and throws the buffered output away otherwise. Nesting made the wasted work grow with the branch depth. Inside a branch (`union_depth > 0`) a failed branch is therefore abandoned at once: the union restores the column, the command stack and the suffix queue, so nothing after the failing text can change the result. Output is unchanged, which the whole suite covers. Measured on nested rejected branches (release, 100 renders): 2.3us -> 0.21us at depth 20, 7.2us -> 0.20us at depth 40 with 2000-byte branches.
The width guarantees, the union probing rule and two unenforced preconditions were only observable through the test suite. Writing them down makes the intended behavior reviewable, and gives the Lean spec something to state theorems against. - crate docs: what a render guarantees about width, and that text is never split, reordered or dropped - `union`/`partial_union`: which branch is measured, that the continuation is not, that both branches must spell the same content, and that a tail union is probed by its fallback - `align`: the alignment column includes weak padding a later break discards - `Doc::Fail`: rejected inside a union branch, but fatal when flushed from a line suffix - `fitting`/`suffix_start`: why consumed suffix entries must survive a speculative frame - tests pin the tail-union probe and the `align` column choice
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
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.
No description provided.