From 44f5e44b9fce3cb4654e8f95249e8fd39e4371c8 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 15:48:03 -0400 Subject: [PATCH] docs: record #168 and #178 as landed, and the generated-buffer invariant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer --- docs/active-work.md | 20 ++++++++++++---- docs/agent-handoff.md | 55 ++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 68 insertions(+), 7 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 7df3466..0c234ee 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -468,7 +468,7 @@ If it does not, stop and repair the remote/fetch configuration. **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 +## Terminal config + copy mode arc — BOTH STAGES MERGED (arc complete) - Approved framing: `docs/terminal-config-and-copy-mode-framing.md` **revision 4** (four review rounds), committed as the first commit of @@ -481,9 +481,15 @@ If it does not, stop and repair the remote/fetch configuration. 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 MERGED as #178** (`main` @ `fe8b8ba`, 2026-07-26, **four + review rounds**, twelve checks green on head `1b44c69` — verified by + `head_sha`, not by the check summary). Copy mode: + `M-x terminal.copy-mode` / `C-c C-t`. Branch + `githubsucks/terminal-copy-mode` and worktree + `../pmacs-terminal-copy-mode` retained. Main was integrated once, after + #168 landed; the `docs/active-work.md` terminal-lane conflict resolved + by taking main's fuller Stage 1 sentence under this lane's Stage 2 + record. - **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 @@ -947,6 +953,12 @@ 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), 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 45ee353..7d1b326 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,7 +41,8 @@ commands, read `docs/active-work.md` immediately after this file. ## 1. Where the project stands (2026-07-26) -- `main` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel Stage 2A +- `main` @ `fe8b8ba` (terminal copy mode #178 atop 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 @@ -884,6 +889,50 @@ 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:** `*compilation*` and listview panels still rely on +intercept-plus-`set_round_trip_input` and remain emptiable by +`M-x buffer.undo`. Adoption is not a one-line swap — it inherits the +fan-out obligation, and `*compilation*` appends rather than replacing, so +it needs a streaming variant. 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,