Four findings, all real, and they rhyme in pairs. Two implementation
defects and two vacuous pins, all four tracing to one root: a name is
not an identity, and a context-free readout is not a state observation.
A foreign buffer carrying the snapshot's name was adopted and then
overwritten. `pmacs.buffer.create` accepts any caller-chosen name and
snapshot writes use bypass_intercept, so found-by-name adoption
clobbered user data — the reviewer reproduced "do not clobber" becoming
23 newlines. Now follows dired's F7 rule: ownership means "in copy
mode's own handle table", never "found by name", and a taken name yields
a `<2>` variant.
Snapshot identity was keyed by terminal NAME.
`TerminalManager::open` uniquifies only the derived name — an explicit
`name = ...` is inserted verbatim — so two valid terminals can share
one, and a name-keyed table handed them a single snapshot: the second
invocation retargeted it, `q` returned to the wrong terminal, and
killing either removed the shared buffer. Identity is now the terminal
buffer, compared in an array, because BufferIdLua implements `__eq` but
each wrapper is a distinct table key: comparison works, hashing does
not. The kill-with-terminal callback now closes over its own record
rather than looking the name up again.
The refresh pins were vacuous. Acceptance 19 compared a quiet
terminal's snapshot against itself and 18 counted buffers, so both
passed with render_snapshot replaced by a no-op. The child is
`exec cat`, so the tests now type a marker into the focused terminal,
require it ABSENT from the existing snapshot, and only then refresh —
via `g` and via re-invocation respectively.
The tail-follow pin could not observe view state.
`TerminalManager::snapshot(buffer_id)` is context-free and always
returns the live screen, so it reported "at the tail" even for a view
forced to the oldest retained row. Now read through
`snapshot_for_view`'s at_bottom and its projected cells.
Adds acceptance 18a (a foreign same-named buffer is never adopted or
clobbered) and 18b (two same-named terminals get two independent
snapshots, each `q` returns to its own source, and killing one leaves
the other's snapshot alive).
Four new bites, all discriminating: restoring adopt-by-name fails 18a
AND 18b; restoring name-keyed identity fails 18b; making
render_snapshot a no-op fails BOTH 18 and 19, which is the vacuity
demonstrated rather than argued; and forcing the view off the tail
fails 20.
Criterion 17 stays a named follow-up, per review agreement, until the
real GPU probe is non-skipping and CI-executed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
The 4a/4b split held; five P1s against rev 6's own content, all real,
all reproduced. Four share a root: rev 6 verified its external facts and
under-verified its internal ones.
1. Stage 4a's declared footprint excluded the tests its own acceptance
required. 46a-46e cannot live in tests/auto_pair_acceptance.rs,
which criterion 46 requires byte-identical. Footprint now names
tests/typed_edit_chain_acceptance.rs and gates on it.
2. Pending abbreviation state had the wrong owner. pmacs is
multi-frontend: EditorCore.views is per-FrontendId with its own
active window, take_typed_edit is already frontend-keyed, and
buffer.after-switch fires with no arguments — so a buffer-keyed
clear-on-switch lets any frontend discard another's pending
abbreviation. Now keyed (frontend, buffer) with a window check,
frontend-scoped clearing, a frontend.detached purge, and acceptance
45i, which the buffer-keyed design passes every other criterion
without.
3. The shortest-match rule was missing its tie-break: upstream keeps
declaration order among equal-length shortest keys, and 101 prefixes
have equal-shortest candidates resolving to different symbols (f
picks f< over f>). A pairs-iterated Lua map cannot express this, so
the vendored artifact is now an ordered sequence and resolution sorts
by (#key, source rank). Rev 6 missed this because it declared the
package ships no README after a 404 on the package root, with the
directory listing showing src/README.md already in hand — a 404 on a
guessed path is not evidence of absence, and the README states the
rule in one sentence.
4. The generator's rejection rule rejected the current table: \ is a key
and " begins eleven, while acceptance 45d requires \ to work.
Replaced with canonical lossless escaping; aborts only on duplicate
keys, invalid UTF-8, and a failed self-round-trip. 45g no longer
claims to diff against abbreviations.json, which is not shipped.
5. Durable and volatile state were not reconciled. agent-handoff.md
anchored main at d152120 with neither #167 nor #170 and no Lean arc
bullet at all; active-work.md kept 407 lines of merged Stage 1/2/3a/3b
history against its own instruction to prune merged entries, under a
stale snapshot date. Durable facts moved to the handoff; the ledger
keeps only the unlanded Stage 4 lane.
Also corrected: 119 multi-codepoint symbols (26 with $CURSOR), not 93;
three backslash values, not two; Q#LN22 now states the terminating-\
reprocess rule acceptance 45d depended on; acceptance 38 says the
terminator is retained, so undo restores "\alpha " with its space;
coherence cites golden-journey step 5, not step 4; and the
config-registry prior art points at Q#LN22.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
**P1-1 — the `Invalidated` arm published the panel context on the
document wire.** Real bug, and the live half of the routing defect: the
semantic peer has ONE statusline slot, so emitting an
authoritative-empty payload for every context replaced the document's
with the panel's. Now filtered by document-window identity exactly like
the `Ready` arm; a panel's own clear belongs to `PanelFrame` in 2B.
Pinned by `invalidated_statusline_clears_only_the_document_not_the_panel`,
which reproduces the reported shape — two targets instead of one — when
the filter is removed.
Honest note on the `Ready` arm: its identity selector is **defensive**,
not independently falsifiable today, because the document context is
captured first so "first context for my frontend" happens to pick it.
Rather than leave that as a silent dependency,
`the_semantic_fan_out_captures_the_document_first` pins the order and
says why it matters.
**P1-2 — round-1 finding 3 was not closed; four of my pins were
vacuous.** All four confirmed and fixed:
- The statusline consumer test discarded `render_frame`'s output. It now
observes the WIRE payload from a v18 peer with a registered provider,
and asserts non-emptiness so it cannot pass by emitting nothing.
- The terminal test compared two NON-terminal buffers, so both routings
answered `false`. The document window now holds a REAL terminal, so
the routes disagree; reverting `semantic_terminal_key` fails it.
- The decorations test used different buffers and an empty selection —
again the same answer either way. The panel now displays the declared
buffer with a non-empty selection while the document has none.
- #1/#3/#21 had no discriminating pin at all. Their only production
caller is `dispatcher_loop`, which no test can drive, so this extracts
three named seams the loop calls — `document_buffer_to_follow`,
`document_cursor_byte`, `peer_displays_buffer_as_document` — and pins
each.
Also newly pinned: #2 the lazy CRDT upgrade (the census's sharpest
case), #7 `Viewport` aligning WITHOUT taking focus, and #9 a focused
terminal panel not suppressing the document viewport.
**Every one of the nine pins was falsified by revert.** Two needed a
second attempt after the first bite came back green.
**P2-3 — stale docs.** `StatuslineEvaluationTarget::Semantic`'s
documentation described evaluating only the focused window; it now
describes the document-plus-side fan-out, the capture order, the
identity-selection requirement, and that `active` reports actual focus.
The ledger's Stage 2A entry is corrected to five commits, 2,014 CRDT
tests, and 16 acceptance tests.
Two clippy findings the refactor introduced were fixed:
`document_buffer_to_follow` is `crdt`-gated to match its only caller,
and the `CursorByte` guard collapses into one `if`.
Gates: fmt clean; workspace clippy clean; 1,832 default + 2,014 CRDT
library; Stage 2A 16; Stage 1 46; statusline 8; m11_5 2; GPU initial
target 14; terminal config 12; folding Stage 2 48; vterm 1/2 10 / 6;
M4 121; required GPU 202; `git diff --check` clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Stage 2 of docs/terminal-config-and-copy-mode-framing.md (rev 4,
approved). `M-x terminal.copy-mode`, or `C-t` in a terminal buffer —
physically `C-c C-t`, since every unescaped key goes to the child —
materializes the retained scrollback into an ordinary read-only,
path-less buffer, with `g` to re-snapshot and `q` to return.
No protocol change.
Materializing is the whole design. isearch, motion, selection and the
kill ring work with no new substrate because the snapshot is a rope, so
SearchStore and the existing match painting apply unchanged. And "keys
must not reach the child" dissolves structurally rather than being
guarded: the transport arm keys on is_terminal(buffer_id), and a
snapshot is not a terminal, so the arm never fires. The
dispatch-shadow count stays at six and describe-key keeps telling the
truth — asserted directly, since that is the observable difference
between the buffer-local idiom and a shadow.
One serializer, not two (Q#TC7). `copy_retained` builds a whole-range
selection and hands it to `copy_selection_bytes`; a second walk would
re-derive soft-wrap joining, wide-glyph continuation, cluster bytes and
per-row trailing-blank trimming, and the two would drift. Four unit
pins in view.rs assert exact bytes against the same projection fixtures
that pin the serializer itself.
Q#TC6a is implemented as two calls, and the second is the load-bearing
one: an intercept guards dispatch only, and no Lua binding sets
Buffer::read_only, so set_round_trip_input is what keeps a replica
frontend from applying optimistically and emitting an op that would
pass ensure_writable and mutate both sides. Acceptance 16 pins that
UNGATED, because CI never compiles the crdt feature.
Eight of nine criteria. Criterion 17's semantic-frontend end-to-end pin
is deliberately absent: the optimistic apply lives only in
pmacs-gpu/src/main.rs and the headless SemanticClient has no optimistic
path, so a faithful test needs the real GPU binary — the a37
foundation, which CI never compiles, silently returns ok when the
binary is unbuilt, and is load-sensitive. Both halves of the mechanism
are pinned ungated instead (16, and 16b for the hazard); the wire-level
half stays an explicit obligation of the CI crdt-coverage lane.
Substrate fact found while wiring lifecycle: TerminalManager::prune
REACTS to a buffer already gone from the registry rather than removing
one, so a child exiting leaves both the terminal and its snapshot
alive. That is why on_removed is a sound teardown hook, and why a
finished command's output stays readable.
Five bites, five different wrong implementations, each failing exactly
one test: removing set_round_trip_input fails acceptance 16 in the
DEFAULT configuration; a naive independent serializer fails all four
unit pins, with the diffs naming each drift mode; making re-invoke
create a fresh buffer fails 18; dropping the kill-with-terminal
teardown fails 18; removing the intercept fails 16b.
COHERENCE.md: §6 gains this as the worked example that a modal-looking
feature need not become a shadow; §11 records the scope="global"
deferral's second live case, making the argument for both registry
deferrals cumulative; §2 step 8 gains copy mode and keeps the
still-missing close command named.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against main
@ d400f30 produced six findings that change the plan and three that
confirm it. The pmacs-side facts were verified in a worktree at that
commit; the upstream facts by reading leanprover/vscode-lean4 @ 17d1d08.
The split: Stage 4's risk column read "refactors pair.lua's provenance
read" — every language's auto-pairing — for a stage the prose called the
Lean input method, which is exactly the rule §4 states and exactly what
round 4 found for Stage 3. Rev 5 had noticed the shape and answered it
with a commit boundary; a commit boundary is not a review boundary.
Stage 4a is now the typed-edit consumer chain (substrate, no Lean) and
4b the input method.
Rev 5's expansion semantics were wrong in three ways. Resolution is the
shortest key having the input as a prefix (\al yields ∀ from `all`, not
`alpha`); there is no terminator list at all ('+ ' is a key, so space
extends after \+; '\' is a key, so \\ yields \); and an unmatchable tail
is appended rather than dropped (\alp7 yields α7).
Three further findings. There is no cursor-motion hook, so acceptance 43
as written was not buildable and abandonment is lazy. dispatch_key is
only half of 4b's production path — \ and the letters are not excluded
from the optimistic classifier, and that producer is crdt-gated, so a
crdt-gated integration test is dark in CI and dark in the gate list. And
the whole expansion has cross-peer-degraded undo, a wider bite than
Q#LN6's three bracket pairs; set_round_trip_input would fix it and is
rejected with reasons.
New decisions Q#LN21 (undo degradation) and Q#LN22 (the state machine);
Q#LN10 and Q#LN11 rewritten; §2.11 records the upstream algorithm; §9.1
states the coherence impact for both stages. Acceptance keeps its
existing numbers and adds letter suffixes on both sides of the split.
Citation sweep per COHERENCE §25: five live citations moved in the 50
commits since rev 5.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Integrates canonical `main` @ `cf54270` and closes every finding.
**P1-1 — a stale document `Pointer` stole focus from the panel.** Real
bug. `align_primary_document_window`'s unknown-buffer arm returned
`Some(window)` despite aligning nothing, so #8's activation focused the
document *before* `dispatch_pointer` rejected the mismatched buffer. It
now returns `None`: alignment did not happen, so no caller may treat it
as a document gesture.
Pinned through `handle_dispatcher_event` — the real dispatcher seam —
because the defect lived in the PAIR of alignment and activation, not
in either alone. **The first version of that test was vacuous**: an
unregistered session is dropped at `daemon.rs:1962` (#148's
membership check) before the aligner runs, so it passed with the bug
restored. It now registers a real semantic session and fails with
exactly the reported symptom, focus moving `WindowId(2)` →
`WindowId(3)`.
**P1-2 — the approved A2A-2 fan-out was missing.** The semantic target
returned one context. It now captures the primary document PLUS the
visible side window, each provider invoked once, with a
derived-hidden side omitted (Q#BP2b — no mode line to paint, so no
callback should run for it). The acceptance asserts `windows.len() == 2`.
This exposed a second defect the finding did not name: the consumer
selected segments with `.find(|w| w.context.frontend_id == frontend_id)`
— the FIRST context for the frontend. With two contexts that silently
depended on capture order and could have shipped the panel's mode-line
text as the document status band. `emit_statusline_segments` now takes
the document `WindowId` and selects on window identity.
**P1-3 — the census suite tested the authority, not the consumers.**
Confirmed: reverting a producer to `active_window_for` left all ten
tests green. Added consumer-level pins that drive the real producers
through `SemanticRenderState::render_frame` with a panel focused, plus
the terminal-declaration guard. Bite-verified: reverting the
`LineNumbers` routing now fails
`consumer_line_numbers_follow_the_document_not_the_focused_panel`.
**P1-4 — main integrated.** The textual conflict was `docs/active-work.md`
(both lanes rewrote the same region; the terminal-config lane is kept
whole and the bottom-panel heading updated). `src/editor.rs` auto-merged,
and the full gate suite was rerun on the merge result.
**P2-5 — the painter test was vacuous.** A fixed-point check that
survived deleting `window.text_view.render`. It now asserts each of the
four extracted outputs actually appears: buffer TEXT, the line-number
GUTTER (with line numbers explicitly enabled, rather than dropping the
assertion), the window MODE LINE, and a returned caret. Bite-verified
by deleting the render call.
**P2-6 — the stale fold-projection claim is corrected.**
`src/window.rs`'s `fold_projection` doc no longer asserts that a
semantic session never enters `paint_frame`; it records that the panel
band breaks that premise and that the extracted painters take the map
as a parameter.
Gates on the merge result: fmt clean; workspace clippy clean; 1,832
default + 2,010 CRDT library tests; Stage 2A acceptance 13; Stage 1 46;
statusline 8; m11_5 2; GPU initial target 14; terminal config 12;
folding Stage 2 48; vterm 1/2 10 / 6; M4 121; required GPU 202;
`git diff --check` clean. `vterm_stage3_acceptance::a37` remains the
pre-existing flake measured on the base commit.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Integrates githubsucks/main @ cf54270 (terminal config Stage 1, #173).
Both conflicts were additive appends to the same lists — the handoff
preamble and the ledger's "Closed since the last snapshot" — so both
sides are kept and the preamble now leads with #173.
Also records what gating #173 measured about a37, because it changes
this lane's proposed fix rather than merely annotating it:
a37 reports `ok` without running whenever `pmacs-gpu` is absent from
the target directory. A fresh worktree reports the Stage 3 suite 9/9 in
0.17 s having never executed the arc's only real-daemon/real-PTY/real-
wgpu path; a genuine run takes about four seconds. Only
PMACS_REQUIRE_GPU=1 promotes that skip to a failure, and the standing
gate list applies that flag to `cargo test -p pmacs-gpu`, a different
package. So fix-shape part 2 must state the flag as a requirement of
the gpu-render job: a crdt leg added to the plain `test` job would run
a37 vacuously and report green.
a37 is also load-sensitive — it passed at d152120 and failed at that
same commit twenty minutes later under machine contention — which makes
a red first CI run ambiguous by construction. The lane now says to
re-run on the merge base before believing a failure, and to prefer
serialized execution over retry-until-green.
The vterm audit's "only 3 of 9 Stage 3 tests drive a real daemon" is
corrected: without the frontend binary the honest number is 2.
Ledger: terminal config Stage 1 flipped from IN REVIEW to MERGED.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
The parallel sweep failed one of the new tests for a real reason, not a
flake: drain_until ticks, and a tick can reap an immediately-exiting
child before the diagnostic runs. Recorded with the matched-load
measurement that shows the fix is load-bearing (0/15 fixed vs 1/10
unfixed under full saturation), and the final sweep numbers.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
Make command-time attachment healing cancel an armed terminal restart
before replacing the server, while keeping request-only lookup pure and
restart-safe.
Track config-driven server ownership privately, bound every fallback
server per SID, scope no-swap retirement to the failed root, and route
the shipped Lean diagnostics command through the safe resolver while
waiting for initialization.
Add direct acceptance counterexamples for all five review findings and
record the sixth-round verification and vacuity lesson.
The parallel workspace sweep failed
observing_the_leader_does_not_consume_the_exit_event with "process
ProcessId(26) is not running". A real defect in the test, not a flake.
The helper that fetched the pid drained for the Started event, and
draining ticks. A tick can observe an immediately-exiting child and
transition the record out of Running, after which signal returns "is not
running" and never reaches the diagnostic -- so the loop spun to its
10 s bound and panicked. It passed standalone because the drain returned
on Started before poll_one saw the exit; only the sweep's load shifted
the timing enough to lose that race.
Fast-exiting children now read the pid straight from the supervisor
record, which does not tick. The bounded loop also fails fast when the
record has left Running, so a future recurrence is diagnosed in one line
rather than surfacing as a timeout.
Verified under matched load: 15/15 green with all 16 cores saturated.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
The ledger's own update protocol requires a lane for volatile work, and
PR #176 had none: branch, worktree, review state, and verification were
all missing.
Records why the lane ships a diagnostic rather than a fix -- three
rejected tolerance designs, the two facts that killed the original
argument (group=true is rejected for PTY mode so the reap ledger never
applies to that path, and the ledger comment asserts EPERM cannot happen
rather than ruling that it means dead), and that the CI evidence never
established the child had exited.
Also records the round-1 test fixes and the four verified bites, so a
reader can tell which assertions are load-bearing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
Round-1 review found both test weaknesses.
The exited-child tests used a fixed 300 ms sleep as proof the child had
exited, which on a loaded runner can be false and would turn them into
spurious failures. nix's waitid is unavailable on macOS and libc::waitid
would need unsafe, which the crate forbids, so the tests now synchronise
on the observation under test: a bounded loop that drives the production
diagnostic until it reports the leader as exited. Each failing attempt
leaves the record untouched because the failure path returns before any
bookkeeping, so the loop is side-effect free, and it is strictly stronger
than a sleep because it observes the actual state rather than assuming it.
The assertions were substring checks -- target=-, expected_group=-,
leader=exited( -- which a hardcoded target or a wrong exit code would
satisfy. They are now exact message equality built from the pid the
kernel actually assigned and the errno's own Display, and the one-event
test asserts the surviving event carries exit code 7 rather than any
terminal event. The group test also spawns /bin/sleep directly rather
than through a shell, since a shell may place the command in a different
foreground process group than the one being asserted.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
Ledger entry for the in-flight Stage 2A branch, plus three findings the
gate run produced that are worth carrying regardless of this PR:
- The structural test comparing the two authorities directly did NOT
catch the focus-class bite; only the consumer-level assertion did.
Both kinds are needed, and the distinction generalizes.
- `vterm_stage3_acceptance::a37` is badly flaky on this machine —
6/8 failures on the BASE commit against 7/8 on the branch in matched
isolated samples, so it is pre-existing rather than a regression. It
also returns `ok` without running unless `pmacs-gpu` is built.
- `m11_5_semantic_acceptance` reports 0 tests and
`gpu_initial_target_acceptance` reports 1 without `--features crdt`.
Both are semantic-census suites, so gating Stage 2A in the default
config alone would exercise almost none of its relevant coverage.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Bottom-panel Stage 2A, second half (Q#BP8, Q#BP17). Still no protocol
change and no behavior change: `paint_frame` builds the same fold map
it always did and passes it in, so grid rendering is unchanged.
Two extractions, both taking the fold map as a **parameter** rather
than building it:
- `prepare_window_cursor_visible` — the active-window auto-scroll
clamp. The panel band (2B) runs this for its own window when that
window owns focus, and leaves a passive panel's `view_top` alone.
- `paint_window_content` — the per-window document body: text, gutter,
overlays, selection, and the mode line. The panel paints into a
panel-sized grid at the same origin-agnostic `Viewport`, so this is
that body lifted out, not a second painter (Bet B2').
The parameter is the point (Q#BP17). Folding built its per-window map
ungated on the premise that "a semantic session never enters
`paint_frame`", which the panel band breaks. The panel path must pass
`None` for a frontend whose `fold_projection` is false, and must not
call `EditorCore::fold_map_for_window` — that gates on the **active**
frontend, which is right for command-time reckoning and wrong for
painting another frontend's panel.
`tests/bottom_panel_stage2a_acceptance.rs` — 10 tests. The negative
half is the load-bearing half, so Projection assertions are paired
with focus-class assertions taken in the SAME state:
- `focus_and_projection_disagree_in_the_same_state` is the key one:
with a panel focused, the focus authority must name the panel while
the projection authority names the document. Routing the focus class
through `primary_document_window` fails this even though every
Projection test still passes.
- The statusline pair pins the split: the LOOKUP resolves the document
window while `active` reports actual focus, with a non-vacuity twin
that flips `active` back to true when focus returns.
- The extraction pair pins cells, the returned cursor, the focused
window's `view_top`, AND a passive window's untouched scroll —
identical cells alone would not catch a clamp that moved to the
wrong window on a single-window frame.
- `the_panel_fixture_really_builds_a_side_window` pins the fixture's
own precondition, since every other test is worthless if
`focused_panel` silently produced an ordinary split.
One crdt-gated caller of the old `align_semantic_window_to_buffer` was
updated; it compiles only under `--features crdt`, which is the
config CI never runs.
1,832 default + 2,009 CRDT library tests, 10 new acceptance; fmt and
workspace clippy clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Bottom-panel Stage 2A, first half. Every consumer the framing classifies
**Projection** now resolves the frontend's primary document window or
buffer instead of its focused one; every consumer classified focus,
focus-chrome, or focus/session is deliberately left alone.
No protocol change, no behavior change for any frontend today: with
`panel_capable = false` for semantic sessions, `primary_document_window`
returns `view.active` for every existing configuration, so this is a
seam adoption that becomes load-bearing in 2B.
Projection consumers routed:
- **#1** semantic buffer-follow / `BufferSnapshot` re-send
- **#2** the lazy CRDT upgrade — the sharpest case, since it BROADCASTS
to every replica, so keying it on focus would let focusing a fresh
generated panel buffer swap every peer's document mirror
- **#3** `CursorByte`
- **#4** `LineNumbers` mode
- **#5** selection decorations
- **#6/#10/#11** the full-window semantic terminal declaration, its
snapshot/sync, and terminal-frame suppression, via the shared
`semantic_terminal_key` resolver
- **#9** the `Viewport` terminal-context gate — a focused terminal panel
must not suppress the still-visible document's viewport
- **#12** the semantic statusline target LOOKUP
- **#21** the `BufferSnapshot` publication recipient filter
`align_semantic_window_to_buffer` splits per Q#BP14, which is the
distinction that makes rejecting panel-named events insufficient on its
own:
- `align_primary_document_window` (**#7**, `Viewport`) — aligns the
document window and **never touches `view.active`**.
- `align_and_activate_primary_document_window` (**#8**, `Pointer`) —
aligns and then activates, because a click in the document area means
"work here". This is the one place projection and focus legitimately
move together.
`dispatch_semantic_terminal_pointer` (**#11**) gains the same rule: an
accepted non-`Move` gesture activates the document window before the
gesture replays, while bare hover neither focuses nor claims.
The statusline change is deliberately a HALF change (parent acceptance
42): the window LOOKUP resolves the primary document window, but
`active` still reports **actual focus**, so a document provider can
truthfully observe `active = false` while a panel owns focus.
Untouched, and that is the load-bearing negative: #13 remote-op
validation, #14 `dispatch_idle_for`, #15 presence, #16-#19 search /
menu / minibuffer / completion chrome, #20 terminal bell drain, and #23
remote-op application all still resolve the actually focused window.
#16-#19's Q#BP14b routing table needs `PanelFrame` and lands in 2B.
1,832 library tests pass; fmt and workspace clippy clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Five findings, all real. The blocker and both majors are the same
mistake in three places: a claim asserted somewhere cheaper than where
it actually lives.
COHERENCE.md was stale in four places, not the three reported. Step 8
still read "no keybinding" and §11 still read "five settings", but §6's
dispatch table also still cited `is_terminal_escape_chord` — a symbol
this branch deletes. §25 requires that update to ride the PR, so a PR
changing audited ground truth has to re-grep the audit for its own
symbols, not only for its topic.
Acceptance 5 asserted a registry round-trip, which is a test of the
registry: it stayed green with the setting's only consumer deleted. It
now opens a real terminal whose child overflows the 24-row screen,
scrolls the view to its oldest retained row, and asserts LINE001 is
present at 10,000 and absent at 0.
Acceptance 8a waited for the session count to fall, which the rejected
editor-side cache map satisfies exactly — a map with no purge hook
leaks while sessions drain. Adds `TerminalManager::escape_caches()`, the
lifetime half of Q#TC4c's contract that `escape_parses` cannot cover.
`table.sort` over `pmacs.terminal.profiles` raised "attempt to compare
number with string" on the unknown-profile path whenever the user's
table held both a string and a numeric key, replacing the exact
diagnostic being asked for; `%q` raised likewise on a non-string
`profile` argument. Both are partial functions applied to user input on
a diagnostic path.
Also corrects the framing's status line, and a status message whose
embedded whitespace run had survived a rustfmt reflow.
Three new bites, each falsified by revert: deleting the scrollback
consumer fails acc5 and only acc5; restoring the raw-key sort
reproduces the comparison error verbatim; and implementing the rejected
map fails the new acc8a at left: 2, right: 1 while passing the old
session-count version.
Merges githubsucks/main @ ccf29e3.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Round 5 review: one P1, a frontend scope hole, and three P2s.
**1. A fallback that SPAWNS and then dies retried forever.** The
once-per-buffer guard bounds calls to `_attach_buffer`, not the server
those calls produce. `ensure_server` still never forwards `cfg.restart`,
so the fallback inherits `OnCrash`; an executable that exits before
`initialize` is respawned by the manager with no attempt ceiling —
silently, because `latched` has already disabled the primary's failure
poll. The fallback now gets its own one-shot die-before-initialize
watch, which retires it (ending the respawn loop) and reports.
The prior failing-fallback test used a NONEXISTENT executable, so it
only ever exercised synchronous ENOENT. To reach "spawned, then died"
the fixture has to actually spawn.
**2. Simultaneous frontends.** Both repair triggers read the ambient
`pmacs.window.buffer()`, and the daemon restores `active_frontend` to
the last-dispatched frontend before `tick_processes` — so a Lean buffer
active in ANOTHER frontend receives no `buffer.after-switch` here and
stays stale after its server is globally retired.
Fixed at the seam that is frontend-agnostic: **make consumption safe.**
`attached_for_active` now rebuilds rather than returning a record whose
server is dead, and `attachment_for_request` reports none (it must not
perturb LSP state, so it cannot rebuild). Whichever frontend runs a
command is the active one while it runs, so healing at the point of use
reaches every buffer no eager sweep can. This also closes the half where
a dead attachment was handed to a command and the request vanished.
**3. The retirement sweep stopped user-managed servers.** Selecting on
`language_id == "lean4"` also names servers the user spawned from
`init.lua`, which are not derived from `pmacs.lsp.config.lean4`. It now
keys on the `default-lean4` label `ensure_server` stamps — the
derivation discriminator.
**4. Repair ran even when no swap occurred.** `swap_to_fallback()`
returning false left `latched` true, so the next tick retried the
UNCHANGED configuration and reported it as a fallback failure. Split
into `probe.fallback_installed`: repair exists to apply a swap, so no
swap means nothing to apply.
**5. The once-per-buffer assertion counted table keys**, which cannot
distinguish "once per buffer" from "every tick for one buffer" —
cardinality stays 1 either way. Replaced with a numeric attempt counter;
the bite reports 174 attempts against the expected 1.
Five bites, each against 7c37bdc: no fallback watch -> attempt reaches
4; retire by language_id -> the user's server is stopped; gate repair on
`latched` -> a repair is attempted with no swap; drop the
once-per-buffer guard -> 174 vs 1; hand back a dead attachment -> a
command receives a `stopped` server.
Two more vacuity shapes recorded in the ledger (8 and 9): counting
distinct keys cannot bound repeated work, and a nonexistent executable
cannot reach any post-spawn failure.
A failing kill in ProcessSupervisor::signal reported an errno and
nothing else, which is not enough to diagnose the macOS CI failure that
prompted this lane: three different hypotheses about that EPERM produce
the same message, and the fix each one implies is different.
The error now carries five facts as separate fields: the target source
(which branch of signal_target ran), the target kind and value, the
spawn-time group for a group-directed signal, the errno, and the
spawned leader's real try_wait state.
Keeping the target and the leader apart is the whole point. For a PTY
the signal goes to the terminal's foreground process group, read from
the tty at signal time, while the leader is the child that was spawned.
Those are different entities whenever job control has moved the
terminal, and three rejected designs for this code were unsound
precisely because they concluded something about one from the other.
The report states both and concludes nothing.
The disposition is unchanged. Every call that failed before still
fails, with no state transition and no reap-ledger arming. That is
asserted directly rather than assumed, because it is what separates
this from the tolerance rules review rejected.
Q#PD3, stated narrowly: this is not a pure message change. Consulting
try_wait reaps an exited child and caches its status, so the child may
be reaped earlier than it otherwise would be. That is observably safe
because portable-pty 0.9.0 returns a std::process::Child on Unix and
delegates try_wait straight to it, so the status is cached and poll_one
still sees it -- but safe by argument is not safe by assertion, so a
test forces a kill failure against the real PTY child and then checks
that exactly one terminal event survives.
Q#PD4: the test seam injects the kill attempt's result only, never the
observation. Target selection, the real ChildHandle::try_wait against
the real child, and the error construction all run unmodified; a
stubbed observation would bypass the code path under test.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
A docs-only PR (#172) failed Test (macos-latest / luajit) on
acc28_child_input_and_the_c_c_escape_work_unchanged_in_a_panel with
"kill: EPERM: Operation not permitted" raised out of terminate. A docs
diff cannot cause that, main was green at the PR's exact base, and three
other PRs passed the same job.
This framing reaches revision 4 after three review rounds, and what it
proposes is much smaller than what it started with. Revisions 1 to 3 each
proposed a tolerance rule -- treat some errno as success -- and each was
unsound in the same way: they concluded something about a process from
something that was not about that process. Revision 1 concluded from an
errno alone, which says only that a syscall failed. Revision 2 concluded
from the spawned leader while a PTY signal targets the tty's foreground
process group, which diverges from the leader exactly when job control is
in use. Revision 3 corrected EPERM but kept group-directed ESRCH, which
proves only that the selected foreground group vanished, not that the
leader exited.
So no tolerance rule lands. The disposition is preserved exactly: every
failing call still fails, with no state transition and no ledger arming.
What lands is that the failure explains itself, recording the target
source and value, the spawn-time pgid or leader pid, the errno, and the
leader's real try_wait state as five separate facts. Every candidate fix
is decidable from those together and none is decidable from the errno
alone.
Two claims are stated more narrowly than earlier revisions had them.
Consulting try_wait reaps an exited child and caches its status, so this
is not "strictly additive" -- it is "no disposition change", with an
event-count test pinning that poll_one still emits exactly one exit
event. And the test seam injects the kill attempt's result only, never
the observation, so the real ChildHandle::try_wait runs against the real
child; a stubbed observation would bypass the path under test.
Parked with their reasons: all tolerance rules, terminate becoming
idempotent for an already-reaped process (an independent fix answering a
different failure), and signal_target's read-then-kill of tcgetpgrp,
which is the most likely real fix site.
The lane closes when this lands rather than waiting for the flake to
recur; the next occurrence carries its own evidence under whoever's PR.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
#175 (bottom-panel Stage 2 framing) landed after this branch's last head
and touches both shared docs, so the previous green run did not cover the
combination. Merged cleanly this time — no conflict.
Also fixes an inconsistency this PR introduced: the recovery check still
accepted `d152120` while the canonical-base line above declared a newer
commit. A threshold looser than the base it guards passes on a tree the
rest of the file does not describe, so the two now move together and the
text says why.
`docs/agent-handoff.md` §1 still said Stage 2 "needs its own
re-framing". It is framed, so that line would be false on `main` the
moment this branch merges.
It now records the approved shape — protocol v21, two serial slices
(2A census routing + painter extraction, then 2B wire/projection/band/
capability flip), parent acceptance 37-55 still authoritative — and
carries the census classification rule itself, since that is the fact
the ledger previously got wrong and the one a future reader is most
likely to re-derive incorrectly.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both conflicts were competing rewrites of the same anchor lines: #172
refreshed the canonical base and the handoff header while this branch
did the same for #165. Resolved by taking main's list, which is the more
accurate of the two (it names Lean 4 Stage 2 #161 properly), refreshing
it to the current tip `ccf29e3`, and keeping this branch's note that
lanes naming an older base have not been re-based.
#172 also removed the inline-math lane, so the stale-header note drops
from three back to two and now says who owes the remaining updates.
Round 4 review: one P1, and it is the same defect for the FOURTH time.
`pmacs.lsp.config.lean4` is a single global entry, so swapping its
command invalidates **every** Lean buffer and **every** Lean server —
Q#LN15 gives one server per project root, so there can be several.
Rounds 1-3 each repaired one buffer and retired one server, and round 3
shipped "repair the armed target, strand the rest": status and config
said fallback while a second open Lean buffer stayed on the retired
command, and a second project root's server stayed live.
The shape that actually holds:
* **Retire ALL `lean4` servers on latch**, not the one the probe
happened to name. `probe.primary` identifies the server the VERDICT
is about; it was never the set of servers the swap invalidates.
* **Repair each buffer lazily and at most once**, when it becomes
active — on `buffer.after-switch` and on the tick. `_attach_buffer`
is an active-buffer-only seam, so a global swap cannot be applied to
every open buffer at once; it has to be applied as they surface.
lsp.lua's own `after-switch` re-pushes views but does not rebuild a
stale attachment, so nothing else covered this.
* The **once-per-buffer bound** is load-bearing: without it a fallback
that also fails to spawn would retry every tick forever — the
round-2 defect, which a naive global repair loop would reintroduce
for every buffer instead of just one.
* `shutting-down` is deliberately not treated as stale. It is still
live by `server_is_live`'s reckoning, so attaching would early-return
the stale record and burn that buffer's single attempt on a no-op.
P2: argument-inclusive attribution was implemented in round 3 but pinned
only by "contains the command name", so a mutation dropping every
argument passed. Now asserted against the exact `<command> <args>`
string.
Also fixed a vacuous assertion this refactor created: a test checked
`_probe.reattach_from == nil` for a field that no longer exists, which
reads as nil and passes for nothing. It now asserts a positive count of
recorded repair attempts.
Three bites, each against 73587b0: repair only the armed buffer -> the
second buffer stays on `lake`; retire only the named server -> one live
stale server remains; drop arguments from attribution -> the exact-string
assertion fails.
The ledger records a second durable lesson beside the vacuity one: **a
scope error repeats until the scope is named.** Four rounds of locally
correct fixes, none of which asked what the config swap invalidates.
When a change edits shared state, enumerate everything derived from it
before repairing anything.
Closes review round 3 — 1 blocking, 1 high, 1 medium.
**R3-1 (blocker) — the call-site table contradicted the source.** The
three-boundary model was right; five rows of its classification were
not, and each was a real defect:
- `:6140` is `completion_dropdown_layout` — DOCUMENT completion
placement, deriving the space below the anchor line. Classified
status-owned, it would let completion overlap the panel.
- `:7195` and `:7212` are the `status_buffer` / `status_left_buffer`
`TextBounds.top` — status text bounds, classified document-owned.
- `:7351` clips global minibuffer CANDIDATE glyphs to the dropdown's
band anchor; classified document-owned, they would be clipped
against a boundary the dropdown does not sit above.
- `:8561` (`edge_scroll_direction`, document edge scrolling) was
missing entirely, leaving it tied to the old bottom.
- `:8077` is `code_caret_rect_in_clip` — caret clipping, not
completion placement. Its class was right, its label wrong.
Every production site is now individually verified against the source
and tabulated with what it actually is. The census is stated as
arithmetic a reader can check: 29 matches = 20 production + 1
definition + 8 test sites.
Root cause recorded in the revision history: rev 3's table was built
from a `grep | head -20` over 29 matches, which is precisely why
`:8561` vanished. The minibuffer's status-owned status is now argued
from Q#BP14b rather than assumed — it is global, bufferless chrome
anchored to the status band, so all four of its sites stay with the
band.
**R3-2 (high) — clamps preserved.** The three equations permitted
negative coordinates on a surface shorter than its chrome, where
today's `text_area_bottom` clamps with `.max(0.0)`. All three now
clamp at zero, which keeps the "exact formula" exact exactly where it
matters most.
**R3-3 (medium) — attachment rejection classified SHARED.**
`validate_cells` also rejects `cell.attachment.is_some()`
(`terminal.rs:305`), whose error text reads "which terminals never
use" (`:190-191`) — phrased as a terminal-specific fact, which is why
rev 3's "exact split" missed it. Panels implement no attachment
rendering in Stage 2, so a `PanelFrame` carrying one describes a
surface the GPU would silently not draw; shared rejection fails closed
on the producer side instead. The message is reworded grid-neutral
when it moves, and giving panels attachment rendering later moves the
rejection back deliberately rather than by default.
A2B-4 now names the counts on both sides (twelve document-owned move,
eight status-owned do not) and carries the three symptom-bearing rows
that a plausible misclassification produces. §9 records that the GPU
three-boundary split belongs to 2B, not 2A — it is only observable
once a band can be installed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 3 review: two P1 asynchronous-correlation defects, with the
focused suite at 25/25 while both were live.
**1. A late version verdict retired nothing and claimed success.**
`probe.watching` is cleared the moment the server initializes — it is
failure-polling state. A slow `lake --version` landing after a
successful initialize therefore reached `fire_latch(nil)`, which retires
nothing: `_attach_buffer` found the still-live primary attachment,
early-returned it, and the retry counted that as done. Status said
"falling back", the config named the fallback, and the buffer stayed on
the old server.
**That is the round-1 silent no-op arriving through a third event
ordering** — first as "no re-attach at all", then as "re-attach cleared
by an unrelated buffer", now as "re-attach satisfied by the server we
were supposed to replace". The fix separates the two facts that were
being carried by one field: `probe.primary` is the server the verdict
applies to and survives initialization; `probe.watching` is the
failure poll and is cleared by it.
The existing fixture could not reach this ordering at all — its `serve`
sleeps, so the primary can never initialize before `--version` returns.
The new one execs the fake LSP for `serve` and delays 0.6s before
reporting 3.0.0.
**2. `buf_key` was the most recently loaded Lean buffer.** Written on
every Lean `buffer.after-load`, so a second Lean file opened before the
verdict became the rebuild target while the latch still watched the
FIRST buffer's server. Target buffer and primary server are one fact and
are now armed together, exactly once. Both files in the new test share a
package, so mis-targeting shows up as a stranded buffer rather than as
two unrelated servers.
**3. The failure message hardcoded `lake serve`** after the latch became
command-agnostic, telling a user whose `my-lean-wrapper` failed to go
debug lake. `configured_command()` names what is actually configured,
arguments included.
**4. The ledger** now records all fifteen bites across the three rounds,
both prior review rounds' findings (the round-2 block was lost when an
earlier edit script aborted before writing), and the durable lesson.
That lesson, recorded for the handoff: **six tests across three rounds
were written, ran green, and pinned nothing** — caught only by biting.
The shapes are enumerated in the ledger; the rule is that a test is not
evidence until the mutation it targets has been shown to fail it. Two
of the six are subtle enough to be worth naming here: a bite that
RAISES is swallowed by the hook's pcall and "passes" for the wrong
reason, and a fixture whose `serve` sleeps cannot reach any ordering
where the primary comes up first.
Closes review round 2 — 1 blocking, 2 high, 1 medium — decides both
remaining open items, and re-integrates canonical `main` @ `ccf29e3`
(#172 + #157; documentation plus one `src/buffer.rs` regression test,
no protocol or Stage 2 source anchor moved).
**R2-1 (blocker) — the seam is three boundaries, not one.** Rev 2 asked
for a single document-bottom accessor. That is wrong: once a panel is
installed the present single value must DIVERGE, because several of its
consumers must not move at all. `text_area_bottom`
(`pmacs-gpu/src/main.rs:8490`) is today `status_band_top`,
`geometry_capacity_bottom`, and `document_text_bottom` at once. Rev 3
defines all three, classifies every one of its ~19 call sites as
status-owned / document-owned / geometry, and records that four sites
rev 2 named (`:3175`, `:3185`, `:6601`, `:6607`) consume a status-band
HEIGHT and no bottom coordinate at all, while the status background
`:5908` and status text `:7134`/`:7922` must stay at the physical
window bottom.
The acceptance is now a contrast assertion: installing a panel moves
every document-owned consumer WHILE the status band stays
pixel-identical. "Everything moved" alone is passed by a blanket
rewrite of the helper, which is exactly the wrong implementation.
**R2-2 (high) — epoch exactness.** `accept_frame_geometry` returns
`Advanced | Duplicate | Rejected` instead of a boolean that cannot
separate reconcile-needed from already-current from stale; if a boolean
is ever kept internally it must be named `advanced`, since `Duplicate`
is also accepted. Rev 2's exhaustion wording permitted retaining stale
geometry, which is not fail-closed — a real resize after exhaustion
would keep painting a panel sized to disowned geometry. The grid path
now clears `frame_geometry` to unknown and reconciles hidden, and the
frontend takes a terminal latch so a retained matching `Present` cannot
resurrect the band; only a fresh session clears it.
**R2-3 (high) — parent acceptance 52 splits.** 2A has no semantic panel
projection, so it can only prove the extracted painter honors an
explicit `None` map plus the `src/window.rs:562` comment fix. The real
contract is production-reachable only in 2B and is reasserted there
beside 42/43/44.
**R2-4 (medium) — touched gates named**: `statusline_segments_acceptance`,
`m11_5_semantic_acceptance`, `gpu_initial_target_acceptance`,
`gpu_font_acceptance`, beside the vterm, folding, and GPU suites.
Open items decided: `BASE_DIVIDER_HEIGHT = 4.0` at scale 1.0, scaled by
`FontMetrics::scale`, whole strip painted `ui.divider` and used as the
exact hover/drag hit rect; `TEXT_TOP` stays `16.0` unscaled, with
Q#BP15a's "all quantities use the frontend's current scale" narrowed to
font-derived metrics and the divider. Wholesale surface-inset/DPI
scaling is recorded as separate work, not smuggled in.
The ledger's bottom-panel lane keeps its census correction and gains
the three-boundary one.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Closes review round 1 — 2 blocking, 3 high, 3 revision points — and
rebases the ground truth onto `main` @ `d152120`.
Both blockers were rev 1 asserting something the parent framing
already decided otherwise:
- **R1-1.** Rev 1 said all 23 census reads route through
`primary_document_window`. Q#BP14 routes only the **Projection**
class that way; focus/input (#13-#15, #23), focus chrome and
surface-routed (#16-#19), and focus/session (#20) keep their own
authorities. Rev 1's rule would have broken remote-op validation and
application, `DispatchIdle`, presence, focused search/menu/completion
routing, and terminal bell ownership. §3.2 restores the four classes
as a table and the acceptance asserts each separately — the
focus-class assertions are the load-bearing half, since a test that
only proves "the document is used" passes with them wrongly
rerouted.
- **R1-2.** The three `src/statusline.rs` active reads have two
dispositions, not one. Only `:644` selects the wrong window; `:629`
and `:675` must keep tracking actual focus, because grid contexts
need a truthful `active`, revalidation must notice a focus change,
and parent acceptance 42 requires a document provider to be able to
observe `active = false` while the panel is focused.
The three high findings:
- Q#BP2S1 resolves to frontend-owned epochs (option 1) — a font or
scale transaction can need to invalidate an old `PanelFrame` while
the derived `CellSize` is identical, which daemon value dedup cannot
detect. Rev 2 adds the four-row transition table, splits grid
allocation from semantic acceptance into two APIs rather than one
ambiguous method, moves the grid allocator off `saturating_add` to
checked-with-fail-closed, and defines the initial epoch and both
exhaustion behaviors. Rev 1's "rejects a lower-or-equal epoch
carrying different data" was itself wrong: a lower epoch carrying
identical data is still stale.
- The `panel_capable` flip is narrowed to an authenticated semantic
session negotiated at **v21 or later**. Denying a v20 peer the new
events is insufficient if the daemon still places its window in a
side panel it cannot render — the gate is on placement.
- Parent acceptance criteria 37-55 are declared authoritative and
mapped to slices 2A/2B, with rev 1's eleven drafts demoted to
refinements. The painter-extraction criterion now pins cells, the
returned cursor, the focused window's `view_top` mutation, and
passive-window state.
All four scout obligations are closed (§5), and the pixel formula is
treated as contract work, not implementation detail:
- The shared/terminal-only validator boundary is named exactly.
- Four new outbox tail-coalescing tags beside the existing four.
- **`State::mono_advance` is unsafe to adopt**: absent a `FontFacts`
probe it samples the document's first shaped glyph, which would make
panel columns document-dependent. The declaration uses the existing
stable normal-face `probe_mono_advance` instead, and declares zero
usable geometry when it returns `None`.
- `BASE_DIVIDER_HEIGHT` does not exist. Rev 2 decides its scaling and
requires **one** document-bottom accessor routing every consumer
(caret, hits, minimap, terminal geometry, clipping, edge scrolling)
— a second unrouted seam is precisely the Stage 1 `Layout::compute`
two-caller defect. The concrete base value is left open for round 2.
Also: the coherence statement now names journey steps 7-10 instead of
claiming none, and drops rev 1's overclaim that this advances
background-work visibility — a panel gives output a placement but adds
no join key to COHERENCE §9's four disjoint activity planes.
The ledger's bottom-panel lane is updated from "no branch and no
framing yet" to the framing's real state, and carries an explicit
correction: that entry was itself the source of rev 1's census
mis-statement.
Factual corrections: `InitialTargetResult` is at `message.rs:1145`;
`primary_document_window` has four references and two production paths
(`daemon.rs:1639`, and `daemon.rs:2998` via `primary_document_buffer`,
which is census #22); fifteen PRs merged since the parent's last
re-scout, not eleven.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The re-framing `docs/bottom-panel-framing.md` rev 4 §2 requires before
Stage 2 (the GPU panel band) is implemented. Re-scouted against
canonical `main` @ `5aa9044`, protocol v20.
It does not restate the parent's decisions; it records what the
re-scout found. Every source anchor Stage 2 inherits had moved, but
none of the parent's mechanical model was falsified. Two facts held
and are load-bearing: protocol is still v20, so Q#BP9 resolves to
**v21** with no reservation needed, and both byte pins
(`InstanceMessage::InitialTargetResult`,
`FrontendEvent::TerminalPointer`) are still their enums' final
variants.
Four findings:
- **Q#BP2S1, new and open.** Stage 1 landed a daemon-side geometry
epoch allocator (`declare_frame_geometry`), but Q#BP15a specifies a
frontend-owned epoch echoed by every `Present`. The landed allocator
also dedups on value and uses `saturating_add`, which is neither
wrapping nor the fail-closed the framing asks for. Three resolutions
are stated with a recommendation.
- **The §1.3 census is essentially unrouted.** Stage 1 built the
`primary_document_window` seam but it has one production caller;
~80 direct `.active` reads remain. This is Stage 2's bulk, not its
tidy-up, and the stage plan sequences it first.
- **The statusline active read is three sites, not one.**
- **Four scout obligations are still open** and are named rather than
papered over, including the GPU-side pixel formula inputs.
Also carries the staged plan, draft acceptance criteria, the coherence
impact per `COHERENCE.md` §20 (§14 is the section it serves), and four
questions for the user.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Stage 1 of the terminal config/copy-mode arc is in review; Stage 2 is
not started. Records the four decisions forced by scouted ground truth,
the four bites against four different wrong implementations, the two
reusable test instruments, and the gate results.
Stage 1 of the terminal config/copy-mode arc. The terminal had no
configuration surface at all: the command hardcoded $SHELL, scrollback
was a per-open argument only, and the escape chord was a literal in
Rust. No protocol change.
Profiles are a raw Lua table, pmacs.terminal.profiles, not a registry
setting: ConfigValue is four scalars with no table kind, so profiles
join pmacs.lsp.config and pmacs.pair.sets until table-valued settings
exist. The registry gains three scalars whose defaults reproduce the
previous behavior exactly.
Field resolution is explicit open argument, then profile field, then
scalar setting, then $SHELL. env MERGES, with explicit entries
overriding the profile's, because first-wins there would silently drop
half a user's environment. An explicitly named profile that does not
exist is an error even when terminal.default-profile is valid, so a typo
cannot silently fall back.
The two open-time settings resolve through the GLOBAL chain, because
they are read before the identity buffer exists and no caller could have
pinned a local override on a buffer that does not yet exist. Only
terminal.escape-key resolves per buffer, which makes a per-terminal
escape a supported feature.
The escape key is parsed at most once per (terminal, config epoch), and
the cache lives on TerminalSession so its lifetime is the terminal's,
with no purge hook to forget. The epoch alone is not a sufficient key:
it does not advance when focus moves between two terminals with
different buffer-local values, so an epoch-only cache serves one
terminal's chord to the other. An unparseable value falls back to C-c
and reports once per terminal per effective invalid value through the
status line, because a terminal with no escape chord cannot be escaped
to fix the setting that broke it.
Repeating the escape now sends THAT chord to the child through the
ordinary key encoder, rather than a hardcoded ETX. With an escape of
C-x, the previous code sent Ctrl-C and made literal Ctrl-X unreachable.
C-c t opens a terminal. COHERENCE Priority 1 names a terminal
keybinding, and section 2 step 8 grades the terminal works-but-
undiscoverable; C-c is already a live global prefix, so this is a new
leaf rather than a shadow. It is unreachable from inside a terminal,
where C-c is the escape.
Acceptance is tests/terminal_config_acceptance.rs, deliberately NOT
crdt-gated so CI actually runs it. Four bites, each against a different
plausible wrong implementation: a hardcoded ETX fails acc6/9; an
epoch-only cache key fails acc7; a single last-entry cache fails acc8's
parse count; removing the invalid-value fallback fails acc10.
Two test-instrument notes worth keeping. cat -v is the echo probe
because the screen rejects C0 controls before they reach cells, so a raw
echoed Ctrl-X would be invisible. And the probe counts occurrences
rather than testing presence, because a single-character probe collides
with the child's own banner text.
Three P1 lifecycle defects and two P2s. The focused suite was 20/20 with
every one of them live, which is the part worth keeping.
**1. The crashed primary respawned forever underneath the fallback.**
Round 2 skipped the retire call for terminal servers to avoid corrupting
them — but the crash had already armed `next_restart_at`, and
`maybe_restart` fires on every elapsed backoff with no attempt ceiling.
The broken command kept respawning under the live fallback.
The right call depends on the state, and each is wrong for the other:
`forget` REQUIRES a terminal state and removes the client outright,
which also drops the restart timer; `stop` is for a live one and
corrupts a terminal one (its not-initialized branch parks it in
`ShuttingDown` forever). `retire_server` now dispatches on state.
**2. Re-attachment targeted whatever buffer was active when the
asynchronous verdict landed.** `_attach_buffer` is an active-buffer-only
seam, and "some attachment now names a different server" is satisfied by
an unrelated Rust buffer — clearing the retry and leaving the Lean buffer
stale forever. The initiating buffer is now captured and the retry waits
for it.
**3. A failing fallback retried every tick forever, silently**,
contradicting acceptance 27's promise that a second failure surfaces.
"Waiting for the old server to go" and "attempting the replacement" are
now separate: once the old one is terminal or gone, the replacement is
attempted EXACTLY once, and a spawn failure is reported.
**4. The Lake version parser was being applied to arbitrary wrappers.**
`version_below_3_1` encodes lake's output contract; a working
`my-lean-wrapper` reporting "wrapper 1.0" would have been replaced
despite its server initializing fine. The version probe is now gated on
the command's basename being `lake`. The FAILURE latch stays
command-agnostic — that one keys on the server actually not starting,
which is true of any command.
**5. An unconfigured Lean server was reported as a failure** and latched,
poisoning the session so a later configuration could never take effect.
Absent config or command now means disabled; only a configured command
that produced no attachment is a failure.
**6. The ledger recorded pre-fix counts** after the fixes were pushed.
Now 25/25 and 3,214. That is the #161 fmt-blocker error in a slower
form: verification must describe the pushed tree.
Sign-offs requested in review: `M.fallback` is now `M._fallback`, an
underscored test seam, and its idempotence check compares args as well as
command — the same command with different arguments is not "already
applied". Dropping the `command ~= "lake"` guard stands for the failure
latch only.
Five regression tests added, and **three of them were too weak on first
write; only bite-testing found it**:
* asserting "no live non-fallback server" misses a respawn loop,
because a respawning server sits in `crashed` most of the time —
`attempt` is the observable that counts respawns;
* returning to a buffer with `find_or_open` re-fires
`buffer.after-load`, which repairs the attachment regardless of the
code under test — `switch_buffer` is the honest return;
* a MISSING command fails synchronously inside `after-load` where the
rebuild happens inline, so the async race cannot occur — only the
probe path exercises it.
Each of the five now fails against the exact round-2 mutation it targets.
Both conflicts were docs-only and resolved as unions, with one repair
taken from main: #156 fixed a pre-existing corrupted duplicate of the
"GPU initial target LANDED — #148" bullet in the handoff, whose tail ran
into the protocol-version text. This branch still carried the broken
copy, so the resolution keeps main's repaired `- Protocol **v20**` bullet
and drops the stub, along with main's now-superseded "Stage 1 IN REVIEW
as PR #165" sub-bullet.
Refreshed the canonical base to `d152120` and widened the stale-header
note from two lanes to three: #158 merged but its lane still reads
"PR #158 OPEN".
Brings the three required docs current after #158 merged, and discharges
the follow-up that framing named for itself.
COHERENCE.md section 16 audits the claim that the GPU frontend exceeds
the TUI "under real divergence pressure" without a privileged frontend
emerging. Inline math is the sharpest instance of that so far -- the GPU
typesets $...$ while the TUI shows LaTeX source, and the TUI fallback is
a named deferral. Section 25 makes that update ride the PR, so the
enumerated list gains the case along with what keeps it inside the rule:
the slice reserves no protocol version and adds no wire surface, so the
divergence is presentational and both frontends read the same model.
docs/inline-math-framing.md carried a licence error the slice framing
flagged in its own section 9 and deliberately did not fix in-branch,
since the parent is a merged document. Latin Modern Math is under the
GUST Font License, not the OFL; the row now says so and records the
~717 KiB bundled size.
docs/agent-handoff.md records the landing and re-anchors section 1 to
d152120. The bullet leads with the facts a fresh agent would otherwise
have to rediscover: the whole slice lives in pmacs-gpu because pmacs-gpu
depends only on pmacs-protocol and never on pmacs; the v0 subset is 34
Greek symbols, sub/superscript and \frac; an unsupported command fails
the WHOLE span back to source, so most inline spans in a real paper
still show LaTeX by design; and math is suppressed while the caret is
inside its span.
docs/active-work.md removes the merged lane per its own update protocol
and adds a Closed entry. Four things there are reusable beyond this arc:
a stale frontend binary is invisible from the source tree, so diagnose
with strings on the binary rather than by re-reading a checkout that is
already current; the dangerous integration was the one that did NOT
conflict, so decide from the shared-file set rather than from whether
git complained; integration is proved by predicting the other side's
test-count delta and checking it; and m4_5_basedpyright has no timeout,
hangs forever, and is intermittent, so an earlier clean sweep proves
nothing. It also corrects a claim I recorded on main: the branch's
missing CI was not an unidentified cause -- a conflicting PR builds no
merge ref, so no pull_request run is created.
Docs only; no code changes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
Round 1 review, four P1s. All real; the first two mean the fallback did
not work at all.
**1. The latch swapped the config but never spawned or re-attached.**
Nothing re-fires an attach on a config change and `attach_buffer`
early-returns for a live attachment, so the buffer stayed bound to the
server that had just been stopped. The user got a config edit and no
language server. `fire_latch` now rebuilds through a new
`pmacs.lsp._attach_buffer` export.
Two mechanics had to be right for that rebuild to happen at all:
* It is **retried on the tick**, because `pmacs.lsp.stop` leaves the
state `shutting-down`, which `server_is_live` counts as LIVE — an
inline re-attach early-returns the stale record and the swap is a
silent no-op.
* The latch **does not stop an already-terminal server**, and this is
a substrate bug worked around rather than a style choice.
`LspManager::stop` on a `Crashed` client takes its not-initialized
branch, terminates the dead process, and sets `ShuttingDown { ..
None }` on the premise that "the next exit observation cleans up" —
but the exit already happened, which is what made it `Crashed`. No
further event arrives, so the client is stuck in `ShuttingDown`
forever: `server_is_live` reads it as live so `attach_buffer` never
rebuilds, and `forget` refuses it for not being terminal. Stopping a
dead server is what makes it un-replaceable. Named in framing §6; the
fix belongs in `stop` and changes behavior for every language.
**2. A missing `lake` bypassed probe and latch entirely** — the single
most likely real failure. `ensure_server` swallows a synchronous ENOENT
and returns nil, so there was no attachment, and the hook keyed on
`active_attachment()` returned before arming anything. The hook now keys
on the buffer's LANGUAGE and treats a Lean buffer with no attachment as
the failure itself.
**3. `waitForDiagnostics` omitted `version`.** Lean's
`WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0,
`src/Lean/Data/Lsp/Extra.lean`); the request is how a client says which
revision it wants. It looked correct only because the fake server echoes
any payload — so the fake server now validates and returns InvalidParams
without it.
**4. The ledger stated the dangerous stacking order** in one sentence
and the correct rule in the next. Fixed to say BEFORE. A safety rule
written twice with opposite senses is worse than not written.
Also (P2): the probe/latch suite now drives the production path —
`buffer.after-load` -> ticks -> probe drain -> latch -> re-attach — with
real executable stubs, and asserts the originally opened buffer ends up
on a LIVE server. Round 1's acceptance 36 asserted every server was
terminal, i.e. pinned the ABSENCE of the fallback it claimed to test.
`M.fallback` is a table so the suite can point it at a working stand-in;
the probe now spawns `cfg.command --version` rather than a hardcoded
`lake`, which is also more correct for a user who configured a wrapper.
`swap_to_fallback`'s `command ~= "lake"` guard is gone: the latch fires
only when the configured server actually failed, one visible fallback
beats no server, and `probe.latched` is what keeps it to exactly one.
Three new bites, all against the committed tree: no re-attach after the
swap -> three latch tests fail; hook keyed on the attachment -> the
missing-`lake` case fails; `waitForDiagnostics` without `version` ->
acc37 fails with the server's InvalidParams.
Two stages, one arc, no protocol change. Stage 1 makes the terminal
configurable (profiles, scrollback, escape key) and binds the opening
command; Stage 2 adds copy mode and search over scrollback. They are
independently releasable and get separate branches and PRs.
Three scouted facts shaped the design, two of them ruling out the
obvious plan.
Profiles cannot be a config-registry setting: ConfigValue is four
scalars and there is no table kind, so profiles join pmacs.lsp.config
and pmacs.pair.sets as a raw Lua table while the registry holds only
scalars.
Search cannot reuse isearch in place: SearchStore addresses matches as
byte ranges into a buffer's rope, and a terminal identity buffer is
empty by construction.
An in-place copy mode would be the seventh dispatch shadow, which
COHERENCE section 6 grades weak and growing by one island per modal
feature, with no transient-keymap mechanism to migrate to.
Copy mode therefore materializes the retained rows into an ordinary
read-only buffer. isearch, motion, selection and the kill ring work
with no new substrate; the "keys must not reach the child" problem
dissolves because the snapshot is not a terminal; and describe-key
stays truthful because the bindings are buffer-local. The cost, stated
in the doc, is that the snapshot is point-in-time rather than a live
freeze.
Four review rounds produced the load-bearing parts: the escape-key
cache is owned by TerminalSession so its lifecycle is the terminal's,
with three acceptance pins that each fail a different wrong cache; the
snapshot needs set_round_trip_input because a Lua intercept does not
set Buffer::read_only and an optimistic CrdtOp would mutate both the
daemon buffer and the mirror; the double-escape must encode the
configured chord rather than a hardcoded ETX; and the two open-time
settings resolve through the global chain because they are read before
the terminal buffer exists.
No code changes in this commit.
Levi Neuwirth