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
Three design blockers, four cleanups, and the staging call taken. Round
3's theme: rev 3 named the right seams but sized two of them from a
partial inventory, and one promise was still stronger than its mechanism.
All three verified against c93f9ee.
H1 — the modified-buffer delete check races the syscall. Rev 3's
"immediately before each syscall" was wrong about where the boundary is:
pmacs.fs.remove DISPATCHES A WORKER, so the interval to remove_blocking's
remove_file is wide open, and acceptance 20 (edit before y) could never
have detected it. NARROWED to a TOCTOU-bounded pre-dispatch check, the
same honest framing G6 forced on R, rather than inventing a reservation
primitive inside a dired stage. The residue is stated precisely: the
buffer survives with its contents (that half IS robust — it runs at drain
time), the file does not. So the orphan deferral rev 3 scoped to the LSP
path now covers dired too, as one deferral rather than two. Acceptance 20
says outright that the interval has no test because it is not closed.
H2 — the LSP teardown inventory was a third of the real one. LspManager
holds FOURTEEN URI-bearing store families (lsp.rs:741-819), not five, plus
the `documents` text map didChange diffs against — a stale entry there is
a correctness problem, not a leak — plus pending_routes, whose
ResponseRoute variants CARRY THE URI at fifteen insert sites, so an
in-flight response repopulates the old key AFTER any clear. Rev 4 gives
the full table and one manager-level forget_uri(sid, uri) that purges
routes, drain-cancels the matching awaiters (the existing contract at
:799-803 already requires that wherever routes are purged), and clears all
fourteen plus documents — handling locations_store's kind key and
symbol_store's scope key specially. Modelled on the server-scoped
teardown at :1316-1331. Also records the surprise found on the way: that
teardown clears routes and documents but NOT the fourteen stores.
H3 — the diagnostic-view seam is now chosen, not either/or. Verified the
constraints: DiagnosticView.uri is private and immutable, View has no
downcast, and _attach_view takes active_window_mut() and ERRORS otherwise,
so it reaches one window and cannot drive a per-window loop from Lua; and
a remove-and-re-push loses composition order in an ordered
Vec<Box<dyn View>>. The seam: a View::rename_resource default-no-op hook,
joining overlay_identity and clone_for_split — the family #113 round 6
added for exactly this class — swept over core.windows.values_mut() the
way overlay disposal already is (mod.rs:2016-2019). In-place mutation, so
order is preserved by construction, the field stays private, and future
URI-bearing overlays opt in by overriding rather than growing a special
case. Acceptance 30 now needs TWO windows and an order assertion; a new
item 31 pins the store inventory and the in-flight repopulation.
Staging: TOOK THE FURTHER CUT as directed. Three PRs — 2a the
reconciliation transaction with no dired surface, 2b marks and operations,
2c the new fs primitives. 2a leads with the two defects it closes on main
today (an LSP-authored delete that destroys unsaved work; a workspace-edit
phantom buffer), neither of which needs dired to be worth fixing. Named
for the substrate per #161's precedent. §10 states the cost: three review
cycles, and 2a ships nothing visible.
Cleanups: item 35→40 (now 41), acceptance 27→30 and 28→32 (now 33), and
the §10 table's obsolete rename-only-Rust description, replaced by a
per-PR breakdown of what each actually carries.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
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.
Four blocking, two high, four cleanups. Round 2's real finding: rev 2
widened the rename fix into a resource transaction, and four of the
consumers it named were not actually reachable by it. All six
substantive claims verified against c8ec8f3.
G1 — acceptance 29 was unimplementable. apply_workspace_edit captures
origin as a STRING (active_buffer_path is pmacs.editor.file_path,
lsp.lua:471-473), so no transaction reaches it and the phantom survives.
The applier itself changes: capture the buffer handle, restore with
switch_buffer, and no path fallback — restoring nothing beats inventing
a file that does not exist.
G2 — the dired subscriber could not rename its own buffer. dired.lua's
module doc says there is no pmacs.buffer.set_name, which is exactly why
Stage 1 chose buffer-per-directory. Rev 3 adds the setter (Q#DR21):
Buffer::set_name already exists and already documents itself as for
"rename operations", §5 needs it anyway for the Buffer.name half, and the
alternative — kill/recreate plus window replacement — loses placement,
cursor, intercept, round-trip input, and mode.
G3 — rec.uri was not the last LSP owner. DiagnosticView captures its URI
at construction and its own field doc anticipates this ("M5 may add
re-rooting if a buffer is renamed", diag.rs:455-457); five more stores
are URI-keyed. §5 now carries the ordered contract: flush pending
didChange, didClose, drop all five stores, re-run ensure_server, didOpen,
re-root the view per window.
G4 — Q#DR18 had no seam and was racy across the prompt. apply_resource_op
kills via find_by_path: raw path, first match, no descendants, no
modified check — it destroys unsaved work today. Rev 3 defines one shared
reconcile_delete called by both paths, harvests remove in the drain like
rename (so fire-and-forget reconciles too), and rechecks modified state
immediately before each syscall, since another frontend can edit while
the prompt is open. The policy stays asymmetric on purpose: dired refuses
the entry, an LSP-authored delete still removes the file but no longer
destroys the buffer.
G5 — w had no surface and the wrong semantics. push_entry is local and
copy() requires a region. Adds pmacs.killring.push (Q#DR22) with copy()'s
own semantics including breaking the kill chain, and makes w SET-BASED:
the parent approved the binding and Emacs copies marked filenames, so
rev 2's point-only narrowing was an unapproved change of its own. R is
now the only point-based operation.
G6 — R's no-clobber was only a preflight. rename_blocking calls plain
std::fs::rename, which silently replaces. The claim is narrowed to a
TOCTOU-bounded preflight refusal, acceptance 12 reworded to promise only
that, and a no-replace primitive named as deferred.
G7 — lsp_multi_root added to the gates, the §13/§7 slips fixed, and the
"2a's only Rust is the rename rebind" line corrected: it is now a rename
and delete reconciliation, two hooks, two new public surfaces, an LSP
teardown contract, and an applier change. §10 says so, and names the
further cut if that is now too large for one PR.
Acceptance renumbered flat (46 items) and the bite obligations are now a
table of eleven item/mutation pairs, three of them round-2 additions
where rev 2's design would have passed a weaker test.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
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>
`m4_5_initial_config_pushed_via_did_change_configuration` fails
intermittently on macOS/lua54 with a truncated payload, observed in CI as:
the daemon pushed the configured settings after initialized: {"rust":{"probe":
This is a real read-while-writing race, not a platform quirk. The wait
predicate was weaker than the assertion it guards: the pump waited for
`contains("probe")` while the assertion needs `"probe":true`, six bytes
further on. The sink is JSONL written by a separate process, so the test
could read a half-written line. Linux wins that race reliably; macOS does
not.
Wait for the trailing newline instead. `src/bin/pmacs_fake_lsp.rs` writes
the sink with `writeln!`, one record per push, so a trailing newline is
true only once a whole record has landed — it waits for exactly the unit
the assertion reads, and stays correct if the payload's field order or
spelling ever changes.
Note this cannot be falsified locally: reproducing it means losing a
scheduler race that Linux wins, so a passing local run is a regression
check rather than proof. The argument is structural — `writeln!` is the
only writer of this file.
The sibling `rooturi` sink test has the same weak-predicate shape and is
deliberately NOT changed, with a comment recording why: waiting for the
expected value there would convert a genuine regression — `rootUri`
falling back to the cwd, which its `assert_ne!`s exist to catch — into a
five-second timeout with a misleading "server didn't initialize?"
message, trading a precise diff for a vague hang. Closing it properly
means giving that sink a record terminator in the fake server, and it has
never been observed failing, so it is a separate change.
Gates: `cargo fmt --check` clean; strict workspace Clippy clean;
`m4_acceptance -- --skip basedpyright` 121 passed; the previously-racy
test 10/10 in isolation; `git diff --check` clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
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.
Seven findings, two blocking. Every checkable claim was verified against
c8ec8f3 before being acted on; all seven held.
F1 (blocking) — the rename contract reached one path owner. Verified the
other four: Buffer::set_name documents itself as for "rename operations"
and set_buffer_path never calls it; rec.uri is cached per LSP attachment
and read at ~20 sites; dired's buffers are PATHLESS so no buffer-keyed
rebind can reach them; and the workspace-edit origin restore does not
fail gracefully — find_or_open on a renamed-away path hits
resolve_target_buffer's NotFound arm, which creates an empty path-backed
buffer, so it materializes a phantom at the obsolete path and selects it.
Rev 2 replaces the rebind with EditorCore::reconcile_rename — whole
registry, equality-or-path-component prefix, updates file_path AND name,
called by BOTH the async drain and apply_resource_op so the two cannot
drift — plus a new resource.renamed(old, new) hook so path-keyed Lua
consumers reconcile. lsp.lua recomputes rec.uri, issues didClose/didOpen,
and re-runs ensure_server because #161 keys affinity on project root, so
a cross-root move needs a different server. dired.lua follows its
handles. Verified the ordering the design needs already holds:
_async.tick calls _tick() before resuming any coroutine.
F2 (blocking) — deletion of visited paths had no policy. New §6 decides
all four cases. An unmodified visited buffer is killed; a MODIFIED one
refuses that entry, deliberately diverging from Emacs, because an
orphaned buffer is indistinguishable from a normal one and the next
C-x C-s silently resurrects the file. The check runs before the confirm
so the prompt states the skip. Adds a symmetric resource.deleted hook.
F3 (high) — the key table silently changed approved scope. The parent
lists `w` and contains no `M`. Restored `w` (Q#DR20); `M` is now an
explicit new-scope decision (Q#DR19) that REFUSES symlinks, since the
parent already ruled that the fixture's symlink-perms rejection "carries
over unchanged" and rev 1's warn-after-the-fact contradicted it.
F4 (high) — Q#DR13 contradicted the R contract. Narrowed to three
classes: set-based (D, M, C), flag-based (x), point-based (R, w).
F5 (high) — five falsifying acceptance items added, and the bite matrix
now names six mutations including "dispatch-all-then-await" and "add a
completion source to confirm".
F6 (medium) — take_settled_renames was underspecified. Took the
reviewer's preferred shape: tick returns a structured TickOutcome so
settle identity and rename metadata stay in one transaction.
F7 (2b) — defined the full C command flow with an up-front collision
scan and one confirm (declining copies the non-colliding entries), pinned
remove_dir_all's lstat safety at the primitive, and stated
dired.recursive-deletes as boolean/default false.
Not done, and said so: R is not widened to the marked set. Multi-file
rename needs a target-directory concept that does not exist, so R stays
point-based and is NAMED as a class rather than left an unstated
exception.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
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.
The inline-math slice landed while this PR was open. Its own merge
removed its ledger lane, so the stale-header note above still names
exactly two; only the base anchor needed moving.
Continues docs/dired-framing.md, whose §§6-7 carry the approved shape of
marks and operations. This re-verifies every claim in them against
main @ c8ec8f3 — Stage 1 changed three of the files Stage 2 leans on
most — and adds what the parent did not decide: the batch-execution
contract, the confirmation surface, the staging cut, and acceptance.
Decisions continue the Q#DR scheme from Q#DR12.
Five corrections to the parent, one load-bearing:
- The rename rebind belongs in the drain (the parent's decision, kept)
but CANNOT be implemented in `AsyncRuntime::tick`: AsyncRuntime has no
buffer registry and no core. The seam is `pmacs._async._tick`, one
layer up, which already has `lua` in scope. AsyncRuntime harvests, the
binding rebinds.
- Line references drifted (tick 991 -> 1003, the FsUnit arm 1022 ->
1046, apply_resource_op's raw lookup 3248 -> 3249).
- The frozen fixture has NO mark-and-operate layer — eight commands, two
keys, and its "marks" are wdired text-position marks. So Stage 2 has
no in-repo reference implementation, which the parent's "45 tests pin
dired/wdired behavior" reads as implying it does.
- No y_or_n exists anywhere, and there is no runtime minibuffer.lua at
all — pmacs.minibuffer is Rust-only.
- `remove_blocking` already deletes files AND empty directories, so
`remove_dir_all` is needed only for non-empty ones. This is what makes
the staging cut possible.
Also carries a verified pre-existing defect, confirmed by probe rather
than inferred: a fire-and-forget non-stream job leaks its pending entry
forever (only stream eviction and take_result remove entries, and the
Lua handle has no __gc). Named as a deferral. The same probe establishes
that a settled job IS still readable at drain time, which is what makes
the rebind design sound.
Recommends splitting Stage 2 at the "needs a new Rust primitive" line:
2a is the mark layer plus d/x/D/R/M on the five ops that already exist,
plus the rename correctness fix; 2b adds mkdir/copy/remove_dir_all and
+/C and recursive delete. The reasoning is that 2a's only Rust is the
rename rebind, whose design is subtle enough to deserve a reviewer's
whole attention.
Coherence impact per COHERENCE.md §20 is stated in §0.5, including the
honest part: Stage 2 must add a `rename_paths` field to `PendingJob`,
which is a one-off where §9 wants a general owner/purpose — though a
side map, the alternative, is worse by §9's own diagnosis of the
parse-job link. 2b grows the closed JobKind enum 12 -> 15.
Touches only this file: docs/active-work.md and docs/agent-handoff.md
are held by the open docs PR #169.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
`main` moved through #158-#166 (Lean 4 Stage 2, COHERENCE.md, find-file,
the dired framing and Stage 1, the GPU terminal input fix) while this
documentation branch waited. Both required docs conflicted; neither
conflict was a code signal.
Resolution:
- `docs/active-work.md`: main's ledger is the base — every lane it has
gained since this branch was cut is kept verbatim. Only the
bottom-panel lane is replaced with this branch's "Stage 1 MERGED;
Stage 2 (GPU band) is next" section, and only the bottom-panel entry
is added to "Closed since the last snapshot".
- `docs/agent-handoff.md`: main's version is the base. This branch's §1
bottom-panel bullet, its §1 roadmap Arc 7 entry (which also records
that DAP is now unblocked), and its four §5 ops lessons are inserted
at their anchors.
One repair rides along. Main's `docs/agent-handoff.md` carried a
garbled fragment at §1: a duplicated, truncated "GPU initial target
LANDED — #148" bullet whose body was the tail of the old head-of-`main`
anchor bullet, leaving the `SUPPORTED=[6..=20]` protocol enumeration
orphaned mid-sentence. The fragment is removed and the enumeration is
restored as its own bullet.
No code changes; the merged tree's non-doc content is main's.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Framing Q#LN7, Q#LN8, Q#LN16; acceptance 22–28, 24a/24b, 35, 36, 36a, 37.
Stacked on Stage 3a (#167), whose notification/response seams and
`pmacs.fs.canonicalize` this consumes. No protocol change; the only Rust
outside the test helper is one `include_str!` line.
**The Lake-aware root (Q#LN8).** `pmacs.project.detect` cannot express
this rule — it is innermost-wins by construction, and a Lake package's
`lean-toolchain` sits at the outermost level, so a file under
`<pkg>/.lake/packages/dep/` belongs to `<pkg>`'s server rather than
`dep`'s. The resolver walks up collecting markers and returns the
outermost, stopping at `pmacs.project.search_boundary()` so a stray
marker above a fixture cannot leak in.
Two things about the marker test are easy to get wrong in opposite
directions, and both are pinned. `io.open` **succeeds on a directory**,
so a truthiness check accepts a `lean-toolchain` directory; but
requiring a non-nil read rejects an **empty** `lean-toolchain`, which is
a legitimate marker — `locate-dominating-file` semantics are existence,
not content. The discriminator is `read`'s second return: decline only
on a non-nil error. Acceptance 24a and 24b each fail against the
implementation that satisfies only the other; both bites are recorded.
The root is canonicalized once up front, because a configured root
reaches `file_uri_for` verbatim and that URI is the affinity key (#161).
Canonicalizing the starting directory suffices — every ancestor of a
canonical path is canonical, since the walk only strips components.
**`lake serve` with a lazy probe and a one-shot latch (Q#LN7).** Nothing
runs at init: `pmacs.lsp.config` is declarative, and spawning a process
at startup for every user, Lean-using or not, is the cost rev 1 refused.
Both the probe and the server spawn are gated on a real Lean attachment.
The probe cannot gate the first attach — there is no blocking process
run, so its verdict arrives after `ensure_server` has already decided.
Hence the optimistic spawn, with the probe and latch correcting it. A
non-zero probe exit is deliberately NOT a trigger: §2.9's elan-shim case
makes `lake --version` fail on machines where `lake serve` still works,
and the server-failure latch covers that better. The probe answers only
the question failure detection would answer slowly — an old-but-working
lake that starts a useless server.
The latch stops the failing server **before** spawning the fallback, and
that ordering is load-bearing rather than defensive: the spec default is
`OnCrash`, the termination handler never consults the exit code, and
`maybe_restart` has no attempt ceiling, so a broken `lake` respawns
forever underneath the latch. `pmacs.lsp.stop` sets `restart = Never`,
which is what disarms it. Bitten: removing the stop fails acceptance 36.
The swap rewrites `command` and `args` only, so a user's `env`,
`settings`, `init_options` and `root` survive — a wholesale table
replacement would discard their `init.lua` at the moment they are least
likely to notice.
**`waitForDiagnostics` (Q#LN16)** resolves through Stage 3a's response
seam, with `M-x lean.wait-for-diagnostics` on top. `$/lean/fileProgress`
subscribes on the notification seam and is pinned end-to-end through a
new `leanprogress` mode on the fake server rather than by calling the
handler directly — the wiring is the only part that can break.
**Attribution (COHERENCE §9/§1.2).** The probe spawns as
`lean:lake-version-probe`, so a user wondering why their editor touched
`lake` finds an owner in `pmacs.process.list`. The latch reports through
`pmacs.editor.set_status` — the channel that exists — and acceptance 36a
observes that channel, so a report made only through the undefined
`pmacs.error` would fail it.
**Stage 1's acceptance 12 is updated, half superseded.** It asserted
`pmacs.lsp.config.lean4 == nil` to guard against a Stage-3 front-run;
Stage 3b is that stage, so keeping it would pin the opposite of the
intended behavior. The half that survives is the one about restraint,
and it matters more now: constructing an editor spawns nothing even
though the config exists and names `lake`, and opening a Lean buffer
with no server configured spawns nothing either. That is what holds
Q#LN7's "not at init" promise.
Bites recorded, all against the committed tree: bare `io.open` -> 24a
fails, 24b passes; require-non-nil-read -> 24b fails, 24a passes; no
canonicalization -> the symlink case spawns two servers; no stop before
fallback -> acceptance 36 fails.
#165's own commits could not update the handoff snapshot to name the
merge that contains them, so the protocol obligation lands here.
- `docs/agent-handoff.md`: absorb the dired lane into §1, replacing the
placeholder that promised exactly this. The bullet carries Stage 1's
durable substrate facts — why the tolerant `read_dir` had to be Rust,
why exposing the core normalizer beat mirroring it in Lua, the
fixed-width `_layout` contract Stage 3 reads offsets from, the
ambient-action buffer guard, treating a failure as the answer instead
of probing, the per-entry error cap, the first mode-scoped keymap and
the pre-existing test it broke, and the dedication a descent does not
carry. Refresh the head-of-`main` anchor and the last-updated line.
- `docs/agent-handoff.md` §5: two ops lessons that cost real time. A fix
must be committed before it is bitten, because `scripts/bite` restores
by `git checkout --` and reverts to HEAD; a CONFLICTING PR runs no CI
at all, because `pull_request` workflows build a merge ref GitHub does
not create while the branch conflicts, and nothing reports the absence.
- `docs/active-work.md`: remove the merged lane per update-protocol rule
4 and summarize it under "Closed since the last snapshot", keeping the
two forward items Stage 2 needs (the rename rebind is first-match-only
over a raw path, and Q#DR5's seam is the main-thread drain). Refresh
the canonical base. Flag the two lane headers that still call a merged
PR "IN REVIEW" — #161 and #166 — rather than editing lanes another
thread owns.
- `COHERENCE.md`: #165 is no longer a PR. Per §25 the audited claims this
work changed were updated when it landed; this corrects their tense in
seven places and the two prose lines that still asserted dired was in
flight.
- `docs/dired-framing.md`: status line to MERGED, and state plainly that
Stages 2 and 3 each still need their own framing.
Docs only; no code, no gate-relevant change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0126d2sikA6jZpFin3rtLCSK
Third merge of main into the lane, at b889873 (GPU terminal input #166).
Unlike the first two this one produced NO conflict -- and it is the case
that shows why a clean git merge-tree is not a reason to skip
integrating. #166 lands 41 lines in pmacs-gpu/src/main.rs, the same
heavily-rewritten file as the first integration; the two edits merged
silently only because they sit in different regions of it (#166 is
entirely in the headless probe, this lane rewrites the render path).
Merging the PR on that clean auto-merge would have shipped a combination
no gate had run.
Reconciliation, run against what #166 actually added rather than against
a pass/fail: it adds 3 library tests, 2 to vterm_stage3_acceptance, and
0 to pmacs-gpu. Predicted lib 1,826 -> 1,829, CRDT 2,003 -> 2,006, GPU
unchanged at 202; that is exactly what ran. Suite count 91 -> 92 is
#161's new lsp_multi_root_acceptance binary. All three sides' markers
verified live in the shared file.
Also records an ops trap that cost hours this session:
m4_5_basedpyright_initializes_and_negotiates_encoding does not time out,
it hangs forever, parking a --workspace sweep at 38 of 92 suites with a
live basedpyright langserver child. The per-suite M4 gate already skips
it; the workspace sweep needs the same flag.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
The lane opened in the previous commit was scoped to the Vterm Stage 3
acceptance. Measuring it properly shows the problem is much larger and
not vterm-specific.
Comparing cargo test --list under CI's exact flags against the same
flags plus crdt: 3,024 versus 3,288. 264 tests are dark in CI, and the
single worst line is the library itself at 177 -- cargo test --lib
--features crdt is a required local gate that CI has never run. Ten
suites run zero or one test, including gpu_initial_target (#148's entire
acceptance, 1 of 14), gpu_invocation (#141's, 1 of 14), and a37, the
Stage 3 real-daemon/real-PTY/real-wgpu path that #135 built precisely
because a decoded-message fixture would prove none of the three fit
together.
The lane now carries the per-target table, the verified flag combination
for the fix, a two-part fix shape (a crdt leg on the test job, plus the
GPU-requiring suites onto the existing gpu-render job that already has
lavapipe), and an explicit instruction to sort deliberate exclusions
from accidental ones first -- some of the 264 are perf suites that are
ignored by default and belong to their own jobs, while m10_10_perf has
no ignore attribute and no job naming it.
docs/vterm-framing.md gains an as-framed audit section. The arc is
structurally complete and every test named in the Stage 2 verification
map exists, but criterion 22's "without thrash" clause was never pinned
anywhere -- the word appears nowhere in src or tests -- and that clause
describes exactly the defect #166 fixed. Of the nine Stage 3 tests, only
three drive a real daemon, so the six that construct EditorState
directly could never see a dispatcher-loop defect; a31 passes on the
broken tree for that reason. Four of the nine, including a37 and Stage 3
review round 1's own presence regression guard, do not run in CI at all.
The section also records what was not audited: section 11's blanket
claim about deferral safety covers roughly twenty items and none were
spot-checked.
docs/gpu-terminal-input-framing.md scores bet B2 true now that the
reporter has confirmed typing works, and retracts Q#GT5. The bash fixture
behind it does not reproduce in real use and was almost certainly
measuring its own timing rather than a product behaviour; it is marked
retracted rather than deleted so nobody re-derives it from an earlier
revision.
docs/agent-handoff.md section 5 gains the lesson the confirmation cost:
a daemon-side fix is not deployed until the daemon is restarted from a
tree containing it, and rebuilding a binary does nothing to a running
process.
No code changes.
CI round 1: both macOS jobs failed on the acceptance case added last
commit. APFS enforces valid UTF-8 in filenames, so `std::fs::write` with
a 0xFF byte in the name fails with EILSEQ ("Illegal byte sequence")
before `pmacs.fs.canonicalize` is ever called. The fixture cannot be
built there.
That is a filesystem refusing to represent the case, not a behavioral
difference: the subject — `to_str()` returning None for a non-UTF-8
resolution — is platform-independent Rust, and the Linux run pins it.
`#[cfg(unix)]` was the wrong granularity; review had asked for unix
gating on the symlink tests and I applied the same gate here without
checking whether the filesystem, rather than the API, was the
constraint.
Gated `#[cfg(target_os = "linux")]` with the reason in place, rather
than skipped at runtime, so a future failure here is a real failure and
not a silent no-op.
Ledger records both CI-round facts: this one, and that
`composition_overhead_under_ten_percent` is load-sensitive under a
parallel workspace sweep (it reported -4.6% realistic overhead in the
same run that tripped its 10% budget at 18.8%, which is noise, not work).
Levi Neuwirth