Commit Graph

194 Commits

Author SHA1 Message Date
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 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 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 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
Levi Neuwirth b123c0b9fe Merge branch 'main' into docs-dired-stage1-landed
Three conflicts, resolved by taking the newer statement on each side
rather than either side wholesale:

- COHERENCE.md journey row 7 keeps this branch's text (dired #165 is
  merged, not a PR); row 8 takes main's, which records terminal config
  #173.
- The ledger's canonical-base line takes main's d400f30 anchor and keeps
  this branch's caveat about lanes that name an older base.
- agent-handoff's two anchors take main's d400f30 wording, with the CRDT
  undo repro #157 and the inline-math landed-doc refresh #172 added
  back — both are merged and main's summary had dropped them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
2026-07-26 14:40:13 -04:00
Levi Neuwirth 23c966cc31 docs(terminal): restate criterion 17's bite for the fixed substrate
Review round 4, P2. A fix can invalidate a test that was never written.

Criterion 17 still specified the pre-round-2 world: remove
`set_round_trip_input` and the optimistic op "passes `ensure_writable()`
and mutates BOTH sides, silently, with no divergence to notice". That
was true while no Lua binding set `read_only`. Since
`set_generated_contents` does, the daemon refuses the op — so only the
frontend's own mirror mutates, and the copies diverge.

The gap matters precisely because 17 is unpinned. A real-GPU test
written to the old spec would hunt for a daemon-side edit that can no
longer occur and pass for the wrong reason, quietly readmitting the
round-2 regression through a test not yet built. The specification is
the artifact under review here, not the code.

Restated around unauthorized MIRROR mutation plus daemon refusal —
divergence — in all four places carrying the obsolete claim: the
criterion itself, the Q#TC6a heading, the acceptance-16 doc comment, and
the bite roster. The heading's "ONLY thing" now says what it is the only
thing FOR: the replica's own mirror. `docs/active-work.md` also still
described acceptance 16b as asserting `is_read_only()` is false, which
round 2 flipped.

Why round-trip input stays load-bearing rather than redundant, now
stated wherever the daemon guard is mentioned: a refusal arrives after
the frontend has already applied optimistically and painted. It buys
divergence instead of silent agreement; it does not prevent the mutation
the user is looking at.

Also recorded, after capturing it properly this time: the gate-run flake
in `cargo test --lib --features crdt` is
`process::tests::setsid_escapee_is_not_reaped_and_teardown_reclaims_readers`
(`active_reader_probe` -> None, "live runtime probe"), ~1 run in 5.
Pre-existing and unrelated — this branch does not touch
`src/process.rs`, the test passes 10/10 standalone and 2017/2017 at
`--test-threads=1`, and it is another instance of the known `drain_until`
trap: draining for `Started` also ticks, and a tick reaps the leader.
That also explains the unattributed "2 failed" run noted in round 2.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-26 14:38:22 -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 a0fb01f24c fix(buffer): fan out generated writes, and clear the history that exists
Review round 3, on the round-2 primitive itself. One lesson covers all
three findings: a rope write is only half of an edit, and "discard
history" means whichever history the buffer actually has.

P1 — the binding swallowed the edit. `set_generated_contents` returned
`()`, so nothing reached `notify_buffer_edit_to_windows`. Two
consequences, both reproduced by the reviewer. In the default build a
window showing the buffer kept a `TextView` line index describing the
PREVIOUS contents, and the next paint indexed the new rope with stale
ranges — `assertion failed: end <= self.len()` in `src/rope.rs`. In the
CRDT build `pending_crdt_ops` stayed empty, so replica mirrors never
imported the owner's write and their optimistic edits were generated
against content already replaced. The `delete`+`insert` pair this
replaced had done that fan-out for free.

Now applies ONE whole-buffer `Replace`, returns its `Edit`, and notifies
from the binding. The doc comment states the obligation, because the
next owner to adopt the primitive inherits it.

P2 — "discard history" was false in CRDT mode. The v0.1 stacks are
bypassed entirely there; the history lives in loro's `UndoManager`.
`read_only` stops the replay but not the retention, which is the memory
cost the contract claims to eliminate. `UndoManager` exposes no clear,
but needs none: it records only what happens after it is constructed,
the same property `CrdtState::from_bytes` already uses to keep the seed
insert out of undo. `CrdtState::clear_undo_history` rebinds a fresh
manager to the same doc.

P2 — the docs described the pre-fix architecture. Q#TC6a said no Lua
binding sets `read_only` and round-trip input is the only guard; the
acceptance text still said `is_read_only() == false` while 16b had been
flipped to true; `terminal.lua`'s comment repeated the obsolete claim.
The architecture is layered and now says so: rope-level read-only
protects the daemon copy, round-trip input protects the replica's
optimistic mirror, and neither substitutes for the other. Q#TC6a keeps
its analysis under a superseded-in-part box rather than being silently
rewritten — its conclusion survives, two of its premises do not.

New pins. acc16d paints the window after a SHRINKING generated write:
stale offsets then point past the buffer end, so the failure is the
reported crash rather than merely stale pixels. acc16e asserts the
refresh is queued for mirrors, through the real copy-mode path;
`crdt`-gated and therefore dark in CI, which is why 16d drives the
binding rather than the terminal. Plus a CRDT unit test that ten renders
leave the `UndoManager` with nothing recorded.

Bites: dropping the notify panics acc16d at `rope.rs:145` and fails
acc16e with `queued: []`; dropping the `UndoManager` rebind fails the
new unit test on `can_undo`.

Still open, and recorded in COHERENCE.md §14: the fan-out obligation
makes `*compilation*`/listview adoption more than a one-line swap.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-26 13:43:22 -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 8c5b39ef32 fix(buffer): make generated buffers survive undo
Review round 2, P1. Undo could empty the "read-only" snapshot.

`render_snapshot` wrote with bypass_intercept, which leaves ordinary
undo history behind, and `Buffer::undo` reaches the rope through
`ensure_writable` without ever consulting the intercept chain. So a
single `C-/` — or `M-x buffer.undo`, which needs no keymap at all —
replaced a freshly rendered snapshot with an empty buffer.
`set_round_trip_input` does not help: it routes the key into the daemon
command path, which is exactly where undo runs.

Rebinding the undo chords buffer-locally would not have closed this,
and `compile.lua` already says so in a comment: "command/menu undo
stays dispatchable". `*compilation*` and listview panels therefore
carry the same latent defect today.

Adds `Buffer::set_generated_contents` (Lua:
`pmacs.buffer.set_generated_contents`): lift `read_only`, replace the
contents skipping intercepts, discard the resulting history, re-assert
`read_only`. This ships the framing's deferred immutability lane as ONE
primitive rather than exposing the setter — a bare `set_read_only`
would let a caller lock a buffer it can no longer refresh, which is
precisely why that lane was deferred. Discarding history is
load-bearing twice: it removes what undo would replay, and it stops a
periodically refreshed buffer accumulating rope clones that `read_only`
guarantees nothing can ever pop.

New acceptance 16c drives the real M-x path
(`command.invoke_interactive`), the chord, and redo, and asserts the
owner's own refresh still works — the operation plain `read_only` would
have broken. Acceptance 16b flips from asserting `is_read_only()` is
false to true, because the property it documented is the one that was
wrong. Three `buffer.rs` unit tests cover the primitive directly,
including that ten refreshes leave an empty undo stack.

Bite: restoring the delete+insert render reproduces the report exactly
— `left: Some("")` against the full snapshot — failing 16c and 16b.

Still open, and now named in the framing, COHERENCE.md §14 and the
ledger: `*compilation*` and listview have not adopted the primitive and
remain emptiable by `M-x buffer.undo`; a streaming-friendly variant is
needed for the append case. In CRDT mode `read_only` is what refuses
undo, since loro's UndoManager exposes no clear through `CrdtState`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
2026-07-26 13:12:08 -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 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 b9fbb42dc0 Merge remote-tracking branch 'githubsucks/main' into terminal-copy-mode 2026-07-26 10:45:32 -04:00