neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

docs: correct the non-adopter attribution and two stale anchors 

Round 6. Documentation only; no code, no protocol change.

1. **The four-writer table mapped the wrong buffers to `ensure_slot`.**
   Verified at the call sites: `ensure_slot` has exactly two callers,
   `*compilation*` (`compile.lua:1090`) and `*shell-command*` (`:1125`).
   `*search-results*` is an **independent panel** in
   `builtin/commands/default.lua` with its own intercept (`:869`),
   round-trip mark and writes; `compile.lua` declares its name only to
   answer a predicate (`:216`), which is what made it look like a third
   slot. Round 5 fixed an undercount and introduced a misattribution in
   the same paragraph — the count was right, the mechanism was not.

   The table is now keyed by **writer**, not by buffer, so the mapping
   cannot silently drift again: four mechanisms, five buffers. It carries
   an explicit "do not read `ensure_slot` as covering the search panel"
   note, because that is the specific wrong inference.

   Corrected identically in `COHERENCE.md` §14 and the framing's
   deferred-lane text, which both carried the error.

   The scope claim is narrowed with it. "Every generated buffer outside
   copy mode" was too wide: `*workers*`, `*help*` and `*buffer-list*` are
   generated but do not use this idiom, and the REPL package's intercept
   (`packages/repl/init.lua:187`) is an op-filtering editing policy
   rather than a read-only panel. The claim is now "every remaining
   intercept-protected writer", and the two excluded groups are named so
   the next reader does not have to re-derive the boundary.

2. **The recovery floor contradicted itself.** The canonical-base line
   said the check accepts `a27f646` or anything newer while the check
   below required `74301d1`. The floor genuinely advanced; the prose now
   says so outright — a tree at `a27f646` no longer passes — and states
   why the floor must move with the base rather than trailing it.

3. **Two anchors survived the integration.** Lean 4 Stage 4a said it was
   part of "the `fe8b8ba` anchor above" when the anchor had become
   `74301d1`; it now refers to the anchor rather than restating a commit,
   which is what let it go stale. And #168's closed entry called its own
   `fe8b8ba` figure "the live figure" — it is a reading taken at
   `1b6a084`, kept as history, and now says so and points at the
   coverage lane as the single authority with an explicit "do not quote
   this one forward".

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
This commit is contained in:
Levi Neuwirth 2026-07-26 16:45:12 -04:00
parent d14fe4c4b9
commit d2ab3761c7
4 changed files with 59 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
COHERENCE.md
View File

@ -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`

15
docs/active-work.md
View File

@ -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 <their base>..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.

37
docs/agent-handoff.md
View File

@ -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

23
docs/terminal-config-and-copy-mode-framing.md
View File

@ -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