diff --git a/COHERENCE.md b/COHERENCE.md index bd9ee02..758b3e2 100644 --- a/COHERENCE.md +++ b/COHERENCE.md @@ -1234,14 +1234,23 @@ Primitive-by-primitive against the list above: `compile.lua`'s own comment admits ("command/menu undo stays dispatchable"). `Buffer::set_generated_contents` (write + discard history + assert `read_only`, in one authorized call) now fixes this - for the terminal snapshot; `*compilation*` and listview panels have - not yet adopted it and remain emptiable. **A second half of the same + for the terminal snapshot; **four writer mechanisms have not yet adopted + it and remain emptiable** — listview panels; `compile.lua`'s + `ensure_slot`, which serves `*compilation*` **and** `*shell-command*`; + the independent `*search-results*` panel in + `builtin/commands/default.lua`; and dired buffers. All pair an erroring + intercept with `bypass_intercept` writes over a still-writable rope. + (`*workers*`, `*help*` and `*buffer-list*` are generated but do not use + this idiom.) **A second half of the same caveat, found in round 3: a rope write is only half of an edit.** The owner-authorized write must be fanned out to the windows showing the buffer and queued for replica mirrors, or the displaying window keeps a line index describing the previous contents and the next paint indexes the new rope with stale ranges. Adoption is therefore not a - one-line swap. + one-line swap — and the three appending buffers (`*compilation*`, + `*shell-command*`, `*search-results*`) need a streaming variant of the + primitive that does not exist yet. Listview and dired already write + whole-buffer replaces and are the cheap half. - **Diagnostics collection** ✓ — `DiagnosticStore` + signs + unified `error.next` source. - **Transient selector** ✓ — the minibuffer (though its `source` diff --git a/docs/active-work.md b/docs/active-work.md index d958fbe..6ee50fe 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -5,14 +5,18 @@ landed on `main`. Read it after `docs/agent-handoff.md`. Remove completed entries when their PR merges; do not let this become a second permanent backlog. -**Two lane headers below are stale on purpose**, pending the docs updates -their own lanes owe: multi-root LSP affinity **#161 has merged** (the -Lean 4 lane still says IN REVIEW; its continuation is PR #167) and GPU -terminal input **#166 has merged** (its lane still says IN REVIEW; PR -#168 records it). Trust the canonical-base line below over a lane header: -if a PR number appears in `git log --first-parent githubsucks/main`, it -has landed regardless of what its lane says. (The inline-math lane was -here too until #172 removed it — that is the update those two owe.) +**One lane below is retained past its merge, and says so at its own +head**: the PTY terminate diagnostic (#176), because no landed-doc PR +owns moving its facts to `docs/agent-handoff.md` yet, and rule 4 removes +a lane only *after* that move. Every other merged lane has been removed — +the Lean 4 and GPU-terminal-input headers this paragraph used to +disclaim are gone, as are the inline-math (#172), dired (#169), and +terminal config + copy mode lanes — the last of these was #180's work, +folded into #182 so two open PRs would stop re-conflicting in this file. + +**Trust the canonical-base line below over any lane header**: if a PR +number appears in `git log --first-parent githubsucks/main`, it has +landed regardless of what a lane says. ## Repository authority @@ -23,17 +27,22 @@ here too until #172 removed it — that is the update those two owe.) machine-local: `origin` may name this canonical URL, a release mirror, or something else, and therefore has no authority by name alone. - Canonical base at this snapshot: - `githubsucks/main` @ `74301d1` (the dired Stage 1 landed-doc refresh - #169 atop Lean 4 Stage 4a #179, bottom-panel - Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal - configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the - CRDT undo repro #157, the inline-math landed-doc refresh #172, the - bottom-panel landed-doc refresh #156, the inline-math slice #158, - dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2 - #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean 4 - Stage 1 #160, and the minimap blank-slab fix #159; protocol v20). The - previous snapshot named `d152120`; the recovery check below accepts it - or anything newer. + `githubsucks/main` @ `42025e4` (Lean 4 Stage 4b #181, atop the dired + Stage 1 landed docs #169 and the PTY-terminate diagnostic #176, + terminal copy mode #178, the GPU-terminal-input landed docs #168, Lean + 4 Stage 4a #179, bottom-panel Stage 2A #177, the bottom-panel Stage 2 + framing #175, terminal configuration Stage 1 #173, Lean 4 Stage 3b + #170, Stage 3a #167, the CRDT undo repro #157, the inline-math + landed-doc refresh #172, the bottom-panel landed-doc refresh #156, the + inline-math slice #158, dired Stage 1 #165, the GPU terminal input fix + #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163, + find-file #162, Lean 4 Stage 1 #160, and the minimap blank-slab fix + #159; protocol v20). The previous snapshot named `74301d1`, and **the + recovery floor advances with it**: the check below now requires + `42025e4` or newer, so a tree at `74301d1` no longer passes. That is + deliberate — the floor moves with the base, because a check that + accepts an older commit than the declared base passes on a tree the + rest of this file does not describe. **Lanes below that name an older base have not been re-based; derive their integration surface from `git diff ..main`.** - On the transfer source, `origin/main` named a release mirror at @@ -69,14 +78,21 @@ git worktree list git status --short --branch ``` -The `git log` command must expose `c93f9ee` — the base named above — or a +The `git log` command must expose `42025e4` — the base named above — or a newer intentional main. Keep this threshold and the canonical-base line in step: a recovery check that accepts an older commit than the base it declares canonical will pass on a tree the rest of this file does not describe. If it does not, stop and repair the remote/fetch configuration. -## PTY terminate diagnostic lane — IN REVIEW (PR #176) +## PTY terminate diagnostic lane — MERGED (PR #176) + +> **Lane retained deliberately, and it is the next one to close.** #176 +> merged into `main` @ `bf8878f` (2026-07-26); rule 4 below removes a +> merged lane, but only after its durable facts reach +> `docs/agent-handoff.md`. **That absorption is unowned** — no landed-doc +> PR exists for #176 — so removing the lane now would delete the record +> instead of moving it. Whoever opens that PR removes this section. - Portable branch: `githubsucks/pty-terminate-eperm`; worktree `../pmacs-math-slice`. **PR #176**, base `main`, based on `ccf29e3` @@ -307,8 +323,10 @@ If it does not, stop and repair the remote/fetch configuration. - Framing `docs/journey-stage1a-framing.md` **rev 8** (four review rounds, two correction revisions found during implementation, one from review round 1 of PR #182). - Branch `journey-stage1a-directory-open`, rebased onto `githubsucks/main` - @ `74301d1`. + Branch `journey-stage1a-directory-open`, based on `githubsucks/main` + @ `42025e4` (rebased onto `74301d1`, then integrated `42025e4` and the + landed-docs work below by merge — the branch is under review, so its + history is no longer rewritten). - Recovery: `git fetch githubsucks && git checkout journey-stage1a-directory-open`. Everything below is committed and pushed; nothing depends on a worktree or `/tmp`. @@ -356,11 +374,18 @@ If it does not, stop and repair the remote/fetch configuration. Every `#[cfg(feature = "crdt")]` test is therefore **not compiled** in CI, not merely skipped. - **Measured, `--list` under CI's exact flags versus the same flags plus - `crdt`: 3,024 vs 3,288 — 264 tests dark.** Per target: + `crdt`: 3,176 vs 3,449 — 273 tests dark.** Re-measured at `74301d1` + (2026-07-26; at `fe8b8ba` it read 3,170 vs 3,443, the same 273 dark — + #176 added six tests, none of them `crdt`-gated). **The number moves + with every merge and must be + re-measured, not quoted.** #168 reported 3,024 vs 3,288 — 264 dark, + 177 in the library — at `1b6a084`; #178 then added CRDT-only + generated-buffer coverage, and other lanes landed CRDT tests in + between. Per target: | dark | CI | full | target | |---:|---:|---:|---| - | 177 | 1,832 | 2,009 | **the library itself** (`src/lib.rs`) | + | 185 | 1,848 | 2,033 | **the library itself** (`src/lib.rs`) | | 21 | 15 | 36 | `m5_5_acceptance` | | 13 | 1 | 14 | `gpu_invocation_acceptance` | | 13 | 1 | 14 | `gpu_initial_target_acceptance` | @@ -372,15 +397,20 @@ If it does not, stop and repair the remote/fetch configuration. | 3 | 0 | 3 | `compile_mode_crdt_acceptance` | | 2 | 22 | 24 | `theme_faces_acceptance` | | 2 | 0 | 2 | `m11_5_semantic_acceptance` | + | 1 | 14 | 15 | `terminal_copy_mode_acceptance` | | 1 | 9 | 10 | `vterm_stage1_acceptance` | | 1 | 7 | 8 | `statusline_segments_acceptance` | | 1 | 10 | 11 | `gpu_font_acceptance` | | 1 | 0 | 1 | `auto_indent_crdt_acceptance` | | 1 | 0 | 1 | `m10_11_perf` | + The rows sum to 273; the table is the whole census, not its head. + - **The single worst line is the library.** `cargo test --lib --features crdt` - is a REQUIRED local gate in `CLAUDE.md`, and CI has never run it. 177 - library tests — the whole CRDT half — are developer-machine-only. + is a REQUIRED local gate in `CLAUDE.md`, and CI has never run it. 185 + library tests — the whole CRDT half — are developer-machine-only, and + that count grows with every merged branch that adds a `crdt`-gated + unit test. - **Ten suites run zero or one test in CI**, including `gpu_initial_target` (#148's entire acceptance, 1/14), `gpu_invocation` (#141's, 1/14), and `a37`, the Vterm Stage 3 real-daemon/real-PTY/real-wgpu path that #135 @@ -434,282 +464,39 @@ If it does not, stop and repair the remote/fetch configuration. - Mitigating fact, verified rather than assumed: #166's three unit pins are **not** `crdt`-gated and do run under CI's exact flags, including the controller-release pin whose only job is catching the plausible wrong fix. - -## Terminal config + copy mode arc — Stage 1 MERGED; Stage 2 IN REVIEW - -- Approved framing: `docs/terminal-config-and-copy-mode-framing.md` - **revision 4** (four review rounds), committed as the first commit of - Stage 1's branch. Two stages, two branches, two PRs; **no protocol - change**. -- **Stage 1 MERGED as #173** (`main` @ `cf54270`, 2026-07-26, one review - round, all twelve checks green). Branch `githubsucks/terminal-config` - and worktree `../pmacs-terminal-config` retained. Profiles, scrollback, - a per-terminal configurable escape key, and the `C-c t` opening - binding; no protocol change. Main was integrated **twice** during the - single review round (`ccf29e3`, then `c93f9ee` after the first merge - left the PR conflicting) — see the no-CI-while-conflicting fact below. -- **Stage 2 = `githubsucks/terminal-copy-mode`**, worktree - `../pmacs-terminal-copy-mode`, based on `githubsucks/main` @ - `cf54270`. Copy mode: `M-x terminal.copy-mode` / `C-c C-t`. -- **Stage 2 ships eight of nine criteria, and the missing one is named.** - Criterion 17 (a real semantic frontend proving neither daemon buffer - nor mirror mutates) is **not pinned**: the optimistic apply exists only - in `pmacs-gpu/src/main.rs`, and the headless `SemanticClient` every - other semantic test uses has no optimistic path, so a faithful test - must drive the real GPU binary — the `a37` foundation, which CI never - compiles, silently skips without the binary, and is load-sensitive. A - second test on that footing buys the appearance of coverage. Both - halves of the mechanism are pinned **ungated** instead: acceptance 16 - (the guard is armed — `dispatch_idle` false while the snapshot is - focused) and 16b (the daemon holds — `is_read_only()` is **true** at - the rope, so an op that did arrive is refused by `ensure_writable()`). - **Rounds 2-3 changed what 17 must show.** 16b asserted `false` through - round 1, documenting the hazard; round 2 closed it. So the eventual - real-GPU test must look for **mirror mutation plus daemon refusal — - divergence** — not the "mutates both sides, silently" the criterion - originally specified, which after the fix cannot happen and would pass - for the wrong reason. The wire-level half stays an explicit obligation - of the CI `crdt`-coverage lane. -- Load-bearing Stage 2 decisions: - - **The snapshot MATERIALIZES into an ordinary buffer**, so isearch, - motion, selection and the kill ring work with no new substrate, and - "keys must not reach the child" dissolves structurally — the - transport arm keys on `is_terminal(buffer_id)` and a snapshot is not - a terminal. **The dispatch-shadow count stays at six.** - - **One serializer, not two** (Q#TC7): `copy_retained` builds a - whole-range *selection* and hands it to `copy_selection_bytes`. - - **`prune` reacts to removal rather than causing it** — it filters on - `!registry.contains(buffer_id)`, so a child exiting does NOT remove - the terminal buffer. That is why `on_removed` is a sound teardown - hook, and why a finished command's output stays readable. -- **Five bites, five different wrong implementations.** Removing - `set_round_trip_input` fails acceptance 16 **in the default - configuration** (the whole reason that pin is ungated); a naive - independently-written serializer fails all four unit pins, with the - diffs naming each drift mode (broken soft wrap, untrimmed blanks, - trailing newline); making re-invoke create a fresh buffer fails 18; - dropping the kill-with-terminal teardown fails 18; removing the - intercept fails 16b. Each failed exactly one test. -- **Review round 1 — four findings, all real, and they rhyme in pairs.** - Two P1 implementation defects and two P2 vacuous pins, all four tracing - to one root: **a name is not an identity, and a context-free readout is - not a state observation.** - - *P1 — a foreign same-named buffer was adopted and clobbered.* Snapshot - writes use `bypass_intercept`, so found-by-name adoption overwrote a - user's buffer; the reviewer reproduced "do not clobber" becoming 23 - newlines. Fixed by dired's F7 rule: **ownership means "in our own - handle table"**, and a taken name yields a `<2>` variant. - - *P1 — snapshot identity was keyed by terminal NAME.* - `TerminalManager::open` uniquifies only the *derived* name, so an - explicit `name = "*same*"` lets two valid terminals share one; they - then shared a snapshot, `q` returned to the wrong terminal, and - killing either removed it. Now keyed by comparing buffer handles in an - array — `BufferIdLua` implements `__eq` but each wrapper is a distinct - table key, so **comparison works and hashing does not**. - - *P2 — the refresh pins were vacuous.* 19 compared a quiet terminal's - snapshot against itself and 18 counted buffers, so both passed with - `render_snapshot` replaced by a no-op. Now the test types a marker - into the `cat` child, requires it **absent** first, then refreshes. - - *P2 — the tail-follow pin could not observe view state.* - `manager.snapshot(buffer_id)` is context-free and always reads the - live screen, so it reported "at the tail" for a view forced to the - oldest retained row. Now read through `snapshot_for_view`'s - `at_bottom` and projected cells. -- **Four more bites, all discriminating.** Restoring adopt-by-name fails - 18a *and* 18b; restoring name-keyed identity fails 18b; making - `render_snapshot` a no-op fails **both** 18 and 19 (the vacuity, - demonstrated); and forcing the view off the tail fails 20. -- **Review round 2 — one P1, and its fix retires half a named deferral.** - **Undo emptied the "read-only" snapshot.** `render_snapshot` wrote with - `bypass_intercept`, leaving ordinary undo history, and **`Buffer::undo` - reaches the rope through `ensure_writable` without ever consulting the - intercept chain** — so `C-/` *or* `M-x buffer.undo` 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 where - undo runs. - - **Rebinding the undo chords would NOT have fixed it**, 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. - - Fixed with `Buffer::set_generated_contents` (Lua - `pmacs.buffer.set_generated_contents`): lift `read_only`, replace - skipping intercepts, **discard history**, re-assert `read_only`. This - ships the deferred lane's two halves *as one primitive* — a bare - `set_read_only` would let a caller lock a buffer it can no longer - refresh, which is exactly why that lane was deferred. Clearing history - also stops a periodically refreshed buffer accumulating rope clones - nothing can ever pop. - - New pins: **acc16c** drives the real M-x path - (`command.invoke_interactive`), the chord, and redo, and asserts the - owner's refresh still works; **acc16b** flipped from asserting - `is_read_only()` is *false* to *true*, because the property it - described is the one that was fixed; plus three `buffer.rs` unit tests. - - Bite: restoring the `delete`+`insert` render reproduces the report - exactly — `left: Some("")` against the full snapshot — failing acc16c - and acc16b. - - **Still open:** `*compilation*` and listview remain emptiable by - `M-x buffer.undo`; the primitive they need now exists and is proven, - so the remainder is adoption plus a streaming-friendly variant. -- **Review round 3 — one P1 and two P2s, all on the round-2 primitive.** - The lesson: **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 called `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 received the owner's write. The prior - `buf:delete`/`buf:insert` pair had done this fan-out for free. - Fixed by applying **one whole-buffer `Replace`**, returning its - `Edit`, and notifying from the binding. - - **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` has no `clear`, but needs none — it records only what - happens after construction, the property `CrdtState::from_bytes` - already uses to keep the seed insert out of undo. New - `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 carries a superseded-in-part box rather than - being silently rewritten. - - New pins: **acc16d** paints the window after a *shrinking* generated - write (the stale offsets then point past the end, which is the - reported crash rather than stale pixels); **acc16e** asserts the - refresh is queued for mirrors through the real copy-mode path - (`crdt`-gated, therefore dark in CI — 16d is the half that runs); - plus a CRDT `buffer.rs` 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:** the fan-out obligation makes `*compilation*`/listview - adoption more than a one-line swap — recorded in `COHERENCE.md` §14 - alongside the undo half. -- **Review round 4 — one P2, docs only, and it is the interesting kind.** - **A fix can invalidate a test that was never written.** Criterion 17's - *bite* still described the pre-round-2 world: remove - `set_round_trip_input` and the op "mutates both sides, silently, with - no divergence to notice". True while nothing set `read_only` from Lua; - false once `set_generated_contents` did. A real-GPU test written to - that spec would hunt for a daemon-side edit that can no longer occur - and pass for the wrong reason — the specification would have leaked - the round-2 regression back in, through a test not yet built. - - Restated around **unauthorized mirror mutation plus daemon refusal = - divergence**, in all four places that carried the old claim: the - criterion, 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. - - Why round-trip input is still load-bearing rather than redundant: a - daemon 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 sees. - - **Gate-run flake observed and scoped without overclaiming its cause.** - `cargo test --lib --features crdt` failed ~1 run in 5 on - `process::tests::setsid_escapee_is_not_reaped_and_teardown_reclaims_readers` - — `active_reader_probe` returning `None` at `process.rs:3179` - ("live runtime probe"). **Pre-existing and unrelated:** this branch - does not touch `src/process.rs` (last changed by the Darwin PTY - signal-name fix), and the test passed 10/10 standalone; the observed - failures were during parallel full-suite runs. That localizes the - trigger to suite load or interaction, but does **not** distinguish - parallelism from another full-suite effect — no serial full-suite bite - was run. The leading code-path explanation is the known `drain_until` - trap: draining for `Started` also ticks, and a tick can reap the leader - before the following `active_reader_probe`. That is an inference from - the failure site and control flow, not yet a falsified root cause. - It belongs to the CI `crdt`-coverage lane for discrimination. The two - round-2 CRDT failures had no captured test names; this flake is a - plausible candidate for them, but they remain **unattributed**. -- Load-bearing decisions, each forced by scouted ground truth: - - profiles are a **raw Lua table** — `ConfigValue` is four scalars with - no table kind, so they join `pmacs.lsp.config` / `pmacs.pair.sets`; - - the **two open-time settings resolve through the global chain**, - because they are read before the identity buffer exists; only - `terminal.escape-key` resolves per buffer; - - the escape cache lives on **`TerminalSession`** so its lifetime is - the terminal's. `value_epoch` alone is not a sufficient key: it does - not advance when focus moves between terminals with different - buffer-local values; - - repeating the escape sends **that chord**, not a hardcoded `0x03`. -- **Four bites, each against a different plausible wrong - implementation** — hardcoded ETX fails acc6/9; epoch-only cache key - fails acc7; single last-entry cache fails acc8's parse count; removing - the invalid-value fallback fails acc10. The first version of acc7 - passed against the epoch-only bite because it asserted only that - terminal A still worked; the discriminating assertion is that **each** - terminal honors its own chord and not the other's. -- Test instruments worth reusing: `cat -v` is the echo probe, because the - screen rejects C0 controls before they reach cells so a raw echoed - `Ctrl-X` is invisible; and the probe **counts occurrences** rather than - testing presence, because a single-character probe collides with the - child's own banner text. -- **Review round 1 (2026-07-25) — five findings, all real, all fixed.** - One blocker and two majors were the same failure in three places: a - claim asserted somewhere cheaper than where it lives. - - *Blocker — `COHERENCE.md` was stale in four places, not the three - reported.* Step 8 still read "no keybinding"; §11 still read "five - settings"; and §6's dispatch table still cited - `is_terminal_escape_chord`, **a symbol this PR deletes**. §25 makes - that update ride the PR. A PR that changes audited ground truth has - to re-grep the audit for its own symbols, not only for its topic. - - *Major — acceptance 5 was vacuous.* It asserted a registry - round-trip, so 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. **Asserting - a value was stored is not asserting anything reads it.** - - *Major — acceptance 8a asserted the session count, not the cache.* - An editor-side map with no purge hook — the exact rejected design — - leaks *while* sessions drain, so it passed. Fixed with a - `TerminalManager::escape_caches()` seam. **A lifecycle claim needs a - lifecycle observable.** - - *Moderate — `table.sort` over user-controlled profile keys.* A - table holding both a string and a numeric key raised `attempt to - compare number with string` **on the unknown-profile path**, - replacing the 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** — the error reporter was the - thing that failed. - - *Minor — the committed framing still said "not yet approved".* -- **Three new bites, each falsified by revert**: deleting the scrollback - consumer fails acc5 (and only acc5); restoring the raw-key sort - reproduces `attempt to compare string with number` verbatim; and - implementing the rejected editor-side map fails the new acc8a at - `left: 2, right: 1` **while passing the old session-count version** — - which is the review finding demonstrated rather than argued. -- Verification after the round-1 fixes, on the tree merged with - `githubsucks/main` @ `c93f9ee`: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,832 default + 2,009 CRDT library tests; - `terminal_config_acceptance` **12/12 in both configurations**; vterm - Stage 1/2 9+10 / 6+6; config registry 16+16; bottom-panel Stage 1 - 46+46; M4 121; required GPU 202; `git diff --check` clean. - - `compile_mode_acceptance` fails 11/67 against the **real** user - config and passes 67/67 with an isolated `XDG_CONFIG_HOME` — the - known pre-existing trap, not this branch. - - **`vterm_stage3_acceptance::a37` fails on this machine — and fails - identically on the PR's own base `d152120`**, so it is not this - branch's regression. It is load-sensitive: it passed at `d152120` - once and failed at that same commit twenty minutes later, with a - second agent saturating the machine with `rustc` in between. Two - ways it lies, both worth knowing: it **silently returns `ok` when - `pmacs-gpu` is not built** in the same target dir (only - `PMACS_REQUIRE_GPU=1` promotes that skip to a failure, and the gate - list applies that flag to `-p pmacs-gpu`, a *different* package), and - it is **crdt-gated, so CI has never run it at all**. A green a37 in - a gate log means nothing unless the binary was built and the flag - was set. Needs its own lane; see the CI `crdt`-coverage lane on #168. - - `pmacs-gpu` itself failed 201/202 once under the same load and passed - 202/202 on immediate rerun. +- **This lane also owns a `--lib --features crdt` flake, observed and + scoped without overclaiming its cause** (inherited from #178's gating, + where the terminal lane recorded it). `cargo test --lib --features + crdt` failed ~1 run in 5 on + `process::tests::setsid_escapee_is_not_reaped_and_teardown_reclaims_readers` + — `active_reader_probe` returning `None` at `process.rs:3179` ("live + runtime probe"). **Pre-existing and unrelated to #178:** that branch + did not touch `src/process.rs` at all, and the test passed 10/10 + standalone; the observed + failures were during parallel full-suite runs. That localizes the + trigger to suite load or interaction, but does **not** distinguish + parallelism from another full-suite effect — no serial full-suite bite + was run. The leading code-path explanation is the known `drain_until` + trap: draining for `Started` also ticks, and a tick can reap the leader + before the following `active_reader_probe`. That is an inference from + the failure site and control flow, not yet a falsified root cause. + Discriminating it belongs here. Two unnamed CRDT failures in #178's + round-2 gating are a plausible match but remain **unattributed** — no + test names were captured. +- **A second standing obstacle for this lane:** `cargo clippy --workspace + --all-targets --features crdt -- -D warnings` **fails on `main`** — + measured at `74301d1`: seven errors before the build aborts, four in + `src/daemon.rs` (`useless_conversion` at 3996, missing doc backticks at + 4076, `too_many_lines` 112/100 at 4083, an unneeded `mut` at 4965) and + three in `tests/vterm_stage3_acceptance.rs` (`too_many_lines` at 637 + and 793, a redundant `continue` at 843). **Treat that as a lower + bound, not an inventory:** Clippy abandons the remaining targets once + one fails, and a run on an older tree surfaced a further doc-backticks + error in `tests/auto_indent_crdt_acceptance.rs:42` that this run never + reached. The + standing gate list runs Clippy without `crdt`, so these lints have + never been enforced. Any CI job that compiles the `crdt` targets has to + fix them first or it will be red on arrival. ## Bottom-panel lane (Arc 7) — Stages 1, 2A + framing MERGED; 2B is next @@ -897,6 +684,24 @@ git worktree add --track \ ## Closed since the last snapshot +- **Terminal configuration + copy mode arc — BOTH STAGES MERGED, lane + removed.** Stage 1 **#173** (`main` @ `cf54270`, one review round) and + Stage 2 **#178** (`main` @ `fe8b8ba`, **four review rounds**, twelve + checks green on head `1b44c69` — verified by `head_sha`, not by the + check summary), both 2026-07-26, both with no protocol change. + Approved framing: `docs/terminal-config-and-copy-mode-framing.md` rev + 4, committed as the first commit of Stage 1's branch; its Q#TC6a + carries a superseded-in-part box rather than a silent rewrite. Durable + facts moved to `docs/agent-handoff.md` §1 (the arc bullet) and §4 (the + `set_generated_contents` invariant) per rule 3 below, and to + `COHERENCE.md` §14. **Stage 2 ships eight of nine criteria and the + missing one is named** — criterion 17 needs a real GPU frontend, so it + waits on the `a37` footing; the handoff records what it must assert. + Branches `githubsucks/terminal-config` and + `githubsucks/terminal-copy-mode` with worktrees + `../pmacs-terminal-config` and `../pmacs-terminal-copy-mode` are + retained. The gate-run flake found while gating #178 moved to the CI + `crdt`-coverage lane above, which owns its discrimination. - **Dired Stage 1 (the directory view) — MERGED as #165** (`main` @ `c8ec8f3`, 2026-07-25, after one review round). pmacs has a directory surface: `C-x d` / `C-x C-j`, one read-only buffer per directory named @@ -946,6 +751,15 @@ git worktree add --track \ reproduces in-process and so is not the GUI/TUI asymmetry; and a geometry change appearing to clear the visible screen, which reproduces pre-fix). Branch `gpu-terminal-input` and worktree `../pmacs-gui-term-input` retained. + **Its landed-doc pair MERGED as #168** (`main` @ `1b6a084`, + 2026-07-26): #166 recorded as landed, the CI `crdt`-coverage gap + measured (**264 tests dark workspace-wide**, 177 in the library — a + reading taken at `1b6a084` and kept here only as history. **The CI + `crdt`-coverage lane above is the authority for the live figure**; + do not quote this one forward), the + vterm audit corrected — "only 3 of 9 acceptances drive a real daemon" + was optimistic; without the frontend binary the honest number is + **2** — and the a37 findings folded into the coverage lane. - **Inline-math slice — MERGED as #158** (`main` @ `5aa9044`, 2026-07-25). Detect → parse → layout → draw for `$…$`, entirely inside `pmacs-gpu`, no protocol change. Verified by the user's manual pass on diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index 6ebe867..6607df6 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,9 +1,13 @@ # Agent handoff — cross-machine continuity -**Last updated: 2026-07-26, after Lean 4 Stage 4a (#179) — the typed-edit +**Last updated: 2026-07-26, after terminal copy mode (#178) — `C-c C-t` +materializes a terminal's whole retained range into an ordinary buffer, +plus `Buffer::set_generated_contents`, the first genuinely immutable +generated-buffer write path — and its landed-doc pair (#168); following +Lean 4 Stage 4a (#179) — the typed-edit consumer chain — and bottom-panel Stage 2A (#177), the classified census routing that makes every Projection-class consumer ask -`primary_document_window`; following the bottom-panel Stage 2 framing +`primary_document_window`; the bottom-panel Stage 2 framing (#175), terminal configuration Stage 1 (#173) — profiles, scrollback, a per-terminal configurable escape key, and the `C-c t` opening binding — Lean 4 stages 3a and 3b (#167, #170), pmacs' first Lean language server; @@ -37,8 +41,10 @@ commands, read `docs/active-work.md` immediately after this file. ## 1. Where the project stands (2026-07-26) -- `main` @ `74301d1` (the dired Stage 1 landed-doc refresh #169 atop - Lean 4 Stage 4a #179, bottom-panel Stage 2A +- `main` @ `42025e4` (Lean 4 Stage 4b #181, atop the dired Stage 1 + landed docs #169 and the PTY-terminate diagnostic #176, terminal copy + mode #178, the GPU-terminal-input landed docs #168, Lean 4 Stage 4a + #179, bottom-panel Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the CRDT undo repro #157, the inline-math landed-doc refresh #172, the bottom-panel @@ -100,9 +106,55 @@ commands, read `docs/active-work.md` immediately after this file. corrected here; changing the lifetime is separate work. - Stage 1b is the named remainder: compile binding + Cargo defaults, LSP spawn guidance, welcome buffer. -- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED** - (`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge - `d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a +- **Terminal configuration + copy mode arc — COMPLETE** + (`docs/terminal-config-and-copy-mode-framing.md` rev 4; Stage 1 #173, + Stage 2 #178; no protocol change in either, still v20). Stage 1 ships + profiles, scrollback, a per-terminal configurable escape key and the + `C-c t` opener; Stage 2 ships copy mode — `M-x terminal.copy-mode` / + `C-c C-t`. + - **The snapshot MATERIALIZES into an ordinary buffer.** That is the + arc's organizing decision: isearch, motion, selection and the kill + ring work with no new substrate, and "keys must not reach the child" + dissolves structurally, because the transport arm keys on + `is_terminal(buffer_id)` and a snapshot is not a terminal. **The + dispatch-shadow count therefore stays at six.** + - **`prune` reacts to buffer removal rather than causing it** — it + filters on `!registry.contains(buffer_id)`, so a child exiting does + **not** remove the terminal buffer. That is what makes `on_removed` a + sound teardown hook, and why a finished command's output stays + readable. + - **Ownership means "in our own handle table", never found-by-name** + (dired's F7 rule, re-learned here): snapshot writes use + `bypass_intercept`, so adopting a same-named foreign buffer clobbers + user data. Snapshot identity is keyed by **comparing buffer handles + in an array** — `BufferIdLua` implements `__eq` but each wrapper is a + distinct table key, so comparison works and hashing does not. + - **Profiles are a raw Lua table**, joining `pmacs.lsp.config` and + `pmacs.pair.sets`, because `ConfigValue` is four scalars with no + table kind. The two open-time settings resolve through the **global** + chain (they are read before the identity buffer exists); only + `terminal.escape-key` resolves per buffer, and its cache lives on + **`TerminalSession`** so its lifetime is the terminal's — + `value_epoch` alone is not a sufficient key, because it does not + advance when focus moves between terminals holding different + buffer-local values. + - **Criterion 17 is deliberately unpinned, and its bite is now stated + correctly.** A real semantic frontend proving neither copy is mutated + needs the actual GPU binary (the optimistic apply exists only in + `pmacs-gpu/src/main.rs`; the headless `SemanticClient` has no + optimistic path), i.e. the `a37` footing §5 warns about. After + `set_generated_contents` the eventual test must look for + **unauthorized mirror mutation plus daemon refusal — divergence**, + not the "mutates both sides silently" the criterion originally + specified, which can no longer happen and would pass for the wrong + reason. *A fix can invalidate a test that was never written.* + - Test instruments worth reusing: **`cat -v` is the echo probe**, + because the screen rejects C0 controls before they reach cells so a + raw echoed `Ctrl-X` is invisible; and such probes must **count + occurrences rather than test presence**, because a single-character + probe collides with the child's own banner text. +- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b, 4a, 4b ALL LANDED** + (`docs/lean4-mode-framing.md`; #160, #161, #167, #170, #179, #181). pmacs edits Lean 4: `arborium-lean` highlighting, a `lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language server with a Lake-aware outermost root, a lazy toolchain probe, a one-shot `lean --server` fallback, and `waitForDiagnostics`. **No @@ -145,8 +197,9 @@ commands, read `docs/active-work.md` immediately after this file. config swap invalidates. The durable lesson is to heal at **consumption** — the point where a stale record is handed out — not at the moment of the swap. - - **Stage 4a (typed-edit consumer chain) MERGED as #179** (`main` @ - `a27f646`, two review rounds). It is substrate only: + - **Stage 4a (the typed-edit consumer chain) MERGED as #179** + (branch `lean4-stage4a-typed-edit-chain`, framing rev 8; it is part + of the main anchor above). It is substrate only: `builtin/runtime/typed_edit.lua` owns the single `buffer.after-edit` subscriber and the single one-shot read, `pair.lua` becomes its first registered consumer, and @@ -171,8 +224,8 @@ commands, read `docs/active-work.md` immediately after this file. reason had been copied into a module comment, an acceptance criterion, a test comment, and the ledger. **Correct the source a rationale derives from, not only the sites that quote it.** - - **Stage 4b (the Unicode input method) is implemented and in review** - (branch `lean4-stage4b-input-method`, framing rev 9): a vendored + - **Stage 4b (the Unicode input method) MERGED as #181** + (framing rev 9): a vendored 1,855-entry table generated from `leanprover/vscode-lean4@17d1d08` by `scripts/regen-lean-abbrev`, plus a consumer registered on the Stage 4a chain at priority 50, ahead of pairing. **A consumer @@ -1036,6 +1089,72 @@ before trusting them: ## 4. Substrate invariants (do not undo; tests enforce most of these) +**Generated buffers: `Buffer::set_generated_contents` is the ONE +authorized write** (terminal copy mode #178) — lift `read_only`, replace +via a single whole-buffer `Replace` skipping intercepts, discard history, +re-assert `read_only`, and **return the `Edit`**. Three things make it a +unit rather than a convenience: + +- **An intercept is not read-only.** `Buffer::undo` reaches the rope + through `ensure_writable` and never consults the intercept chain, so an + intercept-only "read-only" buffer is emptied by `M-x buffer.undo`. + Rebinding the undo *chords* buffer-locally does **not** close it — + `compile.lua`'s own comment says so ("command/menu undo stays + dispatchable"). Only rope-level `read_only` does. +- **A bare `set_read_only` would be worse than nothing**, because it also + refuses the owner's refresh — the operation such buffers exist for. + That is why the pairing, not the setter, is the primitive. There is + deliberately no Lua `set_read_only`. +- **A rope write is only half of an edit.** The returned `Edit` must be + fanned out (`notify_buffer_edit_to_windows`, which also queues the + daemon-origin CRDT op). Skip it and a displaying window keeps a + `TextView` line index describing the previous contents — the next paint + indexes the new rope with stale ranges and trips + `assertion failed: end <= self.len()` — while replica mirrors never + import the write at all. + +History clearing is load-bearing twice (nothing can pop entries +`read_only` makes unreachable, so they leak), and must clear **whichever +history the buffer has**: the v0.1 stacks are bypassed in CRDT mode, where +it lives in loro's `UndoManager`. That has no `clear`, and needs none — a +manager records only what happens after construction, so +`CrdtState::clear_undo_history` rebinds a fresh one to the same doc. + +**Not yet adopted — the inventory is four writer mechanisms covering +five buffers.** *Every remaining intercept-protected writer* uses the +older idiom: an erroring intercept plus `set_round_trip_input`, written +through `bypass_intercept`, with the rope left writable. All are +emptiable by `M-x buffer.undo`: + +| writer | buffers | shape | +|---|---|---| +| `builtin/runtime/listview.lua:60-61` | every listview panel | delete-all + insert | +| `builtin/runtime/compile.lua` (`ensure_slot`) | `*compilation*`, `*shell-command*` | **append** per output batch | +| `builtin/commands/default.lua:869` | `*search-results*` | reset per query, then **append** per match batch | +| `builtin/runtime/dired.lua:371` | every dired buffer | whole-buffer replace | + +**Do not read `ensure_slot` as covering the search panel** — it serves +`*compilation*` and `*shell-command*` only (`compile.lua:1090,1125`). +`*search-results*` is an independent panel with its own intercept, +round-trip mark and writes, and `compile.lua` names it only in a +predicate. Nor is the scope "every generated buffer": `*workers*`, +`*help*` and `*buffer-list*` are generated too but do not use this +idiom, and the REPL package's intercept +(`builtin/packages/repl/init.lua:187`) is an op-filtering editing +policy, not a read-only panel — neither group belongs to this lane. + +Adoption is not a one-line swap. It inherits the fan-out obligation, and +the three appending buffers need a **streaming variant** of the +primitive; listview and dired already write whole-buffer replaces and +are the cheap half. Recorded in `COHERENCE.md` §14. + +**And it does not replace `set_round_trip_input`.** The protection is +layered across two copies: rope-level `read_only` refuses the op at the +daemon; round-trip input stops a semantic frontend applying +optimistically to its **own mirror**, which a daemon-side refusal cannot +reach — the refusal arrives after the frontend has already painted, so it +buys divergence, not prevention. + **Command boundaries (Arc 2 kill-ring substrate)** — `EditorCore.command_history: HashMap`, per frontend. Rotate on: keybound command, self-insert, menu invoke, diff --git a/docs/terminal-config-and-copy-mode-framing.md b/docs/terminal-config-and-copy-mode-framing.md index 15878cf..bd405ea 100644 --- a/docs/terminal-config-and-copy-mode-framing.md +++ b/docs/terminal-config-and-copy-mode-framing.md @@ -564,11 +564,21 @@ additive, on its own binding, and does not replace scroll-and-select. would replay, and it stops a periodically refreshed buffer accumulating rope clones that `read_only` guarantees nothing can ever pop. - **What remains of the lane:** `*compilation*` and listview panels still - rely on intercept-plus-round-trip and are still emptiable by - `M-x buffer.undo`. The primitive they need now exists and is proven, so - the remaining work is adoption plus a streaming-friendly variant - (`*compilation*` appends rather than replacing wholesale). + **What remains of the lane — four writer mechanisms over five + buffers**, not the two this section first named (round 5 found the + inventory short; round 6 found the corrected version misattributing + the search panel). Every remaining intercept-protected writer still + relies on intercept-plus-round-trip over a writable rope, and every one + is still emptiable by `M-x buffer.undo`: listview panels + (`listview.lua:60-61`); `compile.lua`'s `ensure_slot`, which serves + `*compilation*` and `*shell-command*` — **not** `*search-results*`, + which `compile.lua` names only in a predicate; the independent + `*search-results*` panel in `builtin/commands/default.lua:869`, with + its own intercept and writes; and dired buffers (`dired.lua:371`). The + primitive they need now exists and is proven, so the remaining work is + adoption plus a streaming-friendly variant — the three appending + buffers need it, while listview and dired already write whole-buffer + replaces and are the cheap half. **The CRDT half is closed too** (review round 3). Clearing the v0.1 stacks proves nothing in CRDT mode, where they are bypassed entirely and