Commit Graph

777 Commits

Author SHA1 Message Date
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 1b6a0844ae
Merge pull request #168 from levineuwirth/gpu-terminal-input-docs
docs: record #166 as landed, measure the CI coverage gap, audit vterm as framed
2026-07-26 18:58:30 +00: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
Levi Neuwirth 9e6c166c57 Merge branch 'main' into pty-terminate-eperm
Resolves the ledger conflict: keep this lane's PTY terminate section and
take main's newer Lean 4 lane heading verbatim. No content of either
lane is rewritten here.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
2026-07-26 14:32:15 -04:00
Levi Neuwirth a27f6467ea
Merge pull request #179 from levineuwirth/lean4-stage4a-typed-edit-chain
Lean 4 Stage 4a: the typed-edit consumer chain
2026-07-26 18:00:48 +00:00
Levi Neuwirth ea9b8c379e docs(lean4): correct Q#LN10's throw-containment rationale
Q#LN10 still said a throwing consumer "fails the fan-out for everyone."
It does not: `run_all_must_succeed` (src/hook.rs:332) collects the error
and continues to the hook's remaining subscribers, so `lsp.lua` still
flushes didChange. The throw stops every LATER consumer in the chain,
which is a narrower consequence and still worth containing — the
failure is silent exactly where the abandoned consumers registered.

The module comment, criterion 46d, the test, and the ledger were all
corrected in the previous commit; Q#LN10 is the decision they descend
from, so leaving it stale would have made the disproven claim the
authoritative one. Also records the protected-rendering rule there.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 13:43:30 -04:00
Levi Neuwirth aef4e98c26 fix(typed-edit): close round-8 review on the consumer chain
Five defects in the chain itself, plus the stale handoff state.

Each consumer now gets its own shallow copy of the typed-edit record.
Handing everyone the same table let a DECLINING consumer rewrite
provenance for the ones behind it, and pairing decides what to close
from `rec.char` — so a forged `char` turned a typed `x` into `x)`.
Every field is a scalar or an opaque id, so a shallow copy is complete.

The fan-out iterates a snapshot of the consumer list. It was iterating
the same array `add_consumer` mutates: a consumer that registered a
lower-priority one shifted itself forward under `ipairs` and ran twice,
and re-registering made that unbounded. Registrations and removals made
during a fan-out now take effect on the next one, stated as a contract
and pinned in both directions.

`tostring` on the caught error moved inside the containment. A Lua
error may be any value, including a table whose `__tostring` throws —
rendering it outside the `pcall` reintroduced exactly the escape the
containment exists to prevent.

Priorities are validated as finite integers in i32 range, matching
`pmacs.completion.register`. NaN is a number and every ordered
comparison with it is false, so a NaN consumer landed wherever the
insertion scan gave up and silently voided the lowest-first ordering
that Q#LN22 depends on.

`add_consumer` returns a handle and `remove_consumer` unregisters it,
reporting whether it was live. Without teardown the chain inherited the
`pmacs.hook.add` callback leak COHERENCE.md §13 already records, and
spread it to every consumer.

Also corrects the rationale the containment was documented with, in the
module, the test, and the framing: an uncontained throw does NOT take
the fan-out's other subscribers down. `run_all_must_succeed`
(src/hook.rs:332) collects errors and continues, so lsp.lua still
flushes didChange. The containment is still required — the throw skips
every later consumer in the chain — but the reason is narrower than
rev 7 claimed.

Criteria 46f (record isolation), 46g (snapshot iteration), and 46h
(lifecycle and priority validation) added; 46d's rationale corrected.
Four new tests, all bite-verified by mutation, each failing only its
target: shared record table (1), live-array iteration (1), unprotected
tostring (1), bare number check (1), no-op removal (2). The suite also
runs green under `--features lua54`.

docs/agent-handoff.md said Stage 4a was awaiting approval while this
branch had it implemented and in review.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 13:39:33 -04:00
Levi Neuwirth 0a3fcd1942
Merge pull request #177 from levineuwirth/bottom-panel-stage2a
feat(panel): bottom-panel Stage 2A — classified census routing + painter extraction
2026-07-26 17:28:49 +00:00
Levi Neuwirth 842417200a fix(panel): close Stage 2A review round 3 (2 P1)
**P1-1 — layout invalidation could suppress the authoritative clear.**
Real bug. Both render paths resolved the document identity AFTER the
evaluator ran callbacks, but BOTH outcome arms carry PHASE-1 contexts.
A provider that closes the primary document split changes
`primary_document_window` mid-evaluation, so the filter compared
phase-1 contexts against a replacement identity, matched nothing, and
emitted no clear — leaving stale statusline text on the wire forever.

The identity is now captured BEFORE `evaluate_statusline` runs and
threaded through both paths (the terminal path via `terminal_chrome`).

Pinning it took three attempts, and the two failures are the useful
part:

- `pmacs.window.close()` takes no argument — it closes the ACTIVE
  window. The first version passed a window id that was silently
  ignored, so it closed the panel instead of the document.
- The Lua window API acts on the ACTIVE FRONTEND, so driving it against
  a synthetic semantic view changed nothing at all.
- Closing the only document window is structurally REFUSED (Q#BP6
  forbids a lone side window as a resting state), so the fixture needs
  TWO document windows for the close to be legal.

The test now asserts its own precondition — that the callback really
changed the identity — before asserting the clear, and reproduces the
reported symptom (no `StatuslineSegments` at all) when the fix is
reverted.

**P1-2 — #21 was pinned at the helper, not the producer.** Confirmed:
reverting only the call site inside
`publish_buffer_snapshot_to_replicas` left both the helper test and the
existing socket-pair test green. The helper assertions are removed (with
a note saying why) and replaced by
`snapshot_publication_follows_the_document_under_a_focused_panel`, which
drives the real producer over socket pairs and asserts BOTH directions:
the document buffer's snapshot is delivered while a panel holds focus,
and a panel-only buffer's is not.

Biting that test exposed a defect in the test itself: the delivery read
had no timeout, so a regression made it HANG rather than fail. A hanging
test is strictly worse than a red one — every read now has a timeout.

Gates: fmt clean; workspace clippy clean; 1,832 default + 2,015 CRDT
library; Stage 2A 17; Stage 1 46; statusline 8; m11_5 2; GPU initial
target 14; terminal config 12; folding Stage 2 48; vterm 1/2 10 / 6;
M4 121; required GPU 202; `git diff --check` clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-26 13:18:05 -04:00
Levi Neuwirth c7072b49e9 docs: record the Stage 4a lane and its bite table
Verification describes the pushed tree, per the standing rule. Includes
the bite that was worthless as first written: moving only typed_edit.lua
past lsp.lua broke the runtime load instead of testing flush ordering.
A bite that kills everything has not isolated anything.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 13:05:41 -04:00
Levi Neuwirth 24ca906294 feat(typed-edit): the typed-edit consumer chain (Arc 8 Stage 4a)
`pmacs.editor.take_typed_edit()` is one-shot and per-frontend (Q#AP9):
the first `buffer.after-edit` callback to call it clears the slot, and
every later callback in the same fan-out sees nil. That was survivable
only because auto-pairing was the sole consumer — never a property
anyone chose. A second independent caller would get nil or steal the
record from pairing depending on hook registration order, and
registration order is not a contract.

This makes it one. `builtin/runtime/typed_edit.lua` owns the single
after-edit subscriber that reads the record, and offers that one read to
consumers registered through `pmacs.typed_edit.add_consumer{ name,
priority, fn }`: lowest priority first, ties by registration order, and
the first consumer to return truthy claims the edit and stops the chain.
`pair.lua` becomes that chain's only consumer, at priority 100.

No Lean content. Stage 4b's abbreviation expander is what needs the
ordering guarantee (64 of its 1,855 keys contain a `lean4` pair-set
character, so pairing running first corrupts them), but the chain is
substrate every language runs through, which is why it ships alone —
framing Q#LN10, and §4's rule that no PR in this arc mixes a
cross-cutting substrate change with Lean feature content.

Three design points worth review attention:

- Consumers are called even when the record is nil. "This fan-out
  carried no typed edit" is information a consumer acts on: it is how
  pairing's test seam observes a non-event, and how Stage 4b will
  abandon a pending abbreviation an unrelated edit invalidated. Three
  existing auto-pairing tests fail if the chain skips consumers on nil.
- The chain pcalls each consumer. `buffer.after-edit` is
  all-must-succeed, so a throwing consumer would otherwise fail the
  fan-out for every other subscriber, including lsp.lua's didChange
  flush. Behavior-preserving for pairing, which already never throws.
- Ordered insertion, not `table.sort`, which is not stable in Lua —
  "ties by registration order" is a stated contract, not a coincidence.

`tests/auto_pair_acceptance.rs` is UNCHANGED — zero lines — and its 45
tests pass. That is criterion 46 and the whole no-behavior-change claim;
a suite edited to accommodate the refactor would prove nothing.

`tests/typed_edit_chain_acceptance.rs` adds 9 tests for criteria
46a-46e. Every one is bite-verified by mutation: appending instead of
ordered insert (5 fail), `>=` for the tiebreak (1), re-taking per
consumer (4), ignoring the claim (1), dropping the pcall (1), skipping
nil fan-outs (1 here plus 3 in the untouched auto-pair suite), and
loading the chain after lsp.lua (the Q#AP7 flush test fails, alongside
the two existing pairing ones).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 13:00:03 -04:00
Levi Neuwirth 174e36fce3 docs(lean4): reconcile peer edits with pending ownership
Advance the Stage 4 framing to revision 8. Keep pending abbreviation
state frontend-owned while conservatively invalidating it after any
intervening shared-buffer edit, make the revision token explicit, and
rewrite acceptance 45i around that contract.

Correct the active-work multi-codepoint count and the stale coherence
revision label.
2026-07-26 10:49:43 -04:00
Levi Neuwirth c4fad0731c docs(lean4): rev 7 — round 6 review, five P1s, and reconcile the ledgers
The 4a/4b split held; five P1s against rev 6's own content, all real,
all reproduced. Four share a root: rev 6 verified its external facts and
under-verified its internal ones.

1. Stage 4a's declared footprint excluded the tests its own acceptance
   required. 46a-46e cannot live in tests/auto_pair_acceptance.rs,
   which criterion 46 requires byte-identical. Footprint now names
   tests/typed_edit_chain_acceptance.rs and gates on it.

2. Pending abbreviation state had the wrong owner. pmacs is
   multi-frontend: EditorCore.views is per-FrontendId with its own
   active window, take_typed_edit is already frontend-keyed, and
   buffer.after-switch fires with no arguments — so a buffer-keyed
   clear-on-switch lets any frontend discard another's pending
   abbreviation. Now keyed (frontend, buffer) with a window check,
   frontend-scoped clearing, a frontend.detached purge, and acceptance
   45i, which the buffer-keyed design passes every other criterion
   without.

3. The shortest-match rule was missing its tie-break: upstream keeps
   declaration order among equal-length shortest keys, and 101 prefixes
   have equal-shortest candidates resolving to different symbols (f
   picks f< over f>). A pairs-iterated Lua map cannot express this, so
   the vendored artifact is now an ordered sequence and resolution sorts
   by (#key, source rank). Rev 6 missed this because it declared the
   package ships no README after a 404 on the package root, with the
   directory listing showing src/README.md already in hand — a 404 on a
   guessed path is not evidence of absence, and the README states the
   rule in one sentence.

4. The generator's rejection rule rejected the current table: \ is a key
   and " begins eleven, while acceptance 45d requires \ to work.
   Replaced with canonical lossless escaping; aborts only on duplicate
   keys, invalid UTF-8, and a failed self-round-trip. 45g no longer
   claims to diff against abbreviations.json, which is not shipped.

5. Durable and volatile state were not reconciled. agent-handoff.md
   anchored main at d152120 with neither #167 nor #170 and no Lean arc
   bullet at all; active-work.md kept 407 lines of merged Stage 1/2/3a/3b
   history against its own instruction to prune merged entries, under a
   stale snapshot date. Durable facts moved to the handoff; the ledger
   keeps only the unlanded Stage 4 lane.

Also corrected: 119 multi-codepoint symbols (26 with $CURSOR), not 93;
three backslash values, not two; Q#LN22 now states the terminating-\
reprocess rule acceptance 45d depended on; acceptance 38 says the
terminator is retained, so undo restores "\alpha " with its space;
coherence cites golden-journey step 5, not step 4; and the
config-registry prior art points at Q#LN22.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 10:39:01 -04:00
Levi Neuwirth ccdf352258 fix(panel): close Stage 2A review round 2 (2 P1, 1 P2)
**P1-1 — the `Invalidated` arm published the panel context on the
document wire.** Real bug, and the live half of the routing defect: the
semantic peer has ONE statusline slot, so emitting an
authoritative-empty payload for every context replaced the document's
with the panel's. Now filtered by document-window identity exactly like
the `Ready` arm; a panel's own clear belongs to `PanelFrame` in 2B.

Pinned by `invalidated_statusline_clears_only_the_document_not_the_panel`,
which reproduces the reported shape — two targets instead of one — when
the filter is removed.

Honest note on the `Ready` arm: its identity selector is **defensive**,
not independently falsifiable today, because the document context is
captured first so "first context for my frontend" happens to pick it.
Rather than leave that as a silent dependency,
`the_semantic_fan_out_captures_the_document_first` pins the order and
says why it matters.

**P1-2 — round-1 finding 3 was not closed; four of my pins were
vacuous.** All four confirmed and fixed:

- The statusline consumer test discarded `render_frame`'s output. It now
  observes the WIRE payload from a v18 peer with a registered provider,
  and asserts non-emptiness so it cannot pass by emitting nothing.
- The terminal test compared two NON-terminal buffers, so both routings
  answered `false`. The document window now holds a REAL terminal, so
  the routes disagree; reverting `semantic_terminal_key` fails it.
- The decorations test used different buffers and an empty selection —
  again the same answer either way. The panel now displays the declared
  buffer with a non-empty selection while the document has none.
- #1/#3/#21 had no discriminating pin at all. Their only production
  caller is `dispatcher_loop`, which no test can drive, so this extracts
  three named seams the loop calls — `document_buffer_to_follow`,
  `document_cursor_byte`, `peer_displays_buffer_as_document` — and pins
  each.

Also newly pinned: #2 the lazy CRDT upgrade (the census's sharpest
case), #7 `Viewport` aligning WITHOUT taking focus, and #9 a focused
terminal panel not suppressing the document viewport.

**Every one of the nine pins was falsified by revert.** Two needed a
second attempt after the first bite came back green.

**P2-3 — stale docs.** `StatuslineEvaluationTarget::Semantic`'s
documentation described evaluating only the focused window; it now
describes the document-plus-side fan-out, the capture order, the
identity-selection requirement, and that `active` reports actual focus.
The ledger's Stage 2A entry is corrected to five commits, 2,014 CRDT
tests, and 16 acceptance tests.

Two clippy findings the refactor introduced were fixed:
`document_buffer_to_follow` is `crdt`-gated to match its only caller,
and the `CursorByte` guard collapses into one `if`.

Gates: fmt clean; workspace clippy clean; 1,832 default + 2,014 CRDT
library; Stage 2A 16; Stage 1 46; statusline 8; m11_5 2; GPU initial
target 14; terminal config 12; folding Stage 2 48; vterm 1/2 10 / 6;
M4 121; required GPU 202; `git diff --check` clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-26 10:38:21 -04:00
Levi Neuwirth 3b54c78494 docs(lean4): rev 6 — re-scout Stage 4 and split it into 4a and 4b
Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against main
@ d400f30 produced six findings that change the plan and three that
confirm it. The pmacs-side facts were verified in a worktree at that
commit; the upstream facts by reading leanprover/vscode-lean4 @ 17d1d08.

The split: Stage 4's risk column read "refactors pair.lua's provenance
read" — every language's auto-pairing — for a stage the prose called the
Lean input method, which is exactly the rule §4 states and exactly what
round 4 found for Stage 3. Rev 5 had noticed the shape and answered it
with a commit boundary; a commit boundary is not a review boundary.
Stage 4a is now the typed-edit consumer chain (substrate, no Lean) and
4b the input method.

Rev 5's expansion semantics were wrong in three ways. Resolution is the
shortest key having the input as a prefix (\al yields ∀ from `all`, not
`alpha`); there is no terminator list at all ('+ ' is a key, so space
extends after \+; '\' is a key, so \\ yields \); and an unmatchable tail
is appended rather than dropped (\alp7 yields α7).

Three further findings. There is no cursor-motion hook, so acceptance 43
as written was not buildable and abandonment is lazy. dispatch_key is
only half of 4b's production path — \ and the letters are not excluded
from the optimistic classifier, and that producer is crdt-gated, so a
crdt-gated integration test is dark in CI and dark in the gate list. And
the whole expansion has cross-peer-degraded undo, a wider bite than
Q#LN6's three bracket pairs; set_round_trip_input would fix it and is
rejected with reasons.

New decisions Q#LN21 (undo degradation) and Q#LN22 (the state machine);
Q#LN10 and Q#LN11 rewritten; §2.11 records the upstream algorithm; §9.1
states the coherence impact for both stages. Acceptance keeps its
existing numbers and adds letter suffixes on both sides of the split.

Citation sweep per COHERENCE §25: five live citations moved in the 50
commits since rev 5.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
2026-07-26 10:10:06 -04:00
Levi Neuwirth 6b2b0f9dd2 fix(panel): close Stage 2A review round 1 (4 P1, 2 P2)
Integrates canonical `main` @ `cf54270` and closes every finding.

**P1-1 — a stale document `Pointer` stole focus from the panel.** Real
bug. `align_primary_document_window`'s unknown-buffer arm returned
`Some(window)` despite aligning nothing, so #8's activation focused the
document *before* `dispatch_pointer` rejected the mismatched buffer. It
now returns `None`: alignment did not happen, so no caller may treat it
as a document gesture.

Pinned through `handle_dispatcher_event` — the real dispatcher seam —
because the defect lived in the PAIR of alignment and activation, not
in either alone. **The first version of that test was vacuous**: an
unregistered session is dropped at `daemon.rs:1962` (#148's
membership check) before the aligner runs, so it passed with the bug
restored. It now registers a real semantic session and fails with
exactly the reported symptom, focus moving `WindowId(2)` →
`WindowId(3)`.

**P1-2 — the approved A2A-2 fan-out was missing.** The semantic target
returned one context. It now captures the primary document PLUS the
visible side window, each provider invoked once, with a
derived-hidden side omitted (Q#BP2b — no mode line to paint, so no
callback should run for it). The acceptance asserts `windows.len() == 2`.

This exposed a second defect the finding did not name: the consumer
selected segments with `.find(|w| w.context.frontend_id == frontend_id)`
— the FIRST context for the frontend. With two contexts that silently
depended on capture order and could have shipped the panel's mode-line
text as the document status band. `emit_statusline_segments` now takes
the document `WindowId` and selects on window identity.

**P1-3 — the census suite tested the authority, not the consumers.**
Confirmed: reverting a producer to `active_window_for` left all ten
tests green. Added consumer-level pins that drive the real producers
through `SemanticRenderState::render_frame` with a panel focused, plus
the terminal-declaration guard. Bite-verified: reverting the
`LineNumbers` routing now fails
`consumer_line_numbers_follow_the_document_not_the_focused_panel`.

**P1-4 — main integrated.** The textual conflict was `docs/active-work.md`
(both lanes rewrote the same region; the terminal-config lane is kept
whole and the bottom-panel heading updated). `src/editor.rs` auto-merged,
and the full gate suite was rerun on the merge result.

**P2-5 — the painter test was vacuous.** A fixed-point check that
survived deleting `window.text_view.render`. It now asserts each of the
four extracted outputs actually appears: buffer TEXT, the line-number
GUTTER (with line numbers explicitly enabled, rather than dropping the
assertion), the window MODE LINE, and a returned caret. Bite-verified
by deleting the render call.

**P2-6 — the stale fold-projection claim is corrected.**
`src/window.rs`'s `fold_projection` doc no longer asserts that a
semantic session never enters `paint_frame`; it records that the panel
band breaks that premise and that the extracted painters take the map
as a parameter.

Gates on the merge result: fmt clean; workspace clippy clean; 1,832
default + 2,010 CRDT library tests; Stage 2A acceptance 13; Stage 1 46;
statusline 8; m11_5 2; GPU initial target 14; terminal config 12;
folding Stage 2 48; vterm 1/2 10 / 6; M4 121; required GPU 202;
`git diff --check` clean. `vterm_stage3_acceptance::a37` remains the
pre-existing flake measured on the base commit.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-26 10:02:01 -04:00
Levi Neuwirth d400f30c06
Merge pull request #170 from levineuwirth/lean4-stage3b-server
feat(lean): the Lean 4 language server (Arc 8 Stage 3b)
2026-07-26 13:49:16 +00:00
Levi Neuwirth 6f348c9285
Merge pull request #167 from levineuwirth/lean4-stage3a-seams
feat(lsp): notification/response dispatch seams and fs.canonicalize (Arc 8 Stage 3a)
2026-07-26 13:47:46 +00:00
Levi Neuwirth f78a5beedc Merge branch 'lean4-stage3a-seams' into lean4-stage3b-server
# Conflicts:
#	docs/active-work.md
2026-07-26 09:36:18 -04:00
Levi Neuwirth 23486fd572 Merge main, and fold #173's a37 findings into the CI-coverage lane
Integrates githubsucks/main @ cf54270 (terminal config Stage 1, #173).
Both conflicts were additive appends to the same lists — the handoff
preamble and the ledger's "Closed since the last snapshot" — so both
sides are kept and the preamble now leads with #173.

Also records what gating #173 measured about a37, because it changes
this lane's proposed fix rather than merely annotating it:

a37 reports `ok` without running whenever `pmacs-gpu` is absent from
the target directory. A fresh worktree reports the Stage 3 suite 9/9 in
0.17 s having never executed the arc's only real-daemon/real-PTY/real-
wgpu path; a genuine run takes about four seconds. Only
PMACS_REQUIRE_GPU=1 promotes that skip to a failure, and the standing
gate list applies that flag to `cargo test -p pmacs-gpu`, a different
package. So fix-shape part 2 must state the flag as a requirement of
the gpu-render job: a crdt leg added to the plain `test` job would run
a37 vacuously and report green.

a37 is also load-sensitive — it passed at d152120 and failed at that
same commit twenty minutes later under machine contention — which makes
a red first CI run ambiguous by construction. The lane now says to
re-run on the merge base before believing a failure, and to prefer
serialized execution over retry-until-green.

The vterm audit's "only 3 of 9 Stage 3 tests drive a real daemon" is
corrected: without the frontend binary the honest number is 2.

Ledger: terminal config Stage 1 flipped from IN REVIEW to MERGED.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-26 09:29:42 -04:00
Levi Neuwirth 7243714b3f Merge remote-tracking branch 'githubsucks/main' into lean4-stage3a-seams
# Conflicts:
#	docs/active-work.md
2026-07-26 09:25:25 -04:00
Levi Neuwirth cf54270173
Merge pull request #173 from levineuwirth/terminal-config
feat(terminal): profiles, scrollback, and a configurable escape key
2026-07-26 13:21:38 +00:00
Levi Neuwirth dec51960da docs: record round-six bite evidence
Capture the concrete counterfactual outcomes for all five review fixes
against 19f48d4.
2026-07-25 22:36:02 -04:00
Levi Neuwirth 3b7cc67197 docs: record the sweep-found test race in the lane
The parallel sweep failed one of the new tests for a real reason, not a
flake: drain_until ticks, and a tick can reap an immediately-exiting
child before the diagnostic runs. Recorded with the matched-load
measurement that shows the fix is load-bearing (0/15 fixed vs 1/10
unfixed under full saturation), and the final sweep numbers.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 22:33:22 -04:00
Levi Neuwirth 786de69d38 fix(lsp): close round-six Lean fallback gaps
Make command-time attachment healing cancel an armed terminal restart
before replacing the server, while keeping request-only lookup pure and
restart-safe.

Track config-driven server ownership privately, bound every fallback
server per SID, scope no-swap retirement to the failed root, and route
the shipped Lean diagnostics command through the safe resolver while
waiting for initialization.

Add direct acceptance counterexamples for all five review findings and
record the sixth-round verification and vacuity lesson.
2026-07-25 22:32:48 -04:00
Levi Neuwirth 00cc615db5 test(process): read the pid without ticking in the fast-exit tests
The parallel workspace sweep failed
observing_the_leader_does_not_consume_the_exit_event with "process
ProcessId(26) is not running". A real defect in the test, not a flake.

The helper that fetched the pid drained for the Started event, and
draining ticks. A tick can observe an immediately-exiting child and
transition the record out of Running, after which signal returns "is not
running" and never reaches the diagnostic -- so the loop spun to its
10 s bound and panicked. It passed standalone because the drain returned
on Started before poll_one saw the exit; only the sweep's load shifted
the timing enough to lose that race.

Fast-exiting children now read the pid straight from the supervisor
record, which does not tick. The bounded loop also fails fast when the
record has left Running, so a future recurrence is diagnosed in one line
rather than surfacing as a timeout.

Verified under matched load: 15/15 green with all 16 cores saturated.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 22:25:05 -04:00
Levi Neuwirth 18d481b046 docs: record the PTY terminate diagnostic lane in the ledger
The ledger's own update protocol requires a lane for volatile work, and
PR #176 had none: branch, worktree, review state, and verification were
all missing.

Records why the lane ships a diagnostic rather than a fix -- three
rejected tolerance designs, the two facts that killed the original
argument (group=true is rejected for PTY mode so the reap ledger never
applies to that path, and the ledger comment asserts EPERM cannot happen
rather than ruling that it means dead), and that the CI evidence never
established the child had exited.

Also records the round-1 test fixes and the four verified bites, so a
reader can tell which assertions are load-bearing.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 22:19:19 -04:00
Levi Neuwirth 00e096ef81 Merge remote-tracking branch 'githubsucks/main' into pty-terminate-eperm 2026-07-25 22:18:32 -04:00
Levi Neuwirth 40f7f81690 test(process): pin exact diagnostic values and drop the timing-dependent sleeps
Round-1 review found both test weaknesses.

The exited-child tests used a fixed 300 ms sleep as proof the child had
exited, which on a loaded runner can be false and would turn them into
spurious failures. nix's waitid is unavailable on macOS and libc::waitid
would need unsafe, which the crate forbids, so the tests now synchronise
on the observation under test: a bounded loop that drives the production
diagnostic until it reports the leader as exited. Each failing attempt
leaves the record untouched because the failure path returns before any
bookkeeping, so the loop is side-effect free, and it is strictly stronger
than a sleep because it observes the actual state rather than assuming it.

The assertions were substring checks -- target=-, expected_group=-,
leader=exited( -- which a hardcoded target or a wrong exit code would
satisfy. They are now exact message equality built from the pid the
kernel actually assigned and the errno's own Display, and the one-event
test asserts the surviving event carries exit code 7 rather than any
terminal event. The group test also spawns /bin/sleep directly rather
than through a shell, since a shell may place the command in a different
foreground process group than the one being asserted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 22:16:56 -04:00
Levi Neuwirth 4413ea93d0 docs: record the Stage 2A lane and what gating it found
Ledger entry for the in-flight Stage 2A branch, plus three findings the
gate run produced that are worth carrying regardless of this PR:

- The structural test comparing the two authorities directly did NOT
  catch the focus-class bite; only the consumer-level assertion did.
  Both kinds are needed, and the distinction generalizes.
- `vterm_stage3_acceptance::a37` is badly flaky on this machine —
  6/8 failures on the BASE commit against 7/8 on the branch in matched
  isolated samples, so it is pre-existing rather than a regression. It
  also returns `ok` without running unless `pmacs-gpu` is built.
- `m11_5_semantic_acceptance` reports 0 tests and
  `gpu_initial_target_acceptance` reports 1 without `--features crdt`.
  Both are semantic-census suites, so gating Stage 2A in the default
  config alone would exercise almost none of its relevant coverage.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 22:14:37 -04:00
Levi Neuwirth d7ad01b535 feat(panel): extract the per-window painter + Stage 2A acceptance
Bottom-panel Stage 2A, second half (Q#BP8, Q#BP17). Still no protocol
change and no behavior change: `paint_frame` builds the same fold map
it always did and passes it in, so grid rendering is unchanged.

Two extractions, both taking the fold map as a **parameter** rather
than building it:

- `prepare_window_cursor_visible` — the active-window auto-scroll
  clamp. The panel band (2B) runs this for its own window when that
  window owns focus, and leaves a passive panel's `view_top` alone.
- `paint_window_content` — the per-window document body: text, gutter,
  overlays, selection, and the mode line. The panel paints into a
  panel-sized grid at the same origin-agnostic `Viewport`, so this is
  that body lifted out, not a second painter (Bet B2').

The parameter is the point (Q#BP17). Folding built its per-window map
ungated on the premise that "a semantic session never enters
`paint_frame`", which the panel band breaks. The panel path must pass
`None` for a frontend whose `fold_projection` is false, and must not
call `EditorCore::fold_map_for_window` — that gates on the **active**
frontend, which is right for command-time reckoning and wrong for
painting another frontend's panel.

`tests/bottom_panel_stage2a_acceptance.rs` — 10 tests. The negative
half is the load-bearing half, so Projection assertions are paired
with focus-class assertions taken in the SAME state:

- `focus_and_projection_disagree_in_the_same_state` is the key one:
  with a panel focused, the focus authority must name the panel while
  the projection authority names the document. Routing the focus class
  through `primary_document_window` fails this even though every
  Projection test still passes.
- The statusline pair pins the split: the LOOKUP resolves the document
  window while `active` reports actual focus, with a non-vacuity twin
  that flips `active` back to true when focus returns.
- The extraction pair pins cells, the returned cursor, the focused
  window's `view_top`, AND a passive window's untouched scroll —
  identical cells alone would not catch a clamp that moved to the
  wrong window on a single-window frame.
- `the_panel_fixture_really_builds_a_side_window` pins the fixture's
  own precondition, since every other test is worthless if
  `focused_panel` silently produced an ordinary split.

One crdt-gated caller of the old `align_semantic_window_to_buffer` was
updated; it compiles only under `--features crdt`, which is the
config CI never runs.

1,832 default + 2,009 CRDT library tests, 10 new acceptance; fmt and
workspace clippy clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 22:04:56 -04:00
Levi Neuwirth b76da70d5d feat(panel): route the Projection half of the §1.3 census (Stage 2A)
Bottom-panel Stage 2A, first half. Every consumer the framing classifies
**Projection** now resolves the frontend's primary document window or
buffer instead of its focused one; every consumer classified focus,
focus-chrome, or focus/session is deliberately left alone.

No protocol change, no behavior change for any frontend today: with
`panel_capable = false` for semantic sessions, `primary_document_window`
returns `view.active` for every existing configuration, so this is a
seam adoption that becomes load-bearing in 2B.

Projection consumers routed:

- **#1** semantic buffer-follow / `BufferSnapshot` re-send
- **#2** the lazy CRDT upgrade — the sharpest case, since it BROADCASTS
  to every replica, so keying it on focus would let focusing a fresh
  generated panel buffer swap every peer's document mirror
- **#3** `CursorByte`
- **#4** `LineNumbers` mode
- **#5** selection decorations
- **#6/#10/#11** the full-window semantic terminal declaration, its
  snapshot/sync, and terminal-frame suppression, via the shared
  `semantic_terminal_key` resolver
- **#9** the `Viewport` terminal-context gate — a focused terminal panel
  must not suppress the still-visible document's viewport
- **#12** the semantic statusline target LOOKUP
- **#21** the `BufferSnapshot` publication recipient filter

`align_semantic_window_to_buffer` splits per Q#BP14, which is the
distinction that makes rejecting panel-named events insufficient on its
own:

- `align_primary_document_window` (**#7**, `Viewport`) — aligns the
  document window and **never touches `view.active`**.
- `align_and_activate_primary_document_window` (**#8**, `Pointer`) —
  aligns and then activates, because a click in the document area means
  "work here". This is the one place projection and focus legitimately
  move together.

`dispatch_semantic_terminal_pointer` (**#11**) gains the same rule: an
accepted non-`Move` gesture activates the document window before the
gesture replays, while bare hover neither focuses nor claims.

The statusline change is deliberately a HALF change (parent acceptance
42): the window LOOKUP resolves the primary document window, but
`active` still reports **actual focus**, so a document provider can
truthfully observe `active = false` while a panel owns focus.

Untouched, and that is the load-bearing negative: #13 remote-op
validation, #14 `dispatch_idle_for`, #15 presence, #16-#19 search /
menu / minibuffer / completion chrome, #20 terminal bell drain, and #23
remote-op application all still resolve the actually focused window.
#16-#19's Q#BP14b routing table needs `PanelFrame` and lands in 2B.

1,832 library tests pass; fmt and workspace clippy clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 21:53:41 -04:00
Levi Neuwirth 56eaf2f07a Merge remote-tracking branch 'githubsucks/main' into terminal-config
# Conflicts:
#	docs/active-work.md
2026-07-25 21:50:25 -04:00
Levi Neuwirth 8e8f281f0e fix(terminal): close review round 1 on Stage 1
Five findings, all real. The blocker and both majors are the same
mistake in three places: a claim asserted somewhere cheaper than where
it actually lives.

COHERENCE.md was stale in four places, not the three reported. Step 8
still read "no keybinding" and §11 still read "five settings", but §6's
dispatch table also still cited `is_terminal_escape_chord` — a symbol
this branch deletes. §25 requires that update to ride the PR, so a PR
changing audited ground truth has to re-grep the audit for its own
symbols, not only for its topic.

Acceptance 5 asserted a registry round-trip, which is a test of the
registry: it stayed green with the setting's only consumer deleted. It
now opens a real terminal whose child overflows the 24-row screen,
scrolls the view to its oldest retained row, and asserts LINE001 is
present at 10,000 and absent at 0.

Acceptance 8a waited for the session count to fall, which the rejected
editor-side cache map satisfies exactly — a map with no purge hook
leaks while sessions drain. Adds `TerminalManager::escape_caches()`, the
lifetime half of Q#TC4c's contract that `escape_parses` cannot cover.

`table.sort` over `pmacs.terminal.profiles` raised "attempt to compare
number with string" on the unknown-profile path whenever the user's
table held both a string and a numeric key, replacing the exact
diagnostic being asked for; `%q` raised likewise on a non-string
`profile` argument. Both are partial functions applied to user input on
a diagnostic path.

Also corrects the framing's status line, and a status message whose
embedded whitespace run had survived a rustfmt reflow.

Three new bites, each falsified by revert: deleting the scrollback
consumer fails acc5 and only acc5; restoring the raw-key sort
reproduces the comparison error verbatim; and implementing the rejected
map fails the new acc8a at left: 2, right: 1 while passing the old
session-count version.

Merges githubsucks/main @ ccf29e3.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-25 21:47:37 -04:00
Levi Neuwirth 52731ba121 style: pass Errno by value (clippy pedantic)
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 21:30:23 -04:00
Levi Neuwirth 19f48d46c0 fix(lsp,lean): bound the fallback's own failure; heal at point of use
Round 5 review: one P1, a frontend scope hole, and three P2s.

**1. A fallback that SPAWNS and then dies retried forever.** The
once-per-buffer guard bounds calls to `_attach_buffer`, not the server
those calls produce. `ensure_server` still never forwards `cfg.restart`,
so the fallback inherits `OnCrash`; an executable that exits before
`initialize` is respawned by the manager with no attempt ceiling —
silently, because `latched` has already disabled the primary's failure
poll. The fallback now gets its own one-shot die-before-initialize
watch, which retires it (ending the respawn loop) and reports.

The prior failing-fallback test used a NONEXISTENT executable, so it
only ever exercised synchronous ENOENT. To reach "spawned, then died"
the fixture has to actually spawn.

**2. Simultaneous frontends.** Both repair triggers read the ambient
`pmacs.window.buffer()`, and the daemon restores `active_frontend` to
the last-dispatched frontend before `tick_processes` — so a Lean buffer
active in ANOTHER frontend receives no `buffer.after-switch` here and
stays stale after its server is globally retired.

Fixed at the seam that is frontend-agnostic: **make consumption safe.**
`attached_for_active` now rebuilds rather than returning a record whose
server is dead, and `attachment_for_request` reports none (it must not
perturb LSP state, so it cannot rebuild). Whichever frontend runs a
command is the active one while it runs, so healing at the point of use
reaches every buffer no eager sweep can. This also closes the half where
a dead attachment was handed to a command and the request vanished.

**3. The retirement sweep stopped user-managed servers.** Selecting on
`language_id == "lean4"` also names servers the user spawned from
`init.lua`, which are not derived from `pmacs.lsp.config.lean4`. It now
keys on the `default-lean4` label `ensure_server` stamps — the
derivation discriminator.

**4. Repair ran even when no swap occurred.** `swap_to_fallback()`
returning false left `latched` true, so the next tick retried the
UNCHANGED configuration and reported it as a fallback failure. Split
into `probe.fallback_installed`: repair exists to apply a swap, so no
swap means nothing to apply.

**5. The once-per-buffer assertion counted table keys**, which cannot
distinguish "once per buffer" from "every tick for one buffer" —
cardinality stays 1 either way. Replaced with a numeric attempt counter;
the bite reports 174 attempts against the expected 1.

Five bites, each against 7c37bdc: no fallback watch -> attempt reaches
4; retire by language_id -> the user's server is stopped; gate repair on
`latched` -> a repair is attempted with no swap; drop the
once-per-buffer guard -> 174 vs 1; hand back a dead attachment -> a
command receives a `stopped` server.

Two more vacuity shapes recorded in the ledger (8 and 9): counting
distinct keys cannot bound repeated work, and a nonexistent executable
cannot reach any post-spawn failure.
2026-07-25 21:28:11 -04:00
Levi Neuwirth 62316a9ced fix(process): make a failing kill describe itself (Q#PD1)
A failing kill in ProcessSupervisor::signal reported an errno and
nothing else, which is not enough to diagnose the macOS CI failure that
prompted this lane: three different hypotheses about that EPERM produce
the same message, and the fix each one implies is different.

The error now carries five facts as separate fields: the target source
(which branch of signal_target ran), the target kind and value, the
spawn-time group for a group-directed signal, the errno, and the
spawned leader's real try_wait state.

Keeping the target and the leader apart is the whole point. For a PTY
the signal goes to the terminal's foreground process group, read from
the tty at signal time, while the leader is the child that was spawned.
Those are different entities whenever job control has moved the
terminal, and three rejected designs for this code were unsound
precisely because they concluded something about one from the other.
The report states both and concludes nothing.

The disposition is unchanged. Every call that failed before still
fails, with no state transition and no reap-ledger arming. That is
asserted directly rather than assumed, because it is what separates
this from the tolerance rules review rejected.

Q#PD3, stated narrowly: this is not a pure message change. Consulting
try_wait reaps an exited child and caches its status, so the child may
be reaped earlier than it otherwise would be. That is observably safe
because portable-pty 0.9.0 returns a std::process::Child on Unix and
delegates try_wait straight to it, so the status is cached and poll_one
still sees it -- but safe by argument is not safe by assertion, so a
test forces a kill failure against the real PTY child and then checks
that exactly one terminal event survives.

Q#PD4: the test seam injects the kill attempt's result only, never the
observation. Target selection, the real ChildHandle::try_wait against
the real child, and the error construction all run unmodified; a
stubbed observation would bypass the code path under test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 21:25:58 -04:00
Levi Neuwirth dd581cd90c docs: frame the PTY terminate diagnostic (revision 4)
A docs-only PR (#172) failed Test (macos-latest / luajit) on
acc28_child_input_and_the_c_c_escape_work_unchanged_in_a_panel with
"kill: EPERM: Operation not permitted" raised out of terminate. A docs
diff cannot cause that, main was green at the PR's exact base, and three
other PRs passed the same job.

This framing reaches revision 4 after three review rounds, and what it
proposes is much smaller than what it started with. Revisions 1 to 3 each
proposed a tolerance rule -- treat some errno as success -- and each was
unsound in the same way: they concluded something about a process from
something that was not about that process. Revision 1 concluded from an
errno alone, which says only that a syscall failed. Revision 2 concluded
from the spawned leader while a PTY signal targets the tty's foreground
process group, which diverges from the leader exactly when job control is
in use. Revision 3 corrected EPERM but kept group-directed ESRCH, which
proves only that the selected foreground group vanished, not that the
leader exited.

So no tolerance rule lands. The disposition is preserved exactly: every
failing call still fails, with no state transition and no ledger arming.
What lands is that the failure explains itself, recording the target
source and value, the spawn-time pgid or leader pid, the errno, and the
leader's real try_wait state as five separate facts. Every candidate fix
is decidable from those together and none is decidable from the errno
alone.

Two claims are stated more narrowly than earlier revisions had them.
Consulting try_wait reaps an exited child and caches its status, so this
is not "strictly additive" -- it is "no disposition change", with an
event-count test pinning that poll_one still emits exactly one exit
event. And the test seam injects the kill attempt's result only, never
the observation, so the real ChildHandle::try_wait runs against the real
child; a stubbed observation would bypass the path under test.

Parked with their reasons: all tolerance rules, terminate becoming
idempotent for an already-reaped process (an independent fix answering a
different failure), and signal_target's read-then-kill of tcgetpgrp,
which is the most likely real fix site.

The lane closes when this lands rather than waiting for the flake to
recur; the next occurrence carries its own evidence under whoever's PR.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HZjWMjwPXhPbt9upku9mCk
2026-07-25 21:12:51 -04:00
Levi Neuwirth c93f9eeeaa
Merge pull request #175 from levineuwirth/bottom-panel-stage2-framing
docs: bottom-panel Stage 2 framing (GPU panel band)
2026-07-26 00:55:14 +00:00
Levi Neuwirth 4fbd47f025 docs: refresh the handoff's Stage 2 status (COHERENCE §25)
`docs/agent-handoff.md` §1 still said Stage 2 "needs its own
re-framing". It is framed, so that line would be false on `main` the
moment this branch merges.

It now records the approved shape — protocol v21, two serial slices
(2A census routing + painter extraction, then 2B wire/projection/band/
capability flip), parent acceptance 37-55 still authoritative — and
carries the census classification rule itself, since that is the fact
the ledger previously got wrong and the one a future reader is most
likely to re-derive incorrectly.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 19:49:19 -04:00
Levi Neuwirth 7c37bdc514 fix(lean): repair every buffer and retire every server on fallback
Round 4 review: one P1, and it is the same defect for the FOURTH time.

`pmacs.lsp.config.lean4` is a single global entry, so swapping its
command invalidates **every** Lean buffer and **every** Lean server —
Q#LN15 gives one server per project root, so there can be several.
Rounds 1-3 each repaired one buffer and retired one server, and round 3
shipped "repair the armed target, strand the rest": status and config
said fallback while a second open Lean buffer stayed on the retired
command, and a second project root's server stayed live.

The shape that actually holds:

  * **Retire ALL `lean4` servers on latch**, not the one the probe
    happened to name. `probe.primary` identifies the server the VERDICT
    is about; it was never the set of servers the swap invalidates.
  * **Repair each buffer lazily and at most once**, when it becomes
    active — on `buffer.after-switch` and on the tick. `_attach_buffer`
    is an active-buffer-only seam, so a global swap cannot be applied to
    every open buffer at once; it has to be applied as they surface.
    lsp.lua's own `after-switch` re-pushes views but does not rebuild a
    stale attachment, so nothing else covered this.
  * The **once-per-buffer bound** is load-bearing: without it a fallback
    that also fails to spawn would retry every tick forever — the
    round-2 defect, which a naive global repair loop would reintroduce
    for every buffer instead of just one.
  * `shutting-down` is deliberately not treated as stale. It is still
    live by `server_is_live`'s reckoning, so attaching would early-return
    the stale record and burn that buffer's single attempt on a no-op.

P2: argument-inclusive attribution was implemented in round 3 but pinned
only by "contains the command name", so a mutation dropping every
argument passed. Now asserted against the exact `<command> <args>`
string.

Also fixed a vacuous assertion this refactor created: a test checked
`_probe.reattach_from == nil` for a field that no longer exists, which
reads as nil and passes for nothing. It now asserts a positive count of
recorded repair attempts.

Three bites, each against 73587b0: repair only the armed buffer -> the
second buffer stays on `lake`; retire only the named server -> one live
stale server remains; drop arguments from attribution -> the exact-string
assertion fails.

The ledger records a second durable lesson beside the vacuity one: **a
scope error repeats until the scope is named.** Four rounds of locally
correct fixes, none of which asked what the config swap invalidates.
When a change edits shared state, enumerate everything derived from it
before repairing anything.
2026-07-25 19:46:29 -04:00
Levi Neuwirth 49757e51a8 docs: bottom-panel Stage 2 framing (revision 4)
Closes review round 3 — 1 blocking, 1 high, 1 medium.

**R3-1 (blocker) — the call-site table contradicted the source.** The
three-boundary model was right; five rows of its classification were
not, and each was a real defect:

- `:6140` is `completion_dropdown_layout` — DOCUMENT completion
  placement, deriving the space below the anchor line. Classified
  status-owned, it would let completion overlap the panel.
- `:7195` and `:7212` are the `status_buffer` / `status_left_buffer`
  `TextBounds.top` — status text bounds, classified document-owned.
- `:7351` clips global minibuffer CANDIDATE glyphs to the dropdown's
  band anchor; classified document-owned, they would be clipped
  against a boundary the dropdown does not sit above.
- `:8561` (`edge_scroll_direction`, document edge scrolling) was
  missing entirely, leaving it tied to the old bottom.
- `:8077` is `code_caret_rect_in_clip` — caret clipping, not
  completion placement. Its class was right, its label wrong.

Every production site is now individually verified against the source
and tabulated with what it actually is. The census is stated as
arithmetic a reader can check: 29 matches = 20 production + 1
definition + 8 test sites.

Root cause recorded in the revision history: rev 3's table was built
from a `grep | head -20` over 29 matches, which is precisely why
`:8561` vanished. The minibuffer's status-owned status is now argued
from Q#BP14b rather than assumed — it is global, bufferless chrome
anchored to the status band, so all four of its sites stay with the
band.

**R3-2 (high) — clamps preserved.** The three equations permitted
negative coordinates on a surface shorter than its chrome, where
today's `text_area_bottom` clamps with `.max(0.0)`. All three now
clamp at zero, which keeps the "exact formula" exact exactly where it
matters most.

**R3-3 (medium) — attachment rejection classified SHARED.**
`validate_cells` also rejects `cell.attachment.is_some()`
(`terminal.rs:305`), whose error text reads "which terminals never
use" (`:190-191`) — phrased as a terminal-specific fact, which is why
rev 3's "exact split" missed it. Panels implement no attachment
rendering in Stage 2, so a `PanelFrame` carrying one describes a
surface the GPU would silently not draw; shared rejection fails closed
on the producer side instead. The message is reworded grid-neutral
when it moves, and giving panels attachment rendering later moves the
rejection back deliberately rather than by default.

A2B-4 now names the counts on both sides (twelve document-owned move,
eight status-owned do not) and carries the three symptom-bearing rows
that a plausible misclassification produces. §9 records that the GPU
three-boundary split belongs to 2B, not 2A — it is only observable
once a band can be installed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 19:36:58 -04:00
Levi Neuwirth e1db5bb392 Merge remote-tracking branch 'githubsucks/main' into terminal-config 2026-07-25 19:32:25 -04:00
Levi Neuwirth 73587b0e37 fix(lean): correlate the probe verdict with its own server and buffer
Round 3 review: two P1 asynchronous-correlation defects, with the
focused suite at 25/25 while both were live.

**1. A late version verdict retired nothing and claimed success.**
`probe.watching` is cleared the moment the server initializes — it is
failure-polling state. A slow `lake --version` landing after a
successful initialize therefore reached `fire_latch(nil)`, which retires
nothing: `_attach_buffer` found the still-live primary attachment,
early-returned it, and the retry counted that as done. Status said
"falling back", the config named the fallback, and the buffer stayed on
the old server.

**That is the round-1 silent no-op arriving through a third event
ordering** — first as "no re-attach at all", then as "re-attach cleared
by an unrelated buffer", now as "re-attach satisfied by the server we
were supposed to replace". The fix separates the two facts that were
being carried by one field: `probe.primary` is the server the verdict
applies to and survives initialization; `probe.watching` is the
failure poll and is cleared by it.

The existing fixture could not reach this ordering at all — its `serve`
sleeps, so the primary can never initialize before `--version` returns.
The new one execs the fake LSP for `serve` and delays 0.6s before
reporting 3.0.0.

**2. `buf_key` was the most recently loaded Lean buffer.** Written on
every Lean `buffer.after-load`, so a second Lean file opened before the
verdict became the rebuild target while the latch still watched the
FIRST buffer's server. Target buffer and primary server are one fact and
are now armed together, exactly once. Both files in the new test share a
package, so mis-targeting shows up as a stranded buffer rather than as
two unrelated servers.

**3. The failure message hardcoded `lake serve`** after the latch became
command-agnostic, telling a user whose `my-lean-wrapper` failed to go
debug lake. `configured_command()` names what is actually configured,
arguments included.

**4. The ledger** now records all fifteen bites across the three rounds,
both prior review rounds' findings (the round-2 block was lost when an
earlier edit script aborted before writing), and the durable lesson.

That lesson, recorded for the handoff: **six tests across three rounds
were written, ran green, and pinned nothing** — caught only by biting.
The shapes are enumerated in the ledger; the rule is that a test is not
evidence until the mutation it targets has been shown to fail it. Two
of the six are subtle enough to be worth naming here: a bite that
RAISES is swallowed by the hook's pcall and "passes" for the wrong
reason, and a fixture whose `serve` sleeps cannot reach any ordering
where the primary comes up first.
2026-07-25 19:23:50 -04:00
Levi Neuwirth 857a86ff59 docs: bottom-panel Stage 2 framing (revision 3)
Closes review round 2 — 1 blocking, 2 high, 1 medium — decides both
remaining open items, and re-integrates canonical `main` @ `ccf29e3`
(#172 + #157; documentation plus one `src/buffer.rs` regression test,
no protocol or Stage 2 source anchor moved).

**R2-1 (blocker) — the seam is three boundaries, not one.** Rev 2 asked
for a single document-bottom accessor. That is wrong: once a panel is
installed the present single value must DIVERGE, because several of its
consumers must not move at all. `text_area_bottom`
(`pmacs-gpu/src/main.rs:8490`) is today `status_band_top`,
`geometry_capacity_bottom`, and `document_text_bottom` at once. Rev 3
defines all three, classifies every one of its ~19 call sites as
status-owned / document-owned / geometry, and records that four sites
rev 2 named (`:3175`, `:3185`, `:6601`, `:6607`) consume a status-band
HEIGHT and no bottom coordinate at all, while the status background
`:5908` and status text `:7134`/`:7922` must stay at the physical
window bottom.

The acceptance is now a contrast assertion: installing a panel moves
every document-owned consumer WHILE the status band stays
pixel-identical. "Everything moved" alone is passed by a blanket
rewrite of the helper, which is exactly the wrong implementation.

**R2-2 (high) — epoch exactness.** `accept_frame_geometry` returns
`Advanced | Duplicate | Rejected` instead of a boolean that cannot
separate reconcile-needed from already-current from stale; if a boolean
is ever kept internally it must be named `advanced`, since `Duplicate`
is also accepted. Rev 2's exhaustion wording permitted retaining stale
geometry, which is not fail-closed — a real resize after exhaustion
would keep painting a panel sized to disowned geometry. The grid path
now clears `frame_geometry` to unknown and reconciles hidden, and the
frontend takes a terminal latch so a retained matching `Present` cannot
resurrect the band; only a fresh session clears it.

**R2-3 (high) — parent acceptance 52 splits.** 2A has no semantic panel
projection, so it can only prove the extracted painter honors an
explicit `None` map plus the `src/window.rs:562` comment fix. The real
contract is production-reachable only in 2B and is reasserted there
beside 42/43/44.

**R2-4 (medium) — touched gates named**: `statusline_segments_acceptance`,
`m11_5_semantic_acceptance`, `gpu_initial_target_acceptance`,
`gpu_font_acceptance`, beside the vterm, folding, and GPU suites.

Open items decided: `BASE_DIVIDER_HEIGHT = 4.0` at scale 1.0, scaled by
`FontMetrics::scale`, whole strip painted `ui.divider` and used as the
exact hover/drag hit rect; `TEXT_TOP` stays `16.0` unscaled, with
Q#BP15a's "all quantities use the frontend's current scale" narrowed to
font-derived metrics and the divider. Wholesale surface-inset/DPI
scaling is recorded as separate work, not smuggled in.

The ledger's bottom-panel lane keeps its census correction and gains
the three-boundary one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 19:23:49 -04:00
Levi Neuwirth 69f9a1bdf9 docs: bottom-panel Stage 2 framing (revision 2)
Closes review round 1 — 2 blocking, 3 high, 3 revision points — and
rebases the ground truth onto `main` @ `d152120`.

Both blockers were rev 1 asserting something the parent framing
already decided otherwise:

- **R1-1.** Rev 1 said all 23 census reads route through
  `primary_document_window`. Q#BP14 routes only the **Projection**
  class that way; focus/input (#13-#15, #23), focus chrome and
  surface-routed (#16-#19), and focus/session (#20) keep their own
  authorities. Rev 1's rule would have broken remote-op validation and
  application, `DispatchIdle`, presence, focused search/menu/completion
  routing, and terminal bell ownership. §3.2 restores the four classes
  as a table and the acceptance asserts each separately — the
  focus-class assertions are the load-bearing half, since a test that
  only proves "the document is used" passes with them wrongly
  rerouted.
- **R1-2.** The three `src/statusline.rs` active reads have two
  dispositions, not one. Only `:644` selects the wrong window; `:629`
  and `:675` must keep tracking actual focus, because grid contexts
  need a truthful `active`, revalidation must notice a focus change,
  and parent acceptance 42 requires a document provider to be able to
  observe `active = false` while the panel is focused.

The three high findings:

- Q#BP2S1 resolves to frontend-owned epochs (option 1) — a font or
  scale transaction can need to invalidate an old `PanelFrame` while
  the derived `CellSize` is identical, which daemon value dedup cannot
  detect. Rev 2 adds the four-row transition table, splits grid
  allocation from semantic acceptance into two APIs rather than one
  ambiguous method, moves the grid allocator off `saturating_add` to
  checked-with-fail-closed, and defines the initial epoch and both
  exhaustion behaviors. Rev 1's "rejects a lower-or-equal epoch
  carrying different data" was itself wrong: a lower epoch carrying
  identical data is still stale.
- The `panel_capable` flip is narrowed to an authenticated semantic
  session negotiated at **v21 or later**. Denying a v20 peer the new
  events is insufficient if the daemon still places its window in a
  side panel it cannot render — the gate is on placement.
- Parent acceptance criteria 37-55 are declared authoritative and
  mapped to slices 2A/2B, with rev 1's eleven drafts demoted to
  refinements. The painter-extraction criterion now pins cells, the
  returned cursor, the focused window's `view_top` mutation, and
  passive-window state.

All four scout obligations are closed (§5), and the pixel formula is
treated as contract work, not implementation detail:

- The shared/terminal-only validator boundary is named exactly.
- Four new outbox tail-coalescing tags beside the existing four.
- **`State::mono_advance` is unsafe to adopt**: absent a `FontFacts`
  probe it samples the document's first shaped glyph, which would make
  panel columns document-dependent. The declaration uses the existing
  stable normal-face `probe_mono_advance` instead, and declares zero
  usable geometry when it returns `None`.
- `BASE_DIVIDER_HEIGHT` does not exist. Rev 2 decides its scaling and
  requires **one** document-bottom accessor routing every consumer
  (caret, hits, minimap, terminal geometry, clipping, edge scrolling)
  — a second unrouted seam is precisely the Stage 1 `Layout::compute`
  two-caller defect. The concrete base value is left open for round 2.

Also: the coherence statement now names journey steps 7-10 instead of
claiming none, and drops rev 1's overclaim that this advances
background-work visibility — a panel gives output a placement but adds
no join key to COHERENCE §9's four disjoint activity planes.

The ledger's bottom-panel lane is updated from "no branch and no
framing yet" to the framing's real state, and carries an explicit
correction: that entry was itself the source of rev 1's census
mis-statement.

Factual corrections: `InitialTargetResult` is at `message.rs:1145`;
`primary_document_window` has four references and two production paths
(`daemon.rs:1639`, and `daemon.rs:2998` via `primary_document_buffer`,
which is census #22); fifteen PRs merged since the parent's last
re-scout, not eleven.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 19:13:44 -04:00
Levi Neuwirth c2eeb60dc7 docs: bottom-panel Stage 2 framing (revision 1)
The re-framing `docs/bottom-panel-framing.md` rev 4 §2 requires before
Stage 2 (the GPU panel band) is implemented. Re-scouted against
canonical `main` @ `5aa9044`, protocol v20.

It does not restate the parent's decisions; it records what the
re-scout found. Every source anchor Stage 2 inherits had moved, but
none of the parent's mechanical model was falsified. Two facts held
and are load-bearing: protocol is still v20, so Q#BP9 resolves to
**v21** with no reservation needed, and both byte pins
(`InstanceMessage::InitialTargetResult`,
`FrontendEvent::TerminalPointer`) are still their enums' final
variants.

Four findings:

- **Q#BP2S1, new and open.** Stage 1 landed a daemon-side geometry
  epoch allocator (`declare_frame_geometry`), but Q#BP15a specifies a
  frontend-owned epoch echoed by every `Present`. The landed allocator
  also dedups on value and uses `saturating_add`, which is neither
  wrapping nor the fail-closed the framing asks for. Three resolutions
  are stated with a recommendation.
- **The §1.3 census is essentially unrouted.** Stage 1 built the
  `primary_document_window` seam but it has one production caller;
  ~80 direct `.active` reads remain. This is Stage 2's bulk, not its
  tidy-up, and the stage plan sequences it first.
- **The statusline active read is three sites, not one.**
- **Four scout obligations are still open** and are named rather than
  papered over, including the GPU-side pixel formula inputs.

Also carries the staged plan, draft acceptance criteria, the coherence
impact per `COHERENCE.md` §20 (§14 is the section it serves), and four
questions for the user.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
2026-07-25 19:13:44 -04:00
Levi Neuwirth ccf29e3eb5
Merge pull request #157 from levineuwirth/crdt-undo-repro
test(buffer): capture the CRDT undo no-op-with-op case
2026-07-25 23:10:46 +00:00
Levi Neuwirth d27d24ffec
Merge pull request #172 from levineuwirth/docs-inline-math-landed
docs: record the inline-math slice (#158) as landed
2026-07-25 23:10:19 +00:00
Levi Neuwirth 04c5ad13e8 docs: record the terminal-config lane
Stage 1 of the terminal config/copy-mode arc is in review; Stage 2 is
not started. Records the four decisions forced by scouted ground truth,
the four bites against four different wrong implementations, the two
reusable test instruments, and the gate results.
2026-07-25 18:41:21 -04:00