diff --git a/COHERENCE.md b/COHERENCE.md index 6aaad38..e2d0143 100644 --- a/COHERENCE.md +++ b/COHERENCE.md @@ -1222,20 +1222,23 @@ Primitive-by-primitive against the list above: `compile.lua`'s own comment admits ("command/menu undo stays dispatchable"). `Buffer::set_generated_contents` (write + discard history + assert `read_only`, in one authorized call) now fixes this - for the terminal snapshot; **four writers have not yet adopted it and - remain emptiable** — listview panels, `*compilation*`, - `*search-results*` (the same `ensure_slot` mechanism in `compile.lua`), - and dired buffers, all of which pair an erroring intercept with - `bypass_intercept` writes over a still-writable rope. **A second half of the same + for the terminal snapshot; **four writer mechanisms have not yet adopted + it and remain emptiable** — listview panels; `compile.lua`'s + `ensure_slot`, which serves `*compilation*` **and** `*shell-command*`; + the independent `*search-results*` panel in + `builtin/commands/default.lua`; and dired buffers. All pair an erroring + intercept with `bypass_intercept` writes over a still-writable rope. + (`*workers*`, `*help*` and `*buffer-list*` are generated but do not use + this idiom.) **A second half of the same caveat, found in round 3: a rope write is only half of an edit.** The owner-authorized write must be fanned out to the windows showing the buffer and queued for replica mirrors, or the displaying window keeps a line index describing the previous contents and the next paint indexes the new rope with stale ranges. Adoption is therefore not a - one-line swap — and the two `compile.lua` slots **append** rather than - replacing wholesale, so they need a streaming variant of the primitive - that does not exist yet. Listview and dired already write whole-buffer - replaces and are the cheap half. + one-line swap — and the three appending buffers (`*compilation*`, + `*shell-command*`, `*search-results*`) need a streaming variant of the + primitive that does not exist yet. Listview and dired already write + whole-buffer replaces and are the cheap half. - **Diagnostics collection** ✓ — `DiagnosticStore` + signs + unified `error.next` source. - **Transient selector** ✓ — the minibuffer (though its `source` diff --git a/docs/active-work.md b/docs/active-work.md index 503689f..a978db0 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -36,8 +36,12 @@ landed regardless of what a lane says. #158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159; - protocol v20). The previous snapshot named `a27f646`; the recovery - check below accepts it or anything newer. + protocol v20). The previous snapshot named `a27f646`, and **the + recovery floor has advanced past it**: the check below now requires + `74301d1` or newer, so a tree at `a27f646` no longer passes. That is + deliberate — the floor moves with the base, because a check that + accepts an older commit than the declared base passes on a tree the + rest of this file does not describe. **Lanes below that name an older base have not been re-based; derive their integration surface from `git diff ..main`.** - On the transfer source, `origin/main` named a release mirror at @@ -733,9 +737,10 @@ git worktree add --track \ Branch `gpu-terminal-input` and worktree `../pmacs-gui-term-input` retained. **Its landed-doc pair MERGED as #168** (`main` @ `1b6a084`, 2026-07-26): #166 recorded as landed, the CI `crdt`-coverage gap - measured (**264 tests dark workspace-wide**, 177 in the library — as - of `1b6a084`; the live figure is 273/185 at `fe8b8ba`, and the - coverage lane above is the authority), the + measured (**264 tests dark workspace-wide**, 177 in the library — a + reading taken at `1b6a084` and kept here only as history. **The CI + `crdt`-coverage lane above is the authority for the live figure**; + do not quote this one forward), the vterm audit corrected — "only 3 of 9 acceptances drive a real daemon" was optimistic; without the frontend binary the honest number is **2** — and the a37 findings folded into the coverage lane. diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index 7b1173f..f029192 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -157,7 +157,7 @@ commands, read `docs/active-work.md` immediately after this file. at the moment of the swap. - **Stage 4a (the typed-edit consumer chain) MERGED as #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev 8; it is part - of the `fe8b8ba` anchor above). It is substrate only: `builtin/runtime/typed_edit.lua` owns the + of the main anchor above). It is substrate only: `builtin/runtime/typed_edit.lua` owns the single `buffer.after-edit` subscriber and the single one-shot read, `pair.lua` becomes its first registered consumer, and `tests/auto_pair_acceptance.rs` is unchanged by zero lines @@ -1036,24 +1036,33 @@ it lives in loro's `UndoManager`. That has no `clear`, and needs none — a manager records only what happens after construction, so `CrdtState::clear_undo_history` rebinds a fresh one to the same doc. -**Not yet adopted — and the inventory is four call sites, not two.** -Every generated buffer outside copy mode still uses the older idiom: -an erroring intercept plus `set_round_trip_input`, written through -`bypass_intercept`, with the rope left writable. All of them are +**Not yet adopted — the inventory is four writer mechanisms covering +five buffers.** *Every remaining intercept-protected writer* uses the +older idiom: an erroring intercept plus `set_round_trip_input`, written +through `bypass_intercept`, with the rope left writable. All are emptiable by `M-x buffer.undo`: -| buffer | writer | shape | +| writer | buffers | shape | |---|---|---| -| listview panels | `builtin/runtime/listview.lua:60-61` | delete-all + insert | -| `*compilation*` | `builtin/runtime/compile.lua` (`ensure_slot`) | **append** per output batch | -| `*search-results*` | same `ensure_slot` mechanism in `compile.lua` | **append** per match batch | -| dired buffers | `builtin/runtime/dired.lua:371` | whole-buffer replace | +| `builtin/runtime/listview.lua:60-61` | every listview panel | delete-all + insert | +| `builtin/runtime/compile.lua` (`ensure_slot`) | `*compilation*`, `*shell-command*` | **append** per output batch | +| `builtin/commands/default.lua:869` | `*search-results*` | reset per query, then **append** per match batch | +| `builtin/runtime/dired.lua:371` | every dired buffer | whole-buffer replace | + +**Do not read `ensure_slot` as covering the search panel** — it serves +`*compilation*` and `*shell-command*` only (`compile.lua:1090,1125`). +`*search-results*` is an independent panel with its own intercept, +round-trip mark and writes, and `compile.lua` names it only in a +predicate. Nor is the scope "every generated buffer": `*workers*`, +`*help*` and `*buffer-list*` are generated too but do not use this +idiom, and the REPL package's intercept +(`builtin/packages/repl/init.lua:187`) is an op-filtering editing +policy, not a read-only panel — neither group belongs to this lane. Adoption is not a one-line swap. It inherits the fan-out obligation, and -the two `compile.lua` slots append rather than replacing wholesale, so -they need a **streaming variant** of the primitive; listview and dired -are already whole-buffer replaces and are the cheap half. Recorded in -`COHERENCE.md` §14. +the three appending buffers need a **streaming variant** of the +primitive; listview and dired already write whole-buffer replaces and +are the cheap half. Recorded in `COHERENCE.md` §14. **And it does not replace `set_round_trip_input`.** The protection is layered across two copies: rope-level `read_only` refuses the op at the diff --git a/docs/terminal-config-and-copy-mode-framing.md b/docs/terminal-config-and-copy-mode-framing.md index 574d58c..bd405ea 100644 --- a/docs/terminal-config-and-copy-mode-framing.md +++ b/docs/terminal-config-and-copy-mode-framing.md @@ -564,16 +564,21 @@ additive, on its own binding, and does not replace scroll-and-select. would replay, and it stops a periodically refreshed buffer accumulating rope clones that `read_only` guarantees nothing can ever pop. - **What remains of the lane — four writers, not two** (corrected in - review round 5, which found the inventory short): listview panels - (`listview.lua:60-61`), `*compilation*` and `*search-results*` (both - through `compile.lua`'s shared `ensure_slot`), and dired buffers - (`dired.lua:371`) all still rely on intercept-plus-round-trip over a - writable rope, and are all still emptiable by `M-x buffer.undo`. The + **What remains of the lane — four writer mechanisms over five + buffers**, not the two this section first named (round 5 found the + inventory short; round 6 found the corrected version misattributing + the search panel). Every remaining intercept-protected writer still + relies on intercept-plus-round-trip over a writable rope, and every one + is still emptiable by `M-x buffer.undo`: listview panels + (`listview.lua:60-61`); `compile.lua`'s `ensure_slot`, which serves + `*compilation*` and `*shell-command*` — **not** `*search-results*`, + which `compile.lua` names only in a predicate; the independent + `*search-results*` panel in `builtin/commands/default.lua:869`, with + its own intercept and writes; and dired buffers (`dired.lua:371`). The primitive they need now exists and is proven, so the remaining work is - adoption plus a streaming-friendly variant — the two `compile.lua` - slots append rather than replacing wholesale, while listview and dired - already write whole-buffer replaces and are the cheap half. + adoption plus a streaming-friendly variant — the three appending + buffers need it, while listview and dired already write whole-buffer + replaces and are the cheap half. **The CRDT half is closed too** (review round 3). Clearing the v0.1 stacks proves nothing in CRDT mode, where they are bypassed entirely and