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
This commit is contained in:
parent
fe8b8ba4c6
commit
44f5e44b9f
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<FrontendId, CommandBoundary{this, last}>`,
|
||||
per frontend. Rotate on: keybound command, self-insert, menu invoke,
|
||||
|
|
|
|||
Loading…
Reference in New Issue