One conflict, in `docs/active-work.md`, and it is adjacency rather than
disagreement. PR #186 inserted its lane block directly above the dired
Stage 2 lane heading; revision 9 rewrote that heading from "OPEN, STALE,
DO NOT MERGE AS-IS" to "AT REVISION 9, AWAITING APPROVAL". Git saw a
rewrite abutting an insertion and could not tell they were independent.
Resolved as both, in order: #186's lane block kept intact, followed by
revision 9's heading. Verified in both directions rather than by
inspection — the resolved file removes zero lines relative to this
branch's tip (8f42826), so nothing of revision 9 was dropped, and
differs from main only in the dired lane, so nothing of #186's was.
Note for whoever refreshes the ledger next: the #186 lane block this
merge preserves still reads "OPEN, PROPOSED, DO NOT MERGE". That was
true when main recorded it and is not true now — #186 merged as
0f4e9e0. Removing a landed lane is legal only once its facts reach
`docs/agent-handoff.md`, so it is left alone here rather than
relabelled, per the ledger's own rule.
No framing content changed. No runtime code.
Resolve review round 8 by making the withdrawn resource ordering
contract singular, assigning every revision-8 acceptance item to 2a,
and specifying one exact-pair LSP tombstone lifecycle.
Replace name/path equivalence with explicit buffer-name provenance,
pin both uncorrelated state creators and tombstone reclamation, correct
the independent-order test's bite, and refresh the active-work lane.
Review round 4 accepted the core design and the two surfaced choices,
then found two remaining contract defects and one ledger-ownership
defect. Close all three without starting runtime implementation.
Narrow the last normative "always answers" consumer to Q#RD7's honest
"always attempts while the response channel remains live" contract.
Strengthen the audit procedure to search normalized prose and term
stems so Markdown emphasis cannot hide a consuming site from a literal
phrase sweep.
Replace Q#RD12's incomplete no-op/clear/conflict table with a total
no-op/clear/refuse verdict exposed through one named internal binding.
The shared Rust helper now has an explicit mapping for missing with and
without ignore, non-NotFound stat errors, modified buffers, and
editing-in-progress buffers. Specify how both the primitive and Lua
preflight consume the same result. Add acceptance 11c for known
NotFound before earlier batch mutation and 11d for fail-closed stat
uncertainty.
Stop rewriting #171's lane from #186. Restore the sibling block exactly
to main, retain only the stable cross-lane ownership split, and record
that #171 owns its volatile state. Sequence #186 before #171 because
the urgent data-loss guard is the dependency #171 adopts, not to make a
textual conflict cheaper.
Correct #186's own ahead count to include this revision commit and add
the previously omitted lsp_dispatch_seams_acceptance file to the lane's
touch list.
Still PROPOSED. No runtime code. Implementation begins only after
explicit user approval.
Review round 3 accepted the core --- pre-filesystem refusal, four-phase
ordering, the #171 split, Q#RD10 --- and raised four P1s and a P2. All
accepted.
The external-claim audit added in revision 3 certified this document as
clean while Q#RD3, the normative decision, still asserted the very LSP
claim the audit's own row 4 marked WITHDRAWN. It did so because it
checked each claim where it was DEFINED and never at the sites that
CONSUMED it, so a withdrawal recorded in one section coexisted with the
same claim doing load-bearing work three sections away. That is a defect
in the audit procedure rather than a missed line, and since the table is
now an artifact readers trust, section 1.15 records both the failure and
the corrected procedure: grep the whole document per row and check every
hit.
P1, lane state. Re-measured: `git rev-list --left-right --count
fd7ae37...7586905` returns `13 2`, so #171 is two commits behind, not
zero, and those two are exactly PR #189's COHERENCE change. Revision 3's
"0 behind" was taken against `ad41cf1` and reported in present tense
after main had moved. Both ledger lane entries are corrected in place
--- #186's revision and base, and #171's superseded `ab42a79` /
153-behind / merge-base-`c8ec8f3` ground truth --- rather than having a
correction layered above stale text, which is what made the ledger
self-contradicting. Every count now appears as pasted command output.
P1, withdrawn claim surviving. Q#RD3 called partial application
`FailureHandlingKind.Abort`, "the strategy the spec itself assigns to
any edit containing resource changes", and section 1.11 called `Abort`
the default "by omission". The spec establishes no default for a client
advertising no strategy. Both sites now say only that verified pmacs
behaviour resembles abort-style application, resting on the reproduction
in section 1.6.
P1, acceptance 15. `WorkspaceEditResponse::from_lsp_value` returns
`Self`, its doc says a shapeless result yields an empty response, and
the binding's only `?` is `lua_to_json` over a value that arrived
through `json_to_lua` --- so no server payload can make the parse fail
and the criterion could not fail. Decision, new Q#RD11: keep the wrap,
drive the test with an explicit throwing stub, label it defensive.
Q#RD7's promise narrows to "always attempts a response while the
response channel remains live", since `send_response` is itself under an
ignored `pcall`.
P1, absent-plus-ignore. `pmacs.fs.stat` dispatches async and
`canonicalize` resolves symlinks and returns nil for a dangling one, so
it disagrees with the primitive's `symlink_metadata` on exactly the
input this query turns on. New Q#RD12 specifies a structured Rust-backed
verdict --- no-op / clear / conflict --- evaluated with the same
`symlink_metadata` call, with an error contract that fails toward
refusal. New criteria 11a and 11b supply the missing opposite direction.
P2. Criterion 14's "fails in both directions" was false: with both
duplicates clean the setup cannot distinguish first-match validation
from full validation. The claim is fixed rather than the setup, because
criterion 6 already pins validation breadth. Section 8's touch table and
section 7's gate list are reconciled.
Sweep for corrections applied at one site while a dependent site kept
the old claim: count 4 --- the two `Abort` sites above, and the stale
#171 count in both the revision history and section 1.12. Nine other
withdrawn or revised claims were checked at every consuming site and
found clean.
Still PROPOSED. No runtime code. Implementation begins only after
explicit user approval.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
All seven citations re-verified against the tree; all seven hold, one is
understated. The split with #186 is untouched.
Revision 7's process read every mechanism it CITED but never read the
mechanisms it RELIED ON: it verified that tick exists and returns
settled ids without reading that the drain is a bare try_recv with no
execution token, and it verified that kill_buffer exists without reading
the order in which it mutates before it can refuse. Reading a symbol to
confirm it is there is not the same as reading it to confirm it does
what the surrounding argument needs.
F1 — reply order is not execution order. AsyncRuntime::tick
(src/async_runtime.rs:1003) drains the reply bus with no execution
token, so a worker can finish, be descheduled before sending, and have a
later reply arrive first. Asked the cheaper question first as directed:
reconciliation does NOT need to be order-dependent. Independent
mutations commute; interdependent ones cannot arise from any production
path (dired serializes, apply_resource_op is synchronous, the fs
primitives have zero production callers); and fs.lua:155-165 already
instructs callers needing ordering to serialize. So the guarantee is
withdrawn rather than engineered. A token under a mutation lock was
rejected: it serializes every fs mutation to close a hazard with no
production reachability and a documented caller-side remedy. No static
ordering rule is offered because none works — worked through in §6.
F2 — preflight, and the review understates it. kill_buffer clears
round_trip_buffers, closes side windows and redirects ordinary windows
before BufferRegistry::remove can refuse. Rev 7 said to treat the
refusal as "keep the buffer", which reads as though skipping phase 2
restored something; it does not. reconcile_delete now preflights
editing_in_progress — sound because phase 1 is pure EditorCore with no
Lua handle, so nothing can re-enter between check and removal.
Acceptance 53b is three separately-asserted properties, each with its
own named bite.
F3 — path-equivalence, not string equality. Names come from
path.display() as given while only file_path is normalized, so a
relative open leaves a short name a string rule mistakes for
user-chosen. Tested both directions; the custom-name arm is what stops
the fix becoming a name-clobberer.
F4 — bounded tombstone, and the census corrected this revision's own
first answer. A first pass checked only handle_notification and
concluded publishDiagnostics was the only uncorrelated writer. Wrong
lens boundary: mark_document_stale takes no LspServerId and creates URI
keys across three stores for every server. The full census also found
that diag_store has zero correlated writers and that
DiagnosticStore.by_uri is keyed by URI alone with no server component —
so the store most needing protection is the one a route purge cannot
help, and a (sid, uri) tombstone would not match it. Recorded as the
round's own defect class occurring inside the round.
F5 — three outcomes, because pmacs.minibuffer.read already has three.
Cancel does not fall through to on_no: for C, declining means copy the
non-colliding entries while cancelling means abandon, and conflating
them would make C-g perform a partial copy.
Sweep for the same defect class: three candidates, two cleared by
reading (run_all_must_succeed really does collect and not abort;
commit_to_refuses_an_await_and_restores really exists), one real and not
raised by review — the framing never said which HookKind the new hooks
register with, and short-circuit would let one subscriber silently stop
every later one reconciling. Both are now all-must-succeed.
P2: pmacs.lsp.forget_uri named with an error contract and pinned; the
ledger note rewritten — it claimed single-file scope while that same
revision edited the ledger — with both line counts measured at this tree
rather than quoted.
Status unchanged: PROPOSED, needs explicit user approval. No runtime
code. Do not merge.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
Review round 2 confirmed everything central from round 1 as fixed and
raised four P1s. All four accepted; both requested sweeps run. Rebased
onto `7586905`.
P1-1, the ownership boundary was stale. Revision 2 described PR #171 as
"OPEN, STALE, 153 commits behind, under re-scout" claiming the rename
side only. Re-checked directly: #171 is at revision 7, `fd7ae37`,
merge-base `ad41cf1`, zero commits behind, and its revision 6 had
assigned rename AND delete to Stage 2a with the opposite policy --- file
deleted, modified buffer kept alive and orphaned, that orphaning named
as accepted residue. Two lanes, opposite answers, same event. The
settled split is now carried verbatim in the framing and the ledger, and
#171 revision 7 has adopted it from its side.
P1-2, the LSP failure-handling claim was wrong. The spec does not assign
`Abort` to resource-op-bearing edits. Recovery is described by the
client's advertised `workspace.workspaceEdit.failureHandling`; `Abort`
is one of four strategies, `Transactional` covers all operations, `Undo`
attempts rollback, and only `TextOnlyTransactional` degrades to abort
when resource changes are present. pmacs advertises none, so the spec
assigns pmacs no strategy at all. Section 1.7 and B2 now rest on
verified repository behaviour --- the reproduced partial batch --- not
on borrowed protocol authority.
P1-3, Q#RD7 had no implementable seam. Three gaps confirmed by reading:
`_parse_workspace_edit` is called one line above `apply_workspace_edit`
and is fallible, so the proposed wrap left "always answers" untrue;
`append_to_errors_buffer` is private and a Lua preflight rejection never
reaches Rust, so the promised logging was not implementable from where
it was promised; and acceptance 13 tested the response but not the
trace. Q#RD7 is rewritten around one seam at the server-request
boundary, and of the two options offered this revision picks wrapping
parse-plus-apply rather than narrowing the claim.
P1-4, clean duplicate reconciliation is now Q#RD10: validate every
match, reconcile today's first exact-path match only. Widening would
enlarge the parked lifecycle defect Q#RD5 exists to contain; the
surviving clean duplicate is named as residue handed to #171.
External-claim sweep. Every non-repo claim is now listed in a new
section 1.15 with its evidence. One was a paraphrase standing in for a
quote: "in Emacs `kill-buffer` on a modified file-visiting buffer
prompts". It is true, but the gate is `INTERACTIVE`, defined as
`(NILP (Vexecuting_kbd_macro) && !noninteractive)` --- keyboard present,
not `call-interactively` --- so eglot's programmatic kill does prompt in
a normal session and does not in batch or during a keyboard macro. The
revision 2 sentence was right for a reason it never established and
false in two environments it never considered.
Cross-lane sweep. Q#RD8 said mode (d) needs its own lane; it has one now
--- #171's `reconcile_delete` composes both removal phases. Q#RD6 claims
the shared walk query explicitly so the duplicate resolves in one
direction. And `pmacs.fs.remove`, guarded by neither lane and verified
to have zero production callers, is named as explicitly out of scope
with its owner rather than left to read as covered.
Still PROPOSED. No runtime code. Implementation begins only after
explicit user approval.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
Review round 1 approved the refusal strategy in principle and rejected
revision 1 as written. Six blocking points, all accepted, plus three
further overclaims found by the requested sweep. Q#RD1 and Q#RD5 are
settled yes; Q#RD9 is settled no and is withdrawn.
Q#RD2 conflated inspection with removal. Revision 1 removed the buffer
before the filesystem call, which fires arbitrary Lua `on_removed`
callbacks while the file still exists and accepts losing the buffer if
the deletion then fails. The sequence is now `stat/no-op -> enumerate
and validate -> mutate filesystem -> reconcile`. Validation inspects
`is_modified` and `editing_in_progress` without removing anything, so a
failed deletion leaves buffers intact automatically and `on_removed`
still observes the path already gone.
Q#RD3 overclaimed whole-batch atomicity. `documentChanges` are
sequential, so an earlier edit can dirty a clean buffer and an earlier
rename can move a modified buffer into a later delete's subtree, after
the snapshot. LSP 3.18 assigns `FailureHandlingKind.Abort` to any edit
containing resource changes --- "all operations executed before the
failing operation stay executed" --- so the protocol itself declines to
promise what revision 1 claimed. The preflight is now described as an
early conflict check, with robustness coming from per-op `pcall`, an
always-sent server response, and best-effort origin restore.
The lookup cannot be `EditorCore::find_buffer_for_path`: it normalizes
but delegates to the first-match-only `find_by_path`, and
`pmacs.buffer.from_file` creates path-bound buffers with no dedup, so a
clean first match can hide a modified second. Q#RD6 now requires a full
scan with component-aware `Path::starts_with`.
Recursive deletion now inspects the tree but reconciles only the exact
path, so the parked lifecycle defect stays exact-path rather than
becoming tree-wide. Q#RD4 holds at both layers, so the preflight cannot
reject an absent path the primitive treats as a no-op.
The prompt argument was overclaimed and that was my error.
`pmacs.lsp.send_response` takes `request_id` as an ordinary value, so a
`workspace/applyEdit` can be answered on a later tick, and a callback
continuation would reuse the existing minibuffer shadow rather than add
a seventh dispatcher rung. Prompting is expensive and separately
scoped, not impossible; the section now claims only what the evidence
carries.
Sweep found three more of the same defect class --- an absence or a
guarantee asserted rather than established:
* a durable error surface does exist (`append_to_errors_buffer` ->
`*errors*`), so Q#RD7 now records the refusal there as well;
* no caller reliably surfaces a raise, because the async path routes
uncaught coroutine errors through the undefined `pmacs.error`;
* pmacs advertises no `workspace.workspaceEdit` capability at all ---
no `documentChanges`, no `resourceOperations`, no
`failureHandling`.
Adds seven acceptance pins with their bite obligations, adds the
`docs/active-work.md` lane the ledger requires for every open PR, and
drops the two-PR plan: #186 is revised in place and becomes the
implementation PR.
Still PROPOSED. No runtime code. Implementation begins only after
explicit user approval.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
PR #186 frames a guard for apply_resource_op's delete arm that refuses
before touching disk when any affected buffer is modified. Rev 6 said the
opposite for the same call site: the file is deleted, the modified buffer
survives orphaned, and §11 named that orphaning as accepted residue. Two
lanes, two answers.
Rev 7 adopts the settled split, recorded verbatim in the framing and in
the ledger lane so the two cannot diverge again: #186 owns the urgent
pre-filesystem refusal for synchronous apply_resource_op; #171 later owns
full post-delete lifecycle reconciliation, including the async race where
a buffer becomes modified after dired dispatch. Not re-litigated.
Census of orphaning claims: 20 matched lines resolving to 13 distinct
passages, classified by reading each enclosing passage rather than the
matched line. 4 ownership claims (this lane closes the LSP data-loss
defect) reassigned to #186; 4 policy claims (LSP intentionally deletes
and orphans) deleted; 3 ground-truth statements kept, because main really
does destroy unsaved work on that arm, but attributed to #186 as fixer;
2 async-race claims kept and narrowed.
Q#DR18 is rewritten, not withdrawn. The reconcile_delete seam survives
and is explicitly not cancelled. Three changes: the synchronous path
refuses before disk (#186 Q#RD1, adopted not re-decided); the policy
becomes symmetric rather than asymmetric; and the walk rule is adopted
from #186's Q#RD6 rather than reinvented — scan every path-bound buffer,
normalize once, component-aware Path::starts_with — which is
character-for-character what rev 6 wrote independently. Whichever lane
lands first owns the query, per #186's own boundary wording.
DeleteReconcile.kept_modified stays and is not dead. The synchronous
caller can no longer produce it; the asynchronous one still can.
Residue kept, and narrowed to one path: dired never goes through
apply_resource_op — it calls pmacs.fs.remove, which dispatches a worker
that an in-applier guard cannot see. So the LSP path has no residue and
dired's is its own. Rev 6 called it "one deferral, two paths"; that was
backwards. Also newly named: pmacs.fs.remove itself is guarded by
neither lane, since both guards sit one layer above it. Latent — zero
production callers.
The full post-delete lifecycle stays here, and #186 hands it over
explicitly rather than by omission: its Q#RD8 parks the window and
last-buffer defects and independently reaches rev 6's R4 finding that
kill_buffer and remove_buffer_and_fire clean disjoint sets; its Q#RD5
keeps reconciliation exact-path precisely so as not to promote those
defects tree-wide. That parked work is this lane's Q#DR27.
LSP failure handling: this document never made the claim — grep returns
10 lines, all about hook fan-out or dired's batch semantics, none about
WorkspaceEdit recovery. Verified the spec anyway and recorded it, since
the two framings will sit side by side: only textOnlyTransactional
degrades to abort for resource ops, transactional covers them, and LSP
3.18 states no default for a client advertising no failureHandling.
Rev 6's one adjacent claim — "refusing mid-edit leaves a half-applied
refactor" — was the load-bearing support for the deleted policy and goes
with it.
Noted without re-litigating: #186's Q#RD5 cites the ledger's "OPEN,
STALE, 153 commits behind, under re-scout" assessment of #171 in support
of taking the delete side now. That citation is stale — the re-scout is
done and this lane is integrated to ad41cf1 — but the conclusion stands
on urgency alone, so nothing about the split changes.
Status unchanged: PROPOSED, needs explicit user approval. Do not
implement, do not merge.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
Revision 5 was reviewed and not approved. Round 5 has one theme, not
six: rev 5 changed the slice split and the ownership of a decision, and
the prose did not follow. Four of the six findings are that same defect
in different places. All six verified against the tree before acting;
two are understated by the review.
R1 (P1) — rev 5 was superseded by its own ledger entry and by a PR body
older still. active-work.md:507 records Q#DR25 as moved out of this lane
(dired's paint is one instance of a CLASS bug — the same
erroring-intercept-over-writable-rope idiom is in listview, compile and
search/grep, and no Lua caller anywhere sets read_only because there is
no Lua set_read_only), while the framing still called it mandatory and
assigned it to 2b, and the PR body still described revision 1's
two-slice plan. All three reconciled: Q#DR25 is withdrawn, §3.1 becomes
a handoff to the generated-buffer-immutability lane, and the PR body is
rewritten. Also corrected in the other direction: rev 5's claim that
Q#DR25 "closes dired's quarter" of the §14 gap was itself wrong — dired
was never a quarter of anything.
R2 (P1) — acceptance allocation contradicted the code split, and the
review undercounts by one. Items 23-24 test apply_resource_op and the
drain harvest (2a substrate) but sat under a 2b header; item 33 needs a
dired.lua subscriber while 2a is defined as containing no dired code.
23-24 moved to 2a; 33 moved to 2b, because 2a's whole review rationale
is that its diff contains no dired code. The cost is stated: between 2a
and 2b a directory rename leaves dired handles stale, which is the
status quo and not a regression. The undercount: that leaves 2a shipping
resource.renamed with no acceptance, so item 50 pins the hook contract.
R3 (P1) — TickOutcome could not carry deletions. Replaced the two ad-hoc
vectors with one ordered Vec<ResourceOp>, and PendingJob carries a
single Option<ResourceOp>. Ordered because a directory rename and a
delete beneath it can settle in one tick; one enum rather than two
Options because two admit a both-Some state that cannot occur, the
argument ResolvedTarget's own doc makes at editor_core.rs:100-102.
R4 (P1) — reconcile_delete stopped short, and the substrate is worse
than the review says. Right that removal is two phases; what it does not
say is that NO existing Rust path composes them. pmacs.buffer.kill
(mod.rs:5476-5491) does, and its doc says it is late-bound precisely to
redirect windows — but apply_resource_op uses remove_buffer_and_fire,
which is phase 2 without phase 1, and BufferRegistry::remove touches
only buffers and order. So an LSP-authored delete leaves a displaying
window pointing at a removed id: a third defect on that arm. §6 now
specifies both phases, the last-buffer and ConcurrentEdit refusals, and
items 51-53.
R5 (P2) — the "every consumer" claim was false for Lean. The deferral
was right and the summary was wrong; fixed the summary. Stage 2 supplies
the hook, Lean's state stays stale until its owner adopts it.
R6 (P2) — pre-three-slice file inventory. minibuffer.lua joins
src/editor.rs's include_str! sequence, so 2b touches a Rust file; "2b is
dired.lua plus one killring binding" was false. + and C retagged 2c.
The sweep the review asked for caught four more stale labels it had not
cited: §4's "C (copy, 2b)", §7's "(in 2b) a recursive delete", §8's op
sections, and §8's d/x line — which was wrong in BOTH halves, saying 2a
where it meant 2b and 2b where it meant 2c, a pure two-slice-era
leftover. Historical round sections keep their original labels, flagged
rather than retconned.
The ledger lane rides this PR and is updated to match.
Status unchanged: PROPOSED, needs explicit user approval. Do not merge.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
The lane described the pre-re-scout state: head ab42a79, 1,570 lines,
"re-scout under way", and a five-owner rename census. All four are now
wrong. It rides this PR rather than a standalone refresh, because a
separate ledger PR with several others open re-conflicts on every merge.
What the lane now records:
- Head e7f811b, 2,304 lines, integrated to main @ ad41cf1, status
PROPOSED and never formally approved — four revisions and three review
rounds are not approval and must not be read as one.
- Seven of rev 4's own claims about pmacs were wrong. The load-bearing
one is kept in full because it is a trap anyone can repeat:
drain_external_cancelled (:1561) and drain_cancelled_externals (:1596)
are two different functions 35 lines apart, and rev 4 named one while
citing the other's line. Following the citation gives the per-tick
token sweep instead of the unconditional server-scoped drain, so the
drain half becomes a silent no-op and the awaiting coroutine hangs.
- The path-owner census is six, not five. The sixth is lean.lua's
M.file_progress, a URI-keyed Lua table in no Rust store, which is the
first evidence outside dired that the hook rather than the Rust method
is what scales.
- The journey ratchet is split across journey_acceptance.rs and
gpu_invocation_acceptance.rs; both are gates, and a scout checking only
the first concludes #183 added nothing.
- open_directory now commits under pmacs.window.commit_to, whose scope
refuses an await, which constrains the proposed batch contract.
Scope moved OUT of this lane: Q#DR25's adoption of
set_generated_contents turned out to address a class bug shared with
listview, compile and search/grep, so it is owned by the
generated-buffer immutability lane now. This PR needs a rev 6 deferring
Q#DR25 there once that framing is approved.
Also records two live bugs this lane confirmed but does not fix, both
owned elsewhere: apply_resource_op's delete arm destroying unsaved work,
and View still lacking rename_resource.
#174 merged while this PR was open, so the lane it had just been given
is already a merged lane. Rule 4 removes those rather than relabelling
them — but only once the durable facts are in the handoff, so do both
here in that order.
docs/agent-handoff.md
- §5 gains the lesson: a wait predicate WEAKER than the assertion it
guards is a race on whichever platform loses it, and "wait until the
file mentions X, then assert Y" races whenever Y is stricter than X.
- Two things that generalize past the fix ride with it: a race you
cannot reproduce can still be bitten at one remove (an unsatisfiable
predicate proves the wait is load-bearing; the old predicate still
passing proves a local run cannot tell them apart), and the obvious
fix is sometimes worse — the sibling m4_26 is deliberately left alone
because closing it the easy way trades a precise assertion diff for a
vague five-second hang.
- Header and §1 anchor advance to 0442d78, noting #174 is test-only and
#184 remains the substantive change at that head.
docs/active-work.md
- Remove the #174 lane; the header paragraph now says where it went.
- Canonical base and recovery floor advance to 0442d78. The floor
explicitly rejects 6bee09d as well as 7fd646d, per its own rule that a
check accepting an older commit than the declared base passes on a
tree the file does not describe.
- Bottom-panel lane: 2B-2 is IN FLIGHT, not merely "next" — branch,
worktree, and the fact it is branched fresh rather than stacked. Its
boundaries are restated because they are easy to overrun: production
Hello stays v20, panel_capable stays false, and 2B-3 may not simply
bump the unsolicited Hello.
- dired lane: the re-scout is under way on the existing branch, so #171
keeps its three-round history and the product is a rev 5.
- Both lanes note that main advancing to 0442d78 changes nothing for
them, since #174 is test-only.
The bottom-panel framing doc keeps its 6bee09d ground-truth line: that
is a scouting statement about what was actually read, and re-anchoring
it to a commit nobody re-scouted against would be a false claim.
Neither #174 nor #171 had any entry in this ledger. An open PR is
exactly the volatile work the file exists to record, so its absence is a
defect rather than a tidy omission — #171 drifted 153 commits while
invisible here, and its still-green old CI run describes a tree nobody
has looked at since.
#174 — M4 config-sink race, revived and regated. Records the predicate
fix, the gate numbers on the integrated head 302c21c, and two things
verified rather than inherited: the "one writeln! is the only writer"
argument re-checked against a fake_lsp that DID change upstream, and the
wait bitten two ways (unsatisfiable predicate fails on the pump deadline;
the old predicate still passes locally, confirming a green local run
cannot tell them apart).
#171 — dired Stage 2 framing, stale, do not merge as-is. Measured 4
ahead / 153 behind with merge base c8ec8f3, which is itself #165's merge
— so dired Stage 1 and find-file are its base, not new arrivals. Names
the three landed changes that move ground under it: #178's
generated-buffer write invariant (dired is a non-adopting writer),
#182's demotion of dired to a replaceable directory-handler slot, and
#179/#181's typed-edit consumer chain. Restates the five-path-owner
rename transaction the framing still has to answer.
Also records that three review rounds in a commit history is not the
same as approval, and that dired 2a's file overlap with Journey 1b needs
assigning before either runs.
PR #184 (bottom-panel Stage 2B-1) merged, but the four documents that
new work is supposed to start from still described it as open. Advance
every canonical anchor and close the one obligation that was blocking a
lane removal.
docs/agent-handoff.md
- §1's head-of-main anchor moves 7fd646d -> 6bee09d.
- State schema support and production advertisement as two separate
facts: SUPPORTED is now v6..=v21, the server-first Hello still says
v20, and #184 landed only the first.
- New §1 bullet for Stage 2B-1 carrying its durable substrate: the
server-first incompatibility argument, the shared wire_grid boundary
and why per-axis caps are a parameter, authoritative Absent, and the
panel_epoch / geometry_epoch split.
- New §1 bullet for the PTY terminate diagnostic (#176), plus two §5
ops lessons: a drain that ticks is not an observation, and how to
prove a child exited without waitid or unsafe.
docs/active-work.md
- Canonical base and the recovery floor both advance to 6bee09d.
- Remove the #176 lane. It was retained only because rule 4 requires
its facts to reach the handoff first; that move is in this commit, so
the lane goes.
- Rewrite the bottom-panel lane as 2B-1 MERGED with 2B-2 next, branching
fresh from landed main rather than stacking.
- Annotate the documentation lane with measured staleness (1 ahead, 320
behind) without deleting it, since nothing has decided its fate.
docs/bottom-panel-stage2-framing.md
- Status header records 2A and 2B-1 as merged and 2B-2 as next. No
revision bump: the header is landed state, and no design decision in
the document changed.
COHERENCE.md
- §16 names #184 as the PR that landed the reserved v21 family.
No runtime code, no protocol change, no gate suite implicated.
Capture the follow-up review finding, the evidence-driven completion
contract, the exact corrected CAT duration, and the proportional green
gate matrix at 9c79ce1.
Capture the exact review-fix and GPU probe checkpoints, the full green
gate evidence, and the classified sandbox-only socket failure in the
cross-machine active-work ledger.
Reserve the additive v21 panel schema without advertising it in the
server-first production handshake. Pin a real shipped-v20 client attach,
make the two aggregate-budget ratchets exactly one byte over, and update
the framing, coherence audit, handoff, and volatile lane record.
Record the complete post-#183 gate matrix for bottom-panel Stage 2B-1
at c8895a8 and mark the lane ready to open for review.
Retain the required-GPU first-pass classification: one unrelated math
render assertion failed, passed immediately in isolated single-threaded
execution, and the mandatory complete 202-test rerun passed.
Integrate main through the Journey/GPU directory-target ratchet (#183).
The public managed-GPU probe additions compose with the v21 wire layer.
Resolve the volatile ledgers to the landed state: advance the canonical
anchor to 7fd646d, remove the completed ratchet lane, preserve the
approved Stage 2 revision-5 recovery facts, and mark the integrated
2B-1 tree as awaiting its from-start full gate rerun.
Drive pmacs --gpu . through the root broker and real managed GPU
connector, keep the session alive through the asynchronous dired
replacement, and assert its canonical listing before daemon reuse.
Expose snapshot count and materialized text through the private
display-less acceptance probe so the public path is observable.
Consume the directory session's later replacement snapshot and assert
the canonical dired header plus a known listing entry before checking
daemon reuse.
Correct the bottom-panel revision-5 recovery branch and advance the
durable handoff to the Journey Stage 1a main anchor.
Capture the complete green gate matrix and retain the diagnosed setup
and transient full-sweep failures so the lane remains recoverable and
the evidence is not flattened into an unexplained rerun.
Replace the stale directory-negative in the GPU initial-target suite
with an explicit snapshot-first readiness path, while retaining all
genuinely malformed and unloadable failure cases. Record the portable
side-quest and bottom-panel dependency state.
Make the statusline and Vterm Stage 3 acceptance suites track the
bottom-panel v21 bump, including the real daemon and headless GPU probe.
Record the full gate result and the unrelated stale directory-target
assertion reproduced on canonical main.
Integrate the Journey Stage 1a merge without rewriting the already
reviewed protocol branch. Record the approved three-way Stage 2B split,
advance the canonical recovery anchor, remove the landed Journey lane,
and put 2B-1 into its full-gating state.
The ledger preamble already says Lean 4's merged lane was removed, and
the durable Stage 4b facts already live in the handoff. Remove the stale
section that still called Stage 4b in review so PR #182's post-merge
state is internally consistent.
Two open documentation PRs editing the same three ledger files
re-conflict on every merge to `main` — the treadmill #169 and #176 each
paid three resolution rounds for. #180 was docs-only and already
CONFLICTING against `main`; folding it here retires one of the two
writers instead of resolving the same file twice.
Also integrates `githubsucks/main` @ `42025e4` (Lean 4 Stage 4b #181).
Conflicts resolved, and three claims corrected rather than picked:
* **The head-of-`main` anchor.** Both sides named `74301d1`, which is no
longer true — `#181` has landed. The anchor now reads `42025e4` and
leads with it, in `docs/agent-handoff.md` §1 and the active-work
canonical-base line, and **the recovery floor moved with it**: the
`git log` check requires `42025e4` or newer, per that section's own
rule that a floor accepting an older commit than the declared base
passes on a tree the file does not describe.
* **The Lean 4 bullet contradicted the anchor I had just written.** Its
header still said "stages 1, 2, 3a, 3b LANDED" and its Stage 4b
sub-bullet still said "implemented and in review", while the anchor
above it now records #181 as merged. Both corrected: all six stages
landed, #181 named.
* **The COHERENCE §2 grade.** #180's side still carried "broken at step
3" / "Broken at entry" in both the ground truth and the §0 scorecard;
this branch's corrections win, since they are what the code change in
this PR makes true.
The removal note at the top of `docs/active-work.md` is reattributed:
the terminal config + copy mode lanes were #180's removal, and it now
says so and says why the fold happened.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A count is a reading, not a constant. Recorded as of rev 8 with an
explicit instruction to re-read rather than quote the line.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review round 1 of PR #182. One implementation gap and two stale claims.
**The scope pins the frontend; it does not pin the window.** Framing
§4.4 specified `display{ window = dest:window() }`, but dired's commit
still ended in `pmacs.window.switch_buffer`, which targets whatever
window the scoped frontend has selected. A split or panel that took
focus while `read_dir` was pending therefore received the listing, and
`prev` was captured from it too — with every preflight check passing,
because the captured window was still live and still held its captured
buffer. Both sites now read the captured window: `display` routes to it
with `select = true` (the later `seat_cursor` acts on the active
window), and the `prev` read asks it directly.
N4c pins both halves. The suite's existing routing pins all varied
*frontend* identity; none varied the selected window within one
frontend, which is exactly why 23 green pins missed this. Bite: dired's
`display` back to `switch_buffer` fails N4c alone; `prev` read from the
ambient window fails N4c alone.
Two stale documentation claims, both of which this PR was supposed to
have already fixed:
* **The §0 scorecard still graded §2 "Broken at entry"** while §2's own
ground truth had been rewritten. The scorecard is a second copy of the
same claim and §25's protocol covers both. §19's row and ground truth
were stale the same way — this PR creates the first cross-subsystem
suite, which §19 says should exist and grades as missing — and are
corrected too.
* **P4 still read "leaves exactly one buffer"**, the exact claim rev 6
corrected as false everywhere else in the framing. Restated to what it
actually pins: the file is in the *active window*. The test was
already written correctly; only the framing lied.
Framing rev 8.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Completes Journey Stage 1a: the `commit_to` acceptance suite (framing
§6 N4, N6, N6b, N6c, P1, P2, P3) plus the documentation updates
COHERENCE §25 requires the PR to carry.
Bite-testing the new pins found a real gap. Deleting the
`ScopedFrontend` arm from `acting_frontend` left N4 green, because
`ScopedFrontend::enter` also swaps `core.active_frontend` and the
ambient fallback then answers correctly on its own. The arm is
load-bearing in exactly one case — a commit reached from inside an
interactive command, where the origin sits between the override and the
ambient value — and nothing pinned it. N4b is added, driven through
`dispatch_key` because that is the only thing that establishes an
interactive origin, and the mutation now bites it.
Two smaller corrections found the same way:
* `commit_to`'s forged-destination message was unreachable. Typed as
`AnyUserData`, mlua rejected a table during argument conversion, so a
caller got "error converting Lua table to userdata" — true, but naming
neither the rule nor the remedy. The parameter is now `mlua::Value`
and the pointed message fires.
* P1 and P2 also fail on full revert, since `commit_to` does not exist
on the pre-image, so §6.0's "legitimately green on the pre-image" does
not describe them. They stay in the P list because their
discriminating falsifier is the named mutation — a revert-only check
cannot distinguish "validates" from "validates in time" — and each pin
now says so at its own site rather than being silently mislabelled.
Bite results, each run against the whole suite:
scope stops swapping `core.active_frontend` -> N6a, P3 fail; nothing else
preflight moved after the callback -> P1, P2 fail; nothing else
drop the `ScopedFrontend` arm -> N4b fails; nothing else
Docs: COHERENCE §2 grade + step-3 verdict row, §20 Priority 1 and the
arc list; the GPU initial-target framing's Q#GT6 and acceptance 10,
whose directory case this stage deliberately supersedes; handoff §1;
the active-work ledger; framing rev 7.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 11 put the nesting count in the expander, which is optional. A
consumer at a lower priority can CLAIM and stop the chain before the
expander runs, while that fan-out's deferred-expansion subscriber still
runs — so the nested pass went uncounted, looked like the outermost
one, expanded early, and outer pairing resumed with a record the
replace had invalidated. `\alp(` gave `α(` again.
The count now comes from a no-op consumer registered at the minimum
priority, which runs first in every chain invocation that reaches any
consumer at all. Its guarantee is exactly the ordering contract the
chain already rests on, and it degrades safely: the only thing that can
skip it is a claim ahead of it, which skips the expander too, so
nothing is queued in that fan-out either.
The other plausible home does not work and the comment now says why: a
subscriber registered beside `run_deferred` is too late, because the
whole nested fan-out completes inside the OUTER chain's subscriber,
before either of them runs.
Acceptance 45o pins the short-circuit path — a consumer at 25 that
claims when the record is nil, so the nested pass never reaches the
expander. 45n passes against this bug, which is why both exist.
Counting in the expander fails 45o and nothing else.
Framing rev 12 also names the shape rounds 10–12 share: each fix was
correct about the failure it was shown and wrong about the boundary of
the mechanism it leaned on — the chain's copy semantics, then its
re-entrancy, then its short-circuit. A queue that outlives the thing
that filled it has to name that thing, not approximate it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
`buffer.after-edit` fan-outs NEST — the typed-edit contract supports a
consumer calling `pmacs.hook.run`, and typed_edit.lua's header says so
in its second paragraph. A nested run re-enters every subscriber,
including the deferred expansion's, while the OUTER chain is still
walking its consumer list and pairing has not yet seen the terminator.
So a consumer registered at priority 75 — between the expander at 50
and pairing at 100 — that runs one nested fan-out made `\alp(` yield
`α(` again: the nested pass consumed the queued expansion and edited,
and outer pairing then resumed holding a record the replace had
invalidated. That is round 10's failure reached through the chain's
documented re-entrancy seam rather than through claiming, which is why
deferring alone did not close it.
Deferring work past a fan-out means owning WHICH fan-out it belongs to.
The chain's subscriber and this module's each run exactly once per
fan-out, in that order, so counting invocations of the first and
matching them off in the second identifies the nesting level. Only the
outermost pass expands; a nested one leaves the expansion queued. No
new seam in typed_edit.lua, which is merged Stage 4a substrate.
Both halves bite: removing the level check and never counting
invocations each fail the new acceptance 45n.
Also fixes a test comment that still described the span design round 10
discarded — it claimed the expansion replaces the span "INCLUDING the
terminator". The behaviour asserted was right; the explanation was
stale. Framing rev 11.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Three defects, all about what happens AROUND the expansion rather than
about resolving an abbreviation.
A pair character that TERMINATES an abbreviation never reached
auto-pairing: `\alp(` gave `α(`. Q#LN22 already said the terminator is
not claimed and the implementation claimed it whenever an expansion
succeeded. Merely declining is not enough either — the chain hands each
consumer a copy of the record made before any consumer ran, so
expanding inside the chain invalidates the copy pairing is holding and
the closer is silently lost. Verified by mutation rather than assumed:
expand-then-decline reproduces `α(` exactly.
The expansion therefore runs on its OWN `buffer.after-edit` subscriber,
registered after typed_edit.lua's and before lsp.lua's. A claim stops
the chain but not a separate subscriber, which is the point: pairing
claims the terminator it reacts to. The replaced span now covers only
the leader and the typed text, so pairing's closer lands outside it and
survives. One undo restores the same text either way, because the
terminator was always its own insert.
That second subscriber is a new instance of Q#AP7 — lsp.lua flushes
didChange synchronously on the signature-trigger path, and `(` is a
trigger — so acceptance 45m pins it with the sighelp fake server: no
didChange may ever carry the unexpanded text.
The relevance check is now three-part, as pairing's has been since
#110: buffer, window, AND `ed.cursor() == rec.post_cursor`. A redefined
self-insert can insert the completing character and then move the
point, and expanding over a span the user has left teleports them back
into it.
Cursor placement after the replace is context-guarded, as
`repair_cursor` is. A buffer intercept may switch buffers while
`buf:replace` runs; the unguarded `goto_byte` then translated the Lean
buffer's pre-edit point through the Lean buffer's edit and applied it
to whatever was ambient.
Q#LN22, criterion 38's span wording, and the ledger are corrected to
describe the deferred design rather than the one that shipped — the
rationale's source, not only the sites quoting it. Acceptance 45j/45k/
45l/45m added; framing rev 10.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Round 6. Documentation only; no code, no protocol change.
1. **The four-writer table mapped the wrong buffers to `ensure_slot`.**
Verified at the call sites: `ensure_slot` has exactly two callers,
`*compilation*` (`compile.lua:1090`) and `*shell-command*` (`:1125`).
`*search-results*` is an **independent panel** in
`builtin/commands/default.lua` with its own intercept (`:869`),
round-trip mark and writes; `compile.lua` declares its name only to
answer a predicate (`:216`), which is what made it look like a third
slot. Round 5 fixed an undercount and introduced a misattribution in
the same paragraph — the count was right, the mechanism was not.
The table is now keyed by **writer**, not by buffer, so the mapping
cannot silently drift again: four mechanisms, five buffers. It carries
an explicit "do not read `ensure_slot` as covering the search panel"
note, because that is the specific wrong inference.
Corrected identically in `COHERENCE.md` §14 and the framing's
deferred-lane text, which both carried the error.
The scope claim is narrowed with it. "Every generated buffer outside
copy mode" was too wide: `*workers*`, `*help*` and `*buffer-list*` are
generated but do not use this idiom, and the REPL package's intercept
(`packages/repl/init.lua:187`) is an op-filtering editing policy
rather than a read-only panel. The claim is now "every remaining
intercept-protected writer", and the two excluded groups are named so
the next reader does not have to re-derive the boundary.
2. **The recovery floor contradicted itself.** The canonical-base line
said the check accepts `a27f646` or anything newer while the check
below required `74301d1`. The floor genuinely advanced; the prose now
says so outright — a tree at `a27f646` no longer passes — and states
why the floor must move with the base rather than trailing it.
3. **Two anchors survived the integration.** Lean 4 Stage 4a said it was
part of "the `fe8b8ba` anchor above" when the anchor had become
`74301d1`; it now refers to the anchor rather than restating a commit,
which is what let it go stale. And #168's closed entry called its own
`fe8b8ba` figure "the live figure" — it is a reading taken at
`1b6a084`, kept as history, and now says so and points at the
coverage lane as the single authority with an explicit "do not quote
this one forward".
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Rev 5 is approved and the branch is cut, so the ledger's "no branch,
commit, or PR exists yet" line no longer describes reality. Records the
recovery command, notes that PR #177 has merged and therefore unblocks
implementation, and carries the standing obligation that dired Stage 2
re-scouts around commit_to before its branch is cut.
Two doc conflicts, both in favour of `main`, and both are this PR's own
findings arriving from the other side:
- **The dired lane.** #169 did exactly what round 5 finding 5 said it
would: absorbed dired Stage 1 into handoff §1 and removed the ledger
lane per rule 4. This branch carried a placeholder saying #169 owned
that text; the placeholder is dropped and #169's version taken whole.
This is the rule working — one PR, one authority per paragraph.
- **The canonical base.** Both sides edited it. Resolved to `74301d1`,
now naming #169 and #176, keeping `main`'s added guidance that a
recovery threshold must move with the base it declares canonical (a
check that accepts an older commit passes on a tree the file does not
describe). The threshold moved with it.
Consequences of the merge, folded in:
- **The census is re-measured on the merged tree**: 3,176 vs 3,449 —
still **273 dark**, 185 of them in the library. #176's six new tests
are not `crdt`-gated, so both totals moved and the gap did not. The
per-target table is unchanged.
- **The `crdt` Clippy failure is re-measured too, and the previous count
was wrong** — it was read off a different checkout. At `74301d1` it is
seven errors before the build aborts: four in `src/daemon.rs`, three in
`tests/vterm_stage3_acceptance.rs`. Recorded as a **lower bound**,
because Clippy abandons the remaining targets once one fails, and an
older tree showed a further error in
`tests/auto_indent_crdt_acceptance.rs` this run never reached.
- **The PTY-terminate lane (#176) is marked MERGED and retained**, with a
note at its head saying why it survives rule 4: no landed-doc PR owns
moving its facts to the handoff, so removing it now would delete the
record rather than move it. The ledger preamble's stale-on-purpose
paragraph is rewritten around that one lane; the Lean 4 and
GPU-terminal-input headers it used to disclaim no longer exist.
- The flake note's "`src/process.rs` last changed by the Darwin PTY
signal-name fix" is dropped — #176 changed it. The load-bearing half
(#178 did not touch that file at all) is what remains.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Reconciles the handoff and ledger against a main that advanced past
this branch's base: the header, `main` anchor, and canonical-base
description take main's richer versions restamped to 74301d1, main's
new PTY-terminate lane is kept alongside the Lean lane, and main's
Stage 4a/rev-8 lane history is dropped in favour of the Stage 4b lane
that supersedes it — per this ledger's own rule to remove entries when
their PR merges.
Also fixes the coherence census's second count, which still said eight
settings three paragraphs below the nine it now lists.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Documentation only; no code, no protocol change. All five findings
reproduced before fixing.
1. The CRDT-dark census was stale. Re-measured at `fe8b8ba` under CI's
exact flags versus the same flags plus `crdt`: 3,170 vs 3,443 —
**273 dark, 185 in the library**, not the 264/177 #168 measured at
`1b6a084`. The per-target table is regenerated (it gains a
`terminal_copy_mode_acceptance` row, acc16e's, from this very arc),
the rows are stated to sum to the total, and the lane now says the
number moves with every merge and must be re-measured rather than
quoted. #168's figure is kept as a dated historical reading with a
pointer to the live one.
2. The generated-buffer non-adopter inventory was short by half. It is
**four writers, not two**: listview panels (`listview.lua:60-61`),
`*compilation*` **and** `*search-results*` — both through
`compile.lua`'s shared `ensure_slot`, so naming only the first
undercounts a mechanism rather than a buffer — and dired
(`dired.lua:371`). All four pair an erroring intercept with
`bypass_intercept` writes over a still-writable rope, and all four are
emptiable by `M-x buffer.undo`. Corrected in the handoff §4 (as a
table, with each writer's shape), `COHERENCE.md` §14, and the
framing's deferred-lane text. The adoption estimate gains a
consequence: the two `compile.lua` slots append and need a streaming
variant; listview and dired are whole-buffer replaces and are the
cheap half.
3. The ledger's canonical base still named `a27f646` while the same file
recorded #168 and #178. Now `fe8b8ba`, with the recovery check's
accept-or-newer floor moved with it — a stale floor is what lets a
wrong base pass verification.
4. The completed terminal lane is **removed**, not marked complete. Rule
4 of this file's own update protocol says a lane goes when it merges,
and its opening contract says the file records only what has not
landed. Its durable facts moved first: a new arc bullet in the handoff
§1 (the snapshot materializes, so the dispatch-shadow count stays at
six; `prune` reacts to removal rather than causing it; ownership means
the handle table, never found-by-name; profiles are a raw Lua table
and why the escape cache lives on `TerminalSession`; what criterion
17 must assert when it can finally be written; the `cat -v` echo probe
and count-don't-match rule), with the `set_generated_contents`
invariant already in §4. A compact entry remains under "Closed since
the last snapshot". The gate-run flake the lane carried moved to the
CI `crdt`-coverage lane, which owns its discrimination — verbatim,
including its explicit refusal to claim a root cause.
5. The refreshed handoff was internally stale: it anchors on a `main`
that contains #179 and #165 while still calling both "in review".
Both now read MERGED. Dired's durable facts are deliberately **not**
absorbed here — that is open PR #169's job, and writing it from two
PRs would put two authorities on one text — so the dired lane stays,
with a note saying why it survives rule 4 and who removes it.
Also recorded while verifying finding 4's new home: the `crdt` Clippy
failure on `main` is re-verified with exact sites (four in `src/daemon.rs`,
one in `tests/auto_indent_crdt_acceptance.rs`), because any CI job that
compiles the `crdt` targets is red on arrival until they are fixed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Typing `\alpha` in a Lean 4 buffer gives `α`; `\<>` gives `⟨⟩` with the
point between them. The abbreviation table is vendored from
vscode-lean4 and the expander is a typed-edit consumer registered on
the Stage 4a chain at priority 50, ahead of auto-pairing.
The ordering is load-bearing. 64 abbreviation keys contain a character
in the `lean4` pair set, so with pairing first, typing `\[` would
insert `[]` and corrupt the pending key to `\[]` before the second `[`
arrives — `\[[]]` becomes unreachable. The consumer therefore claims
every keystroke that EXTENDS a pending abbreviation, not only one that
completes an expansion; claiming only completions would hand each
intermediate `[` to pairing by a different route.
The vendored table is an ORDERED SEQUENCE, not a map. Upstream breaks
equal-length ties by source declaration order — 101 prefixes depend on
it, and `\f` resolves through `f<` rather than `f>` — which a
`pairs`-iterated Lua table cannot express. `scripts/regen-lean-abbrev`
takes a vscode-lean4 commit, emits the file with its provenance header,
and aborts on a duplicate key, invalid UTF-8, or a round-trip mismatch.
Undo is cross-peer-degraded on CRDT frontends and that is accepted and
named, not papered over (Q#LN21): `\alpha` arrives as six source-peer
optimistic inserts while the expansion is one daemon-peer replace.
`set_round_trip_input` would fix it and also makes `dispatch_idle`
report false, so RET would stop inserting a newline.
Round 9 corrects three approved acceptance criteria that the real table
contradicts, found by simulating the state machine over all 1,855
entries and re-reading upstream at the pinned commit rather than
re-reading the prose. `\to` is not eager — `top`, `to0` and `toa`
extend it. `\zzzz` expands to `ζzzz ` because `ze`, `zeta` and
`zsqrtd` exist; only `$ % , ; @ W` open no key at all. And `\alpha`'s
undo does not restore `\alpha ` because `alpha` IS eager, so the
terminator is a separate edit. Criteria 38, 41 and 42 now state both
paths, and the false halves are asserted too: they read as correct
until the table is consulted.
Three implementation traps worth the record. The generator's own
round-trip check was broken twice and failed closed both times:
`str.splitlines()` splits on U+2028, which 53 symbols contain, and
escaping through `chr(byte)` produced a latin-1-shaped string that the
UTF-8 write re-encoded. The first check compared in-memory strings and
agreed with itself; it now stages the file, re-reads the bytes from
disk, and renames into place only on a match. And the expansion SHRINKS
the buffer, so the point must be placed explicitly — pairing's
no-cursor-motion rule holds only for an insert AT the cursor, and
without this every self-insert after the first expansion is silently
rejected and the editor looks dead.
25 acceptance tests plus one `--lib` test for the optimistic CRDT
producer (45f), which is where the gate list's `--features crdt` run
reaches it; a crdt-gated integration test would be dark in CI and in
the gates both. Fifteen mutations bite, each failing its target. Three
of these tests were vacuous when first written and biting is what
found them: the abandonment test asserted text a surviving record
would also produce, the re-arm test used an example that never reaches
the re-arm branch, and both switch tests ran through
`find_or_open`'s fresh-load path rather than `buffer.after-switch`.
No protocol change (Q#LN14). Also reconciles the handoff and ledger
for Stage 4a (#179) and adds `lean.abbrev` to COHERENCE.md's
config-registry adoption census, now nine settings.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Re-integrated after #178 (terminal copy mode) landed. One conflict, in
COHERENCE.md's journey table: row 7 keeps this branch's text (dired #165
is merged, so "PR #165" is wrong), row 8 takes main's, which adds copy
mode and the missing close/kill command to the terminal step.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
Documentation only; no code, no protocol change.
Handoff §1 anchors on `main` @ `fe8b8ba` and leads with terminal copy
mode (#178) and its landed-doc pair (#168). The active-work terminal lane
flips to BOTH STAGES MERGED, and the #166 lane records #168 landing with
what it measured: 264 tests dark workspace-wide for want of `crdt` in CI,
and the vterm audit's honest count of acceptances that drive a real
daemon (2, not 3).
The substantive addition is a new §4 substrate invariant for
`Buffer::set_generated_contents`, because it is now the one authorized
write for every generated buffer and three of its properties are
non-obvious enough that four review rounds were spent finding them:
- an intercept is not read-only — `Buffer::undo` reaches the rope through
`ensure_writable` without consulting the intercept chain, and rebinding
the undo chords does not help because `M-x buffer.undo` needs no
keymap;
- a bare `set_read_only` would be worse than nothing, since it also
refuses the owner's refresh — the pairing is the primitive, which is
why no Lua `set_read_only` exists;
- a rope write is only half of an edit: the returned `Edit` must be
fanned out, or a displaying window paints the new rope with stale line
offsets and replica mirrors never import the write.
Also recorded: history clearing must clear whichever history the buffer
has (the v0.1 stacks are bypassed in CRDT mode), that `*compilation*` and
listview have NOT adopted the primitive and remain emptiable by
`M-x buffer.undo`, and that this does not replace `set_round_trip_input`
— the two guards cover different copies, and a daemon refusal arrives
after the frontend has already painted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Re-integrated after #168 landed the ledger refresh. Five conflicts, none
resolved by taking a side wholesale:
- Both head-of-main anchors take main's a27f646 wording (written by
#168); the ledger keeps this branch's caveat about lanes naming an
older base.
- The dired lane section is pruned, which is this PR's purpose, but main
had meanwhile pruned the GPU terminal input lane as landed — so the
union drops both stale lanes rather than resurrecting either.
- "Closed since the last snapshot" keeps BOTH new entries: dired Stage 1
#165 from this branch and GPU terminal input #166 from main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
Same one-line ledger conflict as the previous integration, now against
the refreshed main (#168): keep this lane's PTY terminate section, take
main's newer Lean 4 lane heading.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
Levi Neuwirth