Commit Graph

398 Commits

Author SHA1 Message Date
Levi Neuwirth d98d0b3994 docs(framing): generated-buffer immutability, revision 4
Answers review round 3 on 8e032d7 -- three P1, two P2. All five confirmed
against the tree; none re-litigated. Withdraws three of revision 3's own
decisions.

Why revision 3's exactness argument did not extend to CRDT: it proved that
`revision` bumps between the undo push and the on_edit broadcast, which
makes the predicate exact for the v0.1 stack -- and then treated that as a
proof about cleanup in general, when CRDT mutation happens upstream of
`revision` entirely (apply_to_crdt_then_normalize_bytes runs before the
rope edit). The argument was sound about the mechanism it examined and
silent about the one it did not, and stating it as a proof is what stopped
it being checked against the second.

P1-1, the cleanup predicate. Wrong in three directions, not two. Section
3.4 is rewritten around an explicit five-variant GeneratedOutcome reported
by the apply. Direction A is fixed by restating the invariant as a property
of the buffer -- a generated-locked buffer carries no history -- so NoOp
clears; that phrasing needs no reference to `revision` and is therefore
mode-independent, which is the actual repair. Direction B gets a Diverged
variant that clears nothing and surfaces, because clearing would destroy
the last local record of the pre-edit rope; the divergence itself is
pre-existing, reaches apply_edit today, and is deferred as its own lane
rather than pretended to be fixed here. Third direction, found while fixing
the other two and not in the review: the unconditional relock locked a
fresh buffer that was never successfully written -- a mid-codepoint
generated insert on a writable *scratch* returned Err and left it
read-only. Rejected now restores the entry lock state.

P1-2, vacuous criteria 15-16. Confirmed, and the contradiction was internal
-- section 3.4 argued pre-validation makes an invalid range cost nothing,
then the criteria used an invalid range to test post-apply cleanup, in
adjacent sections. Both rewritten around a valid write that fails at the
on_edit broadcast, staged with a Rust-side FailingView (view::View is pub,
attach_view is pub). Criterion 16 splits, because section 3.4 now answers
relock-on-failure and no-lock-on-refusal differently. New 16b and 16c cover
the two P1-1 directions; 16c carries an explicit caveat that its staging
recipe is not verified here, with a four-variant fallback rather than a
criterion that passes by never reaching its path. Rule adopted: every
criterion names the exit it drives the implementation to, and that exit
must be inside the mechanism under test.

P1-3, provenance. generated_lock withdrawn. The defect is not the rule's
details but that a derived fact must be maintained by every mutation of
what it derives from, and set_read_only is pub with callers this document
does not control. Replaced by identity_protected -- a property of what the
buffer is, set once by TerminalSession::open, never written by
set_read_only. The lift/upgrade/restore cycle at
terminal_copy_mode_acceptance.rs:578-584 is transparent to it, so Q#GB12
and Stage 2 criterion 4 need no change, which is the test that the rule is
right. Section 10 now names `--test terminal_copy_mode_acceptance --features
crdt` as its own gate step: acc16e is cfg-gated, so a default-feature run
never compiles it.

P2-4, the registration dependency. Confirmed: revision 3 replaced an
existing guarded optional dependency with an unguarded call, and the
configuration the guard defends is reachable -- LuaHost is pub and nine
test files already build one. Q#GB18 becomes symmetric guarded optionality:
each module answers for its own buffers and consults the other through the
guard shape already in the tree. That also removes the teardown obligation
revision 3's registry introduced. New criterion 21 pins the minimal
harness.

P2-5, the fold criterion. Confirmed. Split into 13a [main] for the
behaviour change and 13b [mutation] for the status string, whose pre-image
cannot be main because on main the call succeeds and sets no status.

Sweep D, rules spanning v0.1/CRDT or fresh-lock/existing-lock: 13 examined,
3 broken (the two the review named plus the relock one), 1 that looked at
risk and verified clean -- undo_crdt_mode does return NothingToUndo
(src/buffer.rs:1374-1376), so Stage 2 criterion 4's assertion is correct in
both modes.

Sweep E, every criterion added in revisions 3 and 4 audited for whether the
state it asserts is reachable by the operation it performs: 19 audited, 3
defects, all fixed here. Also records that S2-17 is the one criterion for
which the pre-validation exit IS the mechanism under test, so it stays as
written.

All counts re-measured at 7586905 with the command output pasted into the
revision-4 block; all unchanged.

Status stays PROPOSED. No runtime code, no protocol change.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
2026-07-28 21:01:31 -04:00
Levi Neuwirth 8e032d75d8 docs(framing): generated-buffer immutability, revision 3
Answers review round 2 on #188 @ 516bd35 -- three P1, two P2 -- integrated
to main @ 7586905 (#189, COHERENCE.md only; clean merge).

P1-1, the route cannot write to a locked buffer. Confirmed, and the
review's first repair option cannot work: reordering begin_edit's two
checks leaves ensure_writable running one line later, so a locked buffer
is still refused and only the reported error changes. Any admitting path
must not reach ensure_writable at all. Q#GB3 is reversed -- generated
writes get their own run_buffer_edit arm and never touch begin_edit -- and
new section 3.4 specifies the transaction: one &mut Buffer method, eight
named exits with the post-state of each, relock and editing_in_progress
clear unconditional, bounds pre-validated so an invalid range costs no
history, and history cleared iff the revision advanced (exact, because
revision bumps after the undo push and before the on_edit broadcast).
Proved along the way that no Lua runs inside a generated write:
LuaInterceptView implements only intercept_edit and inherits View::on_edit's
no-op default, so the only re-entrancy direction that needs a gate is
outward.

P1-2, disambiguation. New section 2.10 is the census: 19 units across 14
grep lines, five classes, arithmetic shown, each classified by reading its
enclosing function. Two sites break; between them six downstream consumers,
not three. The fourth listview consumer is listview.open's own
never-capture-a-panel guard, which fails inverted and silently -- it
captures the panel as its own q target, the exact loop its comment says it
prevents. compile's slots table is NOT affected (keyed by a module
constant, slot_for_buffer is id-based). New Q#GB18 routes both by owned
BufferId, and notes listview registers no on_removed so its new list must
compact on scan like dired's live_handles.

P1-3, unlock_generated. Withdrawn as written; both halves of the finding
hold. Sweep C found the mirror-image hole the review did not: the SHIPPED
set_generated_contents lifts a lock it did not install, so it can already
overwrite a live terminal identity buffer. Provenance (new Q#GB15,
generated_lock beside read_only) therefore earns its cost in both
directions rather than existing to make the unlock safe. Q#GB7 moves to
Stage 2, its claim narrows from "brick escape" to "the closure of the
capability { generated = true } adds", and the asymmetry with the standing
no-Lua-set_read_only policy is addressed directly: a provenance-bounded
unlock adds no reachable state that { generated = true } did not.

P2-4, criterion 6. Confirmed, and the framing cited the wrong precedent:
terminal_copy_mode_acceptance has zero dispatch_idle_for references. The
model is dired_acceptance.rs:969. dispatch_idle_for has six ways to return
false and the review named one, so the criterion now carries three halves
-- document-window premise, the gate, and acc16's positive control, which
rules out the other five clauses in one assertion.

P2-5, the path-backed refusal. Now exercised on all four surfaces with
guard misplacement as the explicit bite.

Sweep C (obligation 3) also found that read_only is one boolean serving
three policies: the generated lock, terminal identity, and -- as a reader
-- fold.rs:313's "is this a document buffer" test, pinned by
folding_acceptance.rs:570. Locking five families silently disables
pmacs.fold.fold on all five, which contradicts Q#GB3's own stated rationale
for preserving the unfold seam. New Q#GB16 names it and recommends
accepting it with a criterion rather than accepting it silently.

Two further corrections the review did not name. COHERENCE.md section 14's
listview list was corrected by #189 while revision 2 was open, so section
1.5 goes from owed to landed -- a merged correction is removed, not
restated. And *help* has two independent writers, src/help.rs:354 (Rust,
apply_edit, mark_clean) and default.lua:1239 (Lua, no mark_clean), each
with its own find-by-name and its own copy of the name constant, so the
inventory's headline is five mechanisms, not four.

Section 2.9's is_modified sweep is corrected a second time: seven
production consumers, two load-bearing. Revision 1 said two, revision 2
said four. The conclusion is unchanged but was reached twice from an
incomplete count.

New section 9b records the cross-lane boundaries verbatim and confirms
Q#DR25 against #171 revision 7 at fd7ae37. Revisions 1 and 2 never
mentioned Q#DR25 at all despite owning it; revision 3 claims it, and
carries #171's trap that dired_acceptance.rs:969's read-only status
assertion passes both before and after adoption.

Twelve acceptance criteria added or rewritten, each stating what it asserts
about content produced and the mutation that falsifies it. Stage 2 gains
criteria for the transaction's error paths specifically -- a leaked
editing_in_progress asserted through the NEXT edit, not the failing one,
because the failing call reports the same error either way.

Why revision 2 shipped these: it audited criteria against pre-images
(sweep A) and capabilities against who may use them (sweep B), but never
read the guards its own mechanisms had to pass through. begin_edit,
document_bytes and terminal/session.rs:305 were all cited elsewhere in the
tree and none was opened. The process fact for revision 4: for every seam
the design routes through, read the callee, not the caller's description of
it.

Status stays PROPOSED. No runtime code, no protocol change.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
2026-07-28 20:26:18 -04:00
Levi Neuwirth 516bd3579a docs(framing): generated-buffer immutability, revision 2
PROPOSED. Framing only; still no runtime code.

Answers five review findings on PR #188 at 9101bf5 (three P1, two P2),
plus the two sweeps the review asked for by class.

P1-1: Stage 2 criteria 3, 4 and 5 all passed on the pre-image. Ordinary
edits are already refused by the existing intercept, and Buffer::undo
checks read_only before it inspects history, so "undo returns false"
passes against an implementation that locks and never clears. Rewritten
to use a bypass write or Rust-side is_read_only for the lock, and to lift
the lock inside a Rust test before asserting NothingToUndo.

P1-2: ownership by handle is now a prerequisite of the stage that locks
each writer. Measured: a foreign *references* is clobbered and left
permanently un-editable, a pmacs.compile.run that raises on validation
still leaves a foreign *compilation* un-editable, and M-x buffer.undo is
currently the only recovery -- which this arc removes.

P1-3: revision 1 was wrong that is_modified drives only the mode line.
autosave.rs:363 and desktop.rs:302 read it. The rule chosen: a generated
write refuses a buffer that has a file_path.

P2-4: view_top is a line index, cursor is a byte position. The clamp is
now per-coordinate and ungated.

P2-5: re-measured at ad41cf1, 276 dark, with the command shown.

Sweep A found Stage 1 criterion 7's stated bite was wrong, and that eight
criteria pass on main by design without saying so; every criterion now
carries a pre-image class. Sweep B found the two halves of the protection
are asymmetric -- the intercept is removable, the rope lock is not --
which falsifies revision 1's reason for deferring the unlock, so Q#GB7 is
upgraded to Stage 1 work.

Adds the PR #188 lane to docs/active-work.md, which the ledger now
requires for every open PR.
2026-07-28 18:32:05 -04:00
Levi Neuwirth 9101bf5b78 docs(framing): generated-buffer immutability, revision 1
PROPOSED. Framing only; no runtime code.

Buffer::undo gates on ensure_writable() and never consults the intercept
chain, so the add_intercept "read-only" idiom leaves the rope writable
and the owner's own bypass_intercept paint on the undo stack. Four writer
mechanisms across five buffer families are affected; every one was
reproduced by execution at ad41cf1, not inferred.

The document carries the measured reproductions, the full classified
census with its arithmetic shown, the primitive decision with numbered
alternatives, per-criterion bite obligations, and the staging proposal.

Recommended primitive: Buffer::apply_generated_edit(op), exposed as a
{ generated = true } option on the existing Lua mutators, with
set_generated_contents reimplemented as its whole-buffer wrapper. It is
the only candidate in which the buffer is never observably unlocked.
2026-07-28 17:57:57 -04:00
Levi Neuwirth 6fc7fee044 docs: absorb #174 and advance the anchors to 0442d78
#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.
2026-07-28 17:04:17 -04:00
Levi Neuwirth a159200756 docs(active-work): give the two open PRs the lanes they never had
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.
2026-07-28 16:42:00 -04:00
Levi Neuwirth e05ac819b5 docs: sync the durable records to landed main @ 6bee09d
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.
2026-07-28 16:28:21 -04:00
Levi Neuwirth 5539b6e8c6 Record the fixture-specific PR 184 probe fix
Capture the follow-up review finding, the evidence-driven completion
contract, the exact corrected CAT duration, and the proportional green
gate matrix at 9c79ce1.
2026-07-28 15:29:55 -04:00
Levi Neuwirth 80b761bb03 Record the regated PR 184 review head
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.
2026-07-28 14:29:04 -04:00
Levi Neuwirth ab7c207904 Keep the v21 panel wire dark for v20 clients
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.
2026-07-28 14:08:17 -04:00
Levi Neuwirth f82d91ed3a docs(active-work): record bottom-panel 2B-1 PR
Record PR #184 as open for review and keep the explicit no-merge hold in
the portable lane state.
2026-07-28 12:51:42 -04:00
Levi Neuwirth 17867ace0e docs(active-work): record integrated 2B-1 gates
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.
2026-07-28 12:44:27 -04:00
Levi Neuwirth c8895a85d3 Merge canonical main into bottom-panel Stage 2B-1
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.
2026-07-28 11:38:19 -04:00
Levi Neuwirth 22c1b14b18 docs(active-work): record review-round cleanup gates
Record the second-pass daemon-cleanup finding, its correction, and the
green verification matrix on the updated PR branch.
2026-07-28 11:03:36 -04:00
Levi Neuwirth 22dc46c184 docs(active-work): record public-path gates
Record the green full matrix for the public pmacs --gpu directory
acceptance revision at 34b8f28.
2026-07-28 10:33:26 -04:00
Levi Neuwirth 34b8f28cf2 test(journey): ratchet the public GPU directory path
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.
2026-07-28 10:27:22 -04:00
Levi Neuwirth 3be4285f7c docs(active-work): record review-round gates
Close PR 183 review round 1 in the volatile ledger and record the
post-correction full gate matrix at ec4191f.
2026-07-28 10:01:18 -04:00
Levi Neuwirth ec4191fd8e test(journey): pin post-quiescence GPU dired surface
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.
2026-07-28 09:48:48 -04:00
Levi Neuwirth c2b855e252 docs(active-work): record directory ratchet PR
Attach the gated Journey/GPU side-quest lane to PR #183 and make its
intentional open, unmerged review state explicit.
2026-07-27 23:19:05 -04:00
Levi Neuwirth a5107ca32d docs(active-work): record directory ratchet gates
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.
2026-07-27 23:15:10 -04:00
Levi Neuwirth 486ce16748 test(journey): ratchet directory GPU bootstrap success
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.
2026-07-27 22:53:36 -04:00
Levi Neuwirth b9123c2f6d test(protocol): advance touched-suite ratchets to v21
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.
2026-07-27 22:39:15 -04:00
Levi Neuwirth d88d60eba6 Merge canonical main into bottom-panel Stage 2B-1
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.
2026-07-27 22:16:11 -04:00
Levi Neuwirth 7a3a55de40 docs(active-work): remove the landed Lean 4 lane
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.
2026-07-27 21:47:01 -04:00
Levi Neuwirth 56301eda02 docs(panel): Stage 2 framing rev 5 — the three-way slice of 2B
Rev 4 §9 scoped Stage 2B as a single PR: v21 protocol, daemon panel
projection, GPU band, and the negotiated `panel_capable` flip.
Implementation showed that to be roughly four thousand lines across
three crates with three different failure modes. Rev 5 splits it into
2B-1 (the wire layer), 2B-2 (the daemon projection and epoch machine),
and 2B-3 (the GPU band and the flip), on the rule that a slice ends
where the next thing to build has a different authority.

No decision changes. What changes is the allocation:

- §7.2 becomes three subsections, and criteria that span a boundary are
  named in every slice they touch with their half stated, rather than
  assigned wholesale to one. Parent 39 is the clearest case: its
  shared-validation and transport-budget halves are wire properties
  provable in 2B-1, while "the previous valid frame is retained" and "a
  duplicate does no work" need the epoch machine and are 2B-2. A2B-1
  splits the same way — grid exhaustion in 2B-2, the frontend latch in
  2B-3.
- §9 lists four serial PRs instead of two, each cut from `main`, and
  states that every slice runs the full gate set rather than the subset
  its own crate suggests.
- §6 records which slice pays the coherence debt. The journey claim
  belongs to 2B-3 alone: with `panel_capable = false`, a GPU user still
  gets the Stage 1 non-side fallback after 2A, 2B-1 and 2B-2 have all
  landed. Three quarters of this stage is preparation.

Two things recorded because they are easy to inherit silently:

- This revision is retroactive for slice 1. `bottom-panel-stage2b`
  already carried the v21 protocol layer, written before the revision
  existed, which inverts framing -> approval -> branch -> implement. The
  slicing was sound; taking it in code rather than in the document is
  how a stage's scope drifts without anyone deciding that it should.
- 2B-1 and 2B-2 ship dark. The bump advertises a capability whose only
  distinguishing feature is unreachable until 2B-3, so the arc must not
  stall between them. Safe for compatibility — appended variants,
  extended ladder, a v20 peer still negotiates 20 — but a stall should
  be visible as a decision, not inherited as a default.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 20:02:19 -04:00
Levi Neuwirth d0817314f9 merge: fold the terminal landed-docs PR (#180) into this branch
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>
2026-07-26 18:36:55 -04:00
Levi Neuwirth 8e31ca4646 Merge remote-tracking branch 'githubsucks/main' into journey-stage1a-directory-open 2026-07-26 18:33:44 -04:00
Levi Neuwirth 4cf1b63198 docs(active-work): the journey suite is 24 pins, not 23
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>
2026-07-26 18:33:26 -04:00
Levi Neuwirth 7741cf806a fix(journey): honor the captured window, not the selected one
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>
2026-07-26 18:20:02 -04:00
Levi Neuwirth d9d1c0b423 test(journey): pin the destination commit, and land the doc updates
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>
2026-07-26 17:25:22 -04:00
Levi Neuwirth d1bff6ac30 fix(lean4): count fan-outs where a claim cannot skip the count
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
2026-07-26 17:15:24 -04:00
Levi Neuwirth 0d7ec7e3a6 fix(lean4): tie the deferred expansion to the fan-out that queued it
`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
2026-07-26 17:00:58 -04:00
Levi Neuwirth f3103a6953 fix(lean4): defer the expansion past the chain, and guard its point
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
2026-07-26 16:47:54 -04:00
Levi Neuwirth d2ab3761c7 docs: correct the non-adopter attribution and two stale anchors
Round 6. Documentation only; no code, no protocol change.

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

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

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

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

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

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

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-26 16:45:12 -04:00
Levi Neuwirth 25b07be97b fix(journey): correct Q#JR3, report the post-dispatch buffer, unvacuate two pins
Four review findings, all confirmed against the tree.

Q#JR3 was false. `replace_active_buffer` does not drop the startup
scratch buffer -- its body is one `switch_active_buffer` call, which
reassigns the window's buffer_id and removes nothing. The claim came
from that function's own doc comment, wrong for as long as it has
existed, and rev 5 propagated it into the framing and into new
documentation this branch added. Both comments are corrected here,
because this PR was adding further false references to a claim P4
depends on. Actually removing the stale scratch is buffer-lifetime work
and stays out.

The daemon bootstrap could report the wrong buffer. The directory arm
captured the destination id, ran the resolver chain synchronously, then
returned the captured id -- so a handler that opened something
synchronously through commit_to had already replaced the window's
buffer, and the reply paired one buffer's snapshot with another's
identity. It also returned early, skipping the post-hook revalidation
the framing said stayed active. The arm now re-reads the destination
after dispatch and rehomes through `non_side_target` as the file arm
does. Pinned by a test whose handler claims synchronously.

N11 tested neither RET nor self-insert: it called display_file and
buf:insert directly, so it stayed green with dired's RET binding, its
entry dispatch, and the editor's self-insert path all broken. Both
gestures now go through dispatch_key.

P7 is removed rather than weakened. Q#JR12 has nothing to pin --
`had_file = file.is_some()` and a directory is Some like any other, so
no directory-specific branch exists to break. The old test never armed
restore and hard-coded had_file, so it could not fail against any
implementation.

Also adds the daemon bootstrap pins (N2, N5) and fixes an insertion that
had orphaned a `#[cfg(feature = "crdt")]` from the test it guarded --
which would have made one new test dark and one existing test escape its
gate.

Framing: docs/journey-stage1a-framing.md rev 6.
2026-07-26 16:39:59 -04:00
Levi Neuwirth dd9f380533 docs(active-work): record Journey Stage 1a branch and ordering
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.
2026-07-26 16:39:59 -04:00
Levi Neuwirth 600b3d0c7d docs: framing for Journey Stage 1a (directory open on one path)
Serves COHERENCE.md §2 (the golden product journey), §19 (coherence
acceptance tests), and §20 Priority 1, which grades the journey broken
at step 3 because `pmacs .` exits 1.

Stage 1a ships four things: the directory argument routed into dired's
buffer on both the local and daemon/GPU startup paths; EditorState::open
adopting resolve_target_buffer so the two path-open implementations
become one; a scoped-destination commit primitive so an async open lands
where it was requested or nowhere; and the first cross-subsystem journey
acceptance suite.

Framing only -- no implementation. Rev 5 after four review rounds.
2026-07-26 16:39:27 -04:00
Levi Neuwirth d14fe4c4b9 Merge githubsucks/main (#169, #176) into docs-terminal-copy-mode-landed
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
2026-07-26 16:37:41 -04:00
Levi Neuwirth f8ca722d66 merge: integrate main (74301d1) into Stage 4b
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
2026-07-26 16:37:19 -04:00
Levi Neuwirth e4c9d65231 docs: fix five review-round-5 findings in the landed-doc refresh
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
2026-07-26 16:28:04 -04:00
Levi Neuwirth a53965474d feat(lean4): the Unicode input method (Arc 8 Stage 4b)
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
2026-07-26 16:24:06 -04:00
Levi Neuwirth 74301d1670
Merge pull request #169 from levineuwirth/docs-dired-stage1-landed
docs: record dired Stage 1 (#165) as landed
2026-07-26 20:23:39 +00:00
Levi Neuwirth c5c9f3f13a Merge branch 'main' into pty-terminate-eperm
Clean integration of #178 (terminal copy mode); no conflicts.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
2026-07-26 16:09:48 -04:00
Levi Neuwirth 4182270fd3 Merge branch 'main' into docs-dired-stage1-landed
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
2026-07-26 15:57:13 -04:00
Levi Neuwirth 44f5e44b9f docs: record #168 and #178 as landed, and the generated-buffer invariant
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
2026-07-26 15:48:03 -04:00
Levi Neuwirth f3e0b98ced Merge branch 'main' into docs-dired-stage1-landed
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
2026-07-26 15:41:58 -04:00
Levi Neuwirth 8943b4c277 Merge branch 'main' into pty-terminate-eperm
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
2026-07-26 15:00:49 -04:00
Levi Neuwirth 1b44c69a53 Merge remote-tracking branch 'githubsucks/main' into terminal-copy-mode
# Conflicts:
#	docs/active-work.md
2026-07-26 14:59:09 -04:00
Levi Neuwirth a58bb110bc docs(terminal): qualify process flake attribution
Separate the observed suite behavior from the suspected drain_until
mechanism, and leave round-2 failures unattributed without test names.
2026-07-26 14:54:37 -04:00
Levi Neuwirth 42f601a7ec Merge branch 'main' into gpu-terminal-input-docs, and refresh the ledger
The handoff's "last updated" paragraph conflicted; resolved by writing
the current statement rather than taking either side, and the same pass
clears the staleness the ledger had accumulated while five PRs contended
for it:

- Both head-of-main anchors (handoff §1 and the ledger's canonical base)
  now name a27f646, and list terminal config #173, the bottom-panel
  Stage 2 framing #175, Stage 2A #177 and Lean 4 Stage 4a #179 — plus
  the CRDT undo repro #157 and the inline-math landed-doc refresh #172,
  which are merged but had dropped out of both lists.
- The bottom-panel lane records Stage 2A as MERGED (#177 @ 0a3fcd1)
  instead of IN REVIEW, and states what 2B is: approved, unstarted,
  branching from main rather than stacking, with §7.2's criteria and
  §5.3's three-boundary trap named.
- The Lean 4 lane records Stage 4a as MERGED (#179 @ a27f646); its
  "framing-only, no code, awaiting approval" bullet was false.

The dired lane is left alone deliberately: #169 is the PR that records
dired Stage 1 as landed, and owns that heading.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
2026-07-26 14:43:43 -04:00