docs: dired Stage 2 framing rev 8 — round 7, five contract defects

All seven citations re-verified against the tree; all seven hold, one is
understated. The split with #186 is untouched.

Revision 7's process read every mechanism it CITED but never read the
mechanisms it RELIED ON: it verified that tick exists and returns
settled ids without reading that the drain is a bare try_recv with no
execution token, and it verified that kill_buffer exists without reading
the order in which it mutates before it can refuse. Reading a symbol to
confirm it is there is not the same as reading it to confirm it does
what the surrounding argument needs.

F1 — reply order is not execution order. AsyncRuntime::tick
(src/async_runtime.rs:1003) drains the reply bus with no execution
token, so a worker can finish, be descheduled before sending, and have a
later reply arrive first. Asked the cheaper question first as directed:
reconciliation does NOT need to be order-dependent. Independent
mutations commute; interdependent ones cannot arise from any production
path (dired serializes, apply_resource_op is synchronous, the fs
primitives have zero production callers); and fs.lua:155-165 already
instructs callers needing ordering to serialize. So the guarantee is
withdrawn rather than engineered. A token under a mutation lock was
rejected: it serializes every fs mutation to close a hazard with no
production reachability and a documented caller-side remedy. No static
ordering rule is offered because none works — worked through in §6.

F2 — preflight, and the review understates it. kill_buffer clears
round_trip_buffers, closes side windows and redirects ordinary windows
before BufferRegistry::remove can refuse. Rev 7 said to treat the
refusal as "keep the buffer", which reads as though skipping phase 2
restored something; it does not. reconcile_delete now preflights
editing_in_progress — sound because phase 1 is pure EditorCore with no
Lua handle, so nothing can re-enter between check and removal.
Acceptance 53b is three separately-asserted properties, each with its
own named bite.

F3 — path-equivalence, not string equality. Names come from
path.display() as given while only file_path is normalized, so a
relative open leaves a short name a string rule mistakes for
user-chosen. Tested both directions; the custom-name arm is what stops
the fix becoming a name-clobberer.

F4 — bounded tombstone, and the census corrected this revision's own
first answer. A first pass checked only handle_notification and
concluded publishDiagnostics was the only uncorrelated writer. Wrong
lens boundary: mark_document_stale takes no LspServerId and creates URI
keys across three stores for every server. The full census also found
that diag_store has zero correlated writers and that
DiagnosticStore.by_uri is keyed by URI alone with no server component —
so the store most needing protection is the one a route purge cannot
help, and a (sid, uri) tombstone would not match it. Recorded as the
round's own defect class occurring inside the round.

F5 — three outcomes, because pmacs.minibuffer.read already has three.
Cancel does not fall through to on_no: for C, declining means copy the
non-colliding entries while cancelling means abandon, and conflating
them would make C-g perform a partial copy.

Sweep for the same defect class: three candidates, two cleared by
reading (run_all_must_succeed really does collect and not abort;
commit_to_refuses_an_await_and_restores really exists), one real and not
raised by review — the framing never said which HookKind the new hooks
register with, and short-circuit would let one subscriber silently stop
every later one reconciling. Both are now all-must-succeed.

P2: pmacs.lsp.forget_uri named with an error contract and pinned; the
ledger note rewritten — it claimed single-file scope while that same
revision edited the ledger — with both line counts measured at this tree
rather than quoted.

Status unchanged: PROPOSED, needs explicit user approval. No runtime
code. Do not merge.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
This commit is contained in:
Levi Neuwirth 2026-07-28 20:30:29 -04:00
parent fb26fb15ae
commit 7ecea94693
2 changed files with 836 additions and 64 deletions

View File

@ -459,18 +459,63 @@ has **no branch and no framing yet**.
`FrontendView.fold_projection` to `true` for semantic frontends, which `FrontendView.fold_projection` to `true` for semantic frontends, which
Stage 2 deliberately left `false` (Q#FD21). Stage 2 deliberately left `false` (Q#FD21).
## dired Stage 2 framing lane — PR #171 AT REVISION 7, AWAITING APPROVAL ## dired Stage 2 framing lane — PR #171 AT REVISION 8, AWAITING APPROVAL
- Portable branch: `githubsucks/dired-stage2-framing`; - Portable branch: `githubsucks/dired-stage2-framing`;
worktree `../pmacs-dired-stage1`. **PR #171**, base `main`, integrated worktree `../pmacs-dired-stage1`. **PR #171**, base `main`, integrated
up to `main` @ `ad41cf1`. Framing only — up to `main` @ `ad41cf1`. Framing only —
`docs/dired-stage2-framing.md`, now **~2,630 lines**, no runtime code. `docs/dired-stage2-framing.md`, **3,624 lines measured at this
This lane rides that PR. revision**, no runtime code. This lane rides that PR — it has since
rev 6, when #185 merged; do not open a standalone ledger PR.
- **Status: PROPOSED, never approved.** Revision 5 was reviewed and NOT - **Status: PROPOSED, never approved.** Revision 5 was reviewed and NOT
approved (six findings, four P1); revision 6 answered them; **revision approved (six findings, four P1); revision 6 answered them; **revision
7 resolves a cross-lane conflict with PR #186**. The commit history 7 resolves a cross-lane conflict with PR #186**. The commit history
embodies six revisions and five rounds of findings; **that is not the embodies six revisions and five rounds of findings; **that is not the
same as approval**, and it must not be read as one. same as approval**, and it must not be read as one.
- **Round 7 (rev 8) found five contract defects of ONE family, and the
family is the transferable lesson: a guarantee assumed from a
mechanism whose implementation was never read.** Reply order assumed
to be execution order; a refusal assumed to be inert; `forget_uri`
assumed to cover every writer. Three of the five were literally that.
The decisions:
- **Reply order is NOT execution order.** `AsyncRuntime::tick`
(`src/async_runtime.rs:1003`) is `while let Ok(env) =
self.main.try_recv()` — a bus drain with **no execution token**, so
a worker can finish, be descheduled before sending, and have a later
reply arrive first. The ordering guarantee was **withdrawn, not
engineered**: reconciliation is order-independent, and `fs.lua:155-165`
already instructs callers needing ordering to serialize. A lock was
rejected — it would serialize every fs mutation for a hazard with no
production reachability.
- **`EditorCore::kill_buffer` damages editor state BEFORE it can
refuse.** It clears `round_trip_buffers`, closes side windows and
redirects ordinary windows, and only then can
`BufferRegistry::remove` return `ConcurrentEdit`. So "refused" is
not "nothing happened". Fixed by preflighting `editing_in_progress`
— sound because phase 1 is pure `EditorCore` and holds no Lua
handle, so nothing can re-enter between check and removal.
- **Buffer names are set from `path.display()` AS GIVEN** while only
`file_path` is normalized (`src/editor_core.rs:917`,
`src/lua_bindings/mod.rs:3112`), so a relative open leaves a short
name that a string-equality rule mistakes for user-chosen. The rule
is now path-equivalence.
- **`diag_store` has ZERO correlated writers**, and
`DiagnosticStore.by_uri` is keyed by **URI alone** with no server
component (`src/diag.rs:198`) — so the store most needing protection
is the one a `pending_routes` purge cannot help, and a
`(sid, uri)` tombstone would not even match it. Gated by a bounded
tombstone, keyed to match the store.
- **A first pass of rev 8 checked only `handle_notification` and
concluded `publishDiagnostics` was the only uncorrelated writer.
Wrong lens boundary** — `pub fn mark_document_stale`
(`src/lsp.rs:3108`) takes **no `LspServerId`** and creates URI keys
across three stores for every server. Recorded because it is the
round's own defect class occurring inside the round.
- **Both new hooks are `all-must-succeed`, not short-circuit** — a gap
the review did not raise and the sweep found. `src/hook.rs` defines
three `HookKind`s; registered short-circuit, one `resource.renamed`
subscriber returning falsey would silently stop every later
subscriber reconciling.
- **CROSS-LANE SPLIT WITH PR #186 — settled, recorded verbatim so the - **CROSS-LANE SPLIT WITH PR #186 — settled, recorded verbatim so the
two lanes cannot diverge again:** two lanes cannot diverge again:**

View File

@ -1,12 +1,13 @@
# Dired Stage 2 — marks and operations — framing # Dired Stage 2 — marks and operations — framing
**Revision 7 — 2026-07-28. Status: PROPOSED — NOT APPROVED. This **Revision 8 — 2026-07-28. Status: PROPOSED — NOT APPROVED. This
document has never received a formal framing approval, and it needs one document has never received a formal framing approval, and it needs one
from the user before any implementation branch is cut.** Its commits from the user before any implementation branch is cut.** Its commits
embody five rounds of findings; that is not the same as approval. embody six rounds of findings; that is not the same as approval.
Revision 6 answered review round 5; **revision 7 resolves a cross-lane Revision 7 resolved the cross-lane split with PR #186 — accepted, and
conflict with PR #186**, which framed the opposite answer to the same not reopened here. **Revision 8 answers review round 7: five blocking
event. §0's round-6 section says what the reconciliation changed. contract defects and two documentation fixes**, all of one family. §0's
round-7 section says what each decided.
**Ground truth: re-scouted 2026-07-28 against canonical `main` @ **Ground truth: re-scouted 2026-07-28 against canonical `main` @
`6bee09d`** (`Merge pull request #184 from levineuwirth/bottom-panel-stage2b`). `6bee09d`** (`Merge pull request #184 from levineuwirth/bottom-panel-stage2b`).
@ -44,6 +45,297 @@ numbers drift and this document has now watched them drift twice.
## 0. Revision history ## 0. Revision history
### Review round 7 (rev 7 → rev 8) — five contract defects, one family
The split with #186 was accepted and **none of it is reopened**. What
round 7 found instead is five places where this framing **asserted a
guarantee it had derived from a mechanism whose implementation it never
read**. Findings 1, 2 and 4 are literally that: reply order assumed to
be execution order, a refusal assumed to be inert, `forget_uri` assumed
to cover every writer. Findings 3 and 5 are the same shape one level
out — a naming rule assumed from how *some* buffers are named, and a
callback contract assumed from a helper signature that cannot express
it.
Every citation was re-verified here before being acted on. **All seven
hold.** One is understated (F2); nothing in the review was wrong.
#### F1 — "settle order" is not filesystem mutation order → **the ordering guarantee is WITHDRAWN, not engineered**
Verified: `AsyncRuntime::tick` (`src/async_runtime.rs:1003`) is
`while let Ok(env) = self.main.try_recv()` — it drains the bus and
records **arrival** order. Mutations run on separate pool workers, so a
worker can finish, be descheduled before sending, and have a later
mutation's reply arrive first. `TickOutcome.resources` therefore cannot
carry execution order, and **rev 7's justification for a single ordered
vector was false.**
**The cheaper question first, as directed: does reconciliation need to
be order-dependent?** Working it through:
- For **independent** mutations — disjoint paths, disjoint subtrees —
reconciliation commutes. Order is irrelevant.
- For **interdependent** ones it genuinely is not, and *no static rule
rescues it*. Take rename `dir`→`newdir` racing delete `dir/child.txt`.
If the delete ran first on disk, correct reconciliation is delete-then-
rename. If the rename ran first (so the delete was really of
`newdir/child.txt`), correct reconciliation is rename-then-delete. A
fixed rule such as "deletes before renames" gets the first case right
and the second wrong: the kill misses, the rename then rebinds the
buffer onto a path whose file is gone, and it survives pointing at
nothing. **So it is a real execution-order token or nothing** — this
was worked out rather than assumed, because the review asked which.
- **But no production path can produce the interdependent case.** dired
**serializes** — one coroutine per batch, awaiting each op before
dispatching the next (§9). `apply_resource_op` is **synchronous on the
main thread** and never enters the drain at all. And §2 verified that
`pmacs.fs.rename` and `pmacs.fs.remove` have **zero production
callers** besides tests. The hazard requires a third-party package to
fire-and-forget two interdependent mutations.
- **And the substrate already tells it not to.** `fs.lua:155-165` states
the contract: *"If a package needs at-most-one-pending semantics for
mutations, it should serialize on the package side (await each op
before dispatching the next)."* §9 already cites this as the reason
dired serializes.
**Decision: the reconciliation contract is order-independent by
construction, and promises nothing about two mutations in flight
simultaneously.** Each settled mutation reconciles on its own; the
framing states explicitly that `resources` is in **bus-arrival order,
which is not execution order**, and does not build on the sequence.
Where interdependence exists, the caller owes serialization, and the
primitive's own documentation already says so.
**Why the token was rejected.** An execution-order token established
while holding a mutation lock would serialize every filesystem mutation
through one lock — undoing the concurrency the worker pool exists for —
to close a hazard with no production reachability and a documented
caller-side remedy. It is named as a deferral (§11) with its trigger
stated: **the first production caller that fire-and-forgets two
interdependent mutations.** That is a condition someone can check, not a
vague "if it becomes a problem".
Consequences carried through: rev 7's one-vector-because-ordered
argument is replaced (§5); §6's "via the same ordered sequence" is
reworded; a new acceptance pins that two **independent** concurrent
mutations reconcile correctly **regardless of arrival order**, and §13
states explicitly that there is **no** item for interdependent ordering,
with the reason — a test cannot pin an order the mechanism does not
establish. That is the same discipline item 20 already applies to H1's
open interval.
#### F2 — a refused mid-edit kill is already destructive → **preflight, and the review understates it by one**
Verified in `EditorCore::kill_buffer` (`src/editor_core.rs:4590`), in
execution order: the last-buffer and unknown-id guards return early
(safe); then `self.round_trip_buffers.remove(&buffer_id)`; then the
fallback is computed; then side windows showing the victim are
**closed** via `remove_side_window`; then every remaining window on the
victim is redirected, resetting `text_view`, `cursor`, `selection`,
`overlays`, `view_top`, `goal_col`; and **only then** does
`BufferRegistry::remove` (`src/buffer_registry.rs:127`) get the chance
to refuse with `ConcurrentEdit`. So "refused" is not "nothing happened".
**Where rev 7 was worse than the review says:** rev 7 did not merely
mis-describe the refusal, it wrote *"the reconcile must treat a phase-1
failure as 'keep the buffer' and not run phase 2"* — which reads as
though skipping phase 2 restores the buffer. It does not. Skipping
phase 2 only avoids firing `on_removed` for a buffer that still exists;
the window and round-trip damage is already done and nothing in the
described flow undoes it.
**Decision: preflight `editing_in_progress` before phase 1.** Not a
transactional kill. Three reasons:
- **The preflight is sound, not merely cheap.** Phase 1 is entirely
`EditorCore`, which holds **no Lua handle** (the layering fact C1
established), so nothing between the check and
`BufferRegistry::remove` can re-enter Lua and start an edit. The
window that would make a preflight racy does not exist on this path.
- **It matches #186.** Its Q#RD2 already moves `editing_in_progress`
out of discovery and into validation, for the same reason — *"Today a
`ConcurrentEdit` refusal from `BufferRegistry::remove` arrives after
the file is gone."* Both lanes then check the same predicate in the
same phase.
- **A transactional kill would need a compensation path** that
snapshots and restores window layout, side-window collapse and
round-trip membership — and compensation can itself fail. A check that
makes the failure unreachable is strictly smaller than a rollback that
handles it.
Acceptance 53 is split into **three separately-asserted properties with
individual bites** (§13).
#### F3 — the name-provenance rule is false for relative opens → **path-equivalence, stated**
Verified: `get_or_load_buffer` (`src/editor_core.rs:917`) sets
`display_name = path.display().to_string()`**the path as given**
and normalizes only the stored `file_path` via `set_buffer_path`.
`pmacs.buffer.from_file` (`src/lua_bindings/mod.rs:3112`) does the same:
`create_from_bytes(path.clone(), …)` with the raw string. So opening
`foo.rs` relatively yields name `foo.rs` and path `/abs/dir/foo.rs`.
Rev 7's rule — update the name only when it **equals** the normalized
old path — leaves that buffer's name stale, and it is not user-renamed.
**Decision: the rule is path-equivalence, not string equality.** The
name is treated as path-derived — and therefore updated — **iff the
stored name, parsed as a path and normalized by
`normalize_buffer_path`, equals the buffer's stored normalized old
path.** In words: *the name still denotes this file.*
- A full-path name (Stage 1's and dired's shape) qualifies.
- A relative name `foo.rs` qualifies, because it normalizes to the same
absolute path.
- A genuinely custom name — `notes`, `*scratch*`, anything the user
chose — does not, and is preserved. That direction is what stops the
rule over-correcting, and §13 tests it.
**One consequence stated rather than hidden:** when the rule fires the
new name is written as the **normalized new path**, so a buffer opened
by a relative path acquires an absolute name after a rename. Preserving
the relative rendering would need a record of *what base the name was
relative to*, which no buffer carries. The effect is confined to the
statusline and buffer list. If that is judged wrong, the alternative is
an explicit provenance flag on `Buffer` — real state, every creation
site audited — and this framing does not think a corner of the
statusline earns that.
#### F4 — late `publishDiagnostics` can repopulate the old URI
Verified: the manager absorbs `textDocument/publishDiagnostics`
unconditionally (`src/lsp.rs:2878`); it is a server-initiated
notification with **no request id**, so `pending_routes` — which is what
`forget_uri`'s purge and awaiter drain operate on — cannot see it. A
notification queued before `didClose` can therefore arrive after the
store is cleared and recreate the entry under the old URI.
This is the five-owner census in a new lens, and the review is right
that it is the same shape. **The re-run is reported in full in §5**, and
it changed the design four times over — most sharply: `diag_store` has
**zero** correlated writers, so the store `forget_uri` most needs to
protect is the one its route purge cannot help; and
`DiagnosticStore.by_uri` is keyed by **URI alone**, with no server
component, so a `(sid, uri)` tombstone would not match it.
**Answering the question as asked: no, `publishDiagnostics` is not the
only one.** It is the only uncorrelated **notification** writer — 1 of
1, and `handle_notification` has no default arm — but
`pub fn mark_document_stale` (`src/lsp.rs:3108`) is a second
uncorrelated writer that takes **no `LspServerId`** and creates URI keys
across three stores for every server at once. **A first pass of this
revision checked only `handle_notification` and concluded it was the
only one. That was the wrong lens boundary, and it is this round's own
defect class occurring inside the round** — recorded rather than
quietly corrected, because "I checked the mechanism" and "I checked the
right mechanism" are different claims.
**Decision: a bounded per-server tombstone, checked at absorb.**
`forget_uri(sid, uri)` records `(sid, uri)` as forgotten; an
uncorrelated absorb whose URI is tombstoned is **dropped**; the
tombstone is cleared when that URI is next `did_open`ed, and wholesale
at the existing server-teardown sites (`start_generation`, `forget`).
**Why a tombstone and not the obvious membership gate.** The tempting
version is "absorb only if `(sid, uri)` is currently in `documents`",
which needs no new state at all. **It would be a behaviour regression:**
servers legitimately publish diagnostics for files the editor never
opened — a crate-wide push naming a dependency — and a membership gate
drops all of them. The tombstone drops **only what this editor
explicitly forgot**, which is the narrow claim that is actually true.
Residue stated: a server that legitimately publishes for the old path
*after* we renamed away from it is also dropped until the tombstone
clears. That is the conservative direction, and it is the same
information-loss trade `forget_uri` already makes for the correlated
stores.
#### F5 — `confirm { prompt, on_yes }` cannot express decline → **three outcomes, because the substrate already has three**
Verified: the copy contract says a declined overwrite **continues**,
copying the non-colliding entries, while the helper exposes only
`on_yes`. There is no negative continuation to hang that on.
And the substrate is richer than the helper: `pmacs.minibuffer.read`
takes a required `on_accept` and an optional `on_cancel`
(`src/lua_bindings/mod.rs:13403-13417`), and the session carries both
(`src/minibuffer.rs:403-405`), with `cancel()` returning the
on-cancel callback (`:353`). So a prompt has **three** outcomes, not
two: accept-affirmative, accept-negative, and cancel — and rev 7's
helper collapsed all three into "call `on_yes` or do nothing".
**Decision: `pmacs.minibuffer.confirm { prompt, on_yes, on_no,
on_cancel }`**, with decline and cancel **distinguishable**, because the
copy flow needs exactly that distinction and the substrate already
draws it:
- **`on_yes`** — `y`/`yes`, case-insensitive.
- **`on_no`** — any other accepted text, **including an empty `RET`**.
The fail-closed default from Q#DR15 is unchanged; it now has somewhere
to go.
- **`on_cancel`** — `C-g`/Escape. **If omitted, cancelling does
nothing at all** — it does *not* fall through to `on_no`.
That last point is the decision worth arguing with, so here is why. For
`x` and `D` the two are equivalent: declining and cancelling both mean
"delete nothing". For `C` they are not — declining means *copy the
non-colliding entries* (a partial action), cancelling means *abandon
the batch*. Defaulting cancel to `on_no` would make `C-g` perform a
partial copy, which is the one thing a user pressing `C-g` is trying to
avoid. So cancel is inert unless a caller explicitly opts in.
Acceptance 39 is extended to exercise the negative path and the cancel
path separately — the current item cannot, because there was nothing to
observe.
#### P2 fixes
- **The Lua surface for `forget_uri` is now named.** Rev 7 told a Lua
subscriber to call a manager-level method with no binding behind it.
Lua reaches only explicit bindings; the nearest precedent is
`pmacs.lsp.forget` (`src/lua_bindings/mod.rs:10257`), a four-line
closure that calls through and maps the error with
`mlua::Error::external`. §5 now specifies `pmacs.lsp.forget_uri`, its
error contract, and a pin.
- **The ledger note is rewritten and its numbers re-measured.** It
claimed this branch touches only the framing file — false since rev 6,
which is when the lane moved onto this PR — and quoted a line count
from a previous revision. Counts in §16 and in the ledger are now
measured at this revision.
#### The sweep for the same defect class
Findings 1, 2 and 4 share one shape: **a guarantee assumed from a
mechanism whose implementation was not read.** Swept the rest of the
framing for it. Three candidates, honestly reported:
- **`run_all_must_succeed` "collects errors and does not abort the
fan-out"** (§2). This had been carried from a project lesson rather
than read. **Read now** (`src/hook.rs:332-348`): it is a plain
`for cb in callbacks` loop pushing into `errors` with no early return,
and `proceed` is `errors.is_empty()`. **Claim holds.**
- **`pmacs.window.commit_to` refuses an `await`** (§2), cited to a test
by name. **Verified**: `commit_to_refuses_an_await_and_restores`
exists at `tests/journey_acceptance.rs:746`. **Claim holds.**
- **One genuine new finding, which the review did not raise: the
framing never says which `HookKind` the two new hooks register
with.** `src/hook.rs` defines **three**`ShortCircuit`,
`AllMustSucceed`, `Accumulate` — and every declared hook picks one in
`builtin/hooks/default.lua` (`buffer.after-edit` is
`all-must-succeed`; `path.open-directory` and `editor.before-quit`
are `short-circuit`). Rev 7's B1b asserted only that the *mechanism*
exists. **That gap matters**: registered `short-circuit`, one
`resource.renamed` subscriber returning falsey would stop the fan-out
and silently prevent every later subscriber from reconciling — the
precise trap the typed-edit chain lesson names, arriving through a
door this framing left unlabelled. **Decision: both hooks are
`all-must-succeed`** (Q#DR28), so a failing subscriber is reported and
the rest still run, and no subscriber can claim the event.
Nothing else in the framing rests on an unread mechanism. Recorded as a
count rather than a shrug: **three candidates, two cleared by reading,
one real.**
---
### Round 6 (rev 6 → rev 7) — cross-lane reconciliation with PR #186 ### Round 6 (rev 6 → rev 7) — cross-lane reconciliation with PR #186
Not a review of this document. **PR #186** Not a review of this document. **PR #186**
@ -1376,11 +1668,44 @@ possible, which is why the hook carries `(old, new)` paths.
- matches normalized stored paths against normalized `old` by **equality - matches normalized stored paths against normalized `old` by **equality
or path-component prefix** (`/foo` must not match `/foobar`); or path-component prefix** (`/foo` must not match `/foobar`);
- sets the new path **and** sets the name, but only when the buffer's - sets the new path **and** sets the name, but only when the buffer's
name still equals its old path — a path-backed buffer is named by its name is **path-derived**, by the equivalence rule below;
full path (Stage 1's finding), while a user-renamed buffer keeps the
name it was given;
- returns every rebind it performed. - returns every rebind it performed.
**The name-provenance rule (Q#DR30, rewritten in rev 8 — F3).** Rev 7
updated the name only when it **equalled** the normalized old path,
assuming path-backed buffers carry full-path names. **They do not.**
`get_or_load_buffer` (`src/editor_core.rs:917`) sets
`display_name = path.display().to_string()` — the path **as given**
and normalizes only the stored `file_path`; `pmacs.buffer.from_file`
(`src/lua_bindings/mod.rs:3112`) passes the raw string the same way. So
`pmacs foo.rs` yields name `foo.rs`, path `/abs/dir/foo.rs`, and rev 7's
rule would have left that name stale while insisting it was
user-chosen.
The rule is **path-equivalence**, not string equality:
> A buffer's name is path-derived — and therefore updated — **iff the
> stored name, parsed as a path and normalized by
> `normalize_buffer_path`, equals the buffer's stored normalized old
> path.**
In words: *the name still denotes this file.* A full-path name
qualifies; a relative name qualifies, because it normalizes to the same
absolute path; and a name the user chose — `notes`, `*scratch*` — does
not, and survives. Both directions are load-bearing, and §13 tests
both: the relative case is what rev 7 got wrong, and the custom case is
what stops the fix over-correcting into a name-clobberer.
**One consequence, stated rather than hidden:** when the rule fires the
new name is written as the **normalized new path**, so a buffer opened
by a relative path acquires an absolute name after a rename. Preserving
the relative rendering would require knowing *which base the name was
relative to*, which no buffer records. The effect is confined to the
statusline and the buffer list. The alternative — an explicit
provenance flag on `Buffer`, with every creation site audited — is real
core state for a corner of the statusline, and this framing does not
think that trade is worth it. Named in §11 in case review disagrees.
**Both rename paths call it**: the async harvest below, and **Both rename paths call it**: the async harvest below, and
`apply_resource_op`'s rename arm (`mod.rs:3234-3255`), whose raw `apply_resource_op`'s rename arm (`mod.rs:3234-3255`), whose raw
first-match lookup at `:3249` is deleted in favour of it. One function, first-match lookup at `:3249` is deleted in favour of it. One function,
@ -1458,6 +1783,25 @@ in-flight routes is a race that reintroduces exactly the state it removed.
**One manager-level method, `forget_uri(sid, uri)`**, doing all of it — **One manager-level method, `forget_uri(sid, uri)`**, doing all of it —
because fourteen call sites at the Lua layer is how one gets forgotten. because fourteen call sites at the Lua layer is how one gets forgotten.
**And it needs a Lua binding, which rev 7 never named** (rev 8, P2).
The subscriber that calls this lives in `lsp.lua`, and Lua reaches only
explicit bindings. The surface is **`pmacs.lsp.forget_uri(server_id,
uri)`**, modelled on `pmacs.lsp.forget` (`src/lua_bindings/mod.rs:10257`)
— a closure over the shared manager that calls through and maps the
error with `mlua::Error::external`. Its **error contract**:
- **Raises** on an unknown `server_id`, matching `forget`'s existing
behaviour for the same input.
- **Succeeds silently** when the URI has no state under that server.
The subscriber fires for every renamed path, including buffers that
never attached to a language server, so "nothing to forget" is the
common case and must not be an error.
- Takes the **old** URI. Calling it after `didOpen` of the new URI is
therefore safe and order-independent with respect to step 5.
Pinned by §13 item 31, which asserts both arms — the raise and the
silent success.
Its shape is modelled on the **server-scoped** teardowns that already Its shape is modelled on the **server-scoped** teardowns that already
exist. **There are two of them, and rev 4 named neither correctly (W2):** exist. **There are two of them, and rev 4 named neither correctly (W2):**
`LspManager::start_generation` (`src/lsp.rs:1307-1345`, the restart- `LspManager::start_generation` (`src/lsp.rs:1307-1345`, the restart-
@ -1497,6 +1841,121 @@ three things one axis over:
too, so only the document-scoped entry is dropped — the same too, so only the document-scoped entry is dropped — the same
asymmetry that makes `WorkspaceSymbol` route-exempt in step 1. asymmetry that makes `WorkspaceSymbol` route-exempt in step 1.
#### The uncorrelated writers, and the tombstone that gates them (rev 8, F4)
`forget_uri`'s three steps all operate on `pending_routes` — the
**correlated** path, where a response is matched to a request id. There
are writers that never go near it.
**The census, re-run with "uncorrelated writers" as the lens.** Counted
over production code only, with `#[cfg(test)]` boundaries read per file
rather than inferred from filenames. **41 writes total**: 16 correlated,
19 uncorrelated store writes, 6 `documents` writes.
- **Correlated: 16**, every one inside
`LspManager::absorb_routed_response` (`src/lsp.rs:2667`), which has
exactly one caller — `handle_response` (`:2523`) behind
`pending_routes.remove(&(sid, rid))` at `:2627`. These are
purged by construction if the route drain runs first.
- **Uncorrelated: 19** = **1** server-initiated notification + **3**
`mark_document_stale` writes + **15** Lua-callable `clear` bindings.
**Four findings that change the design, not just the prose:**
1. **`diag_store` has ZERO correlated writers.** The 16 correlated
writes cover 13 of the 14 stores; diagnostics are populated *only*
by the uncorrelated path. So the one store `forget_uri` most needs
to protect is the one its route purge cannot help at all.
2. **`publishDiagnostics` is the only uncorrelated *notification*
writer — but not the only uncorrelated writer.** `handle_notification`
(`src/lsp.rs:2878`) is 22 lines, matches exactly one method string,
and has no default arm; everything else reaches only `push_event`,
which writes the event queue and status tracker and no URI-keyed
store. So among notifications it is **1 of 1**. But
**`pub fn mark_document_stale(&self, uri)` (`src/lsp.rs:3108`)** is a
second uncorrelated writer: it takes `&self` and **no
`LspServerId`**, marks `stale_uris` in three stores **for every
server at once**, *creates* URI keys, and is exposed to Lua as
`pmacs.lsp._mark_document_stale` (`src/lua_bindings/mod.rs:9742`).
**An earlier pass of this framing checked only `handle_notification`
and concluded "publishDiagnostics is the only one in Rust". That was
the wrong lens boundary and the answer was wrong** — recorded because
it is the round's own defect class caught inside the round.
3. **`DiagnosticStore.by_uri` is keyed by URI *alone*** (`src/diag.rs:198`),
with **no `LspServerId` component**, unlike the other thirteen which
key on `(server, uri)`. **So `forget_uri(sid, uri)` cannot be
server-scoped for the one store that has the uncorrelated writer.**
The tombstone must therefore be keyed to match whatever the store is
keyed to, and the framing must not pretend a `(sid, uri)` tombstone
protects a URI-only store.
4. **`epochs` is never pruned.** `DiagnosticStore::clear` *creates* an
`epochs` entry (`src/diag.rs:266`, `or_insert(0) += 1`), as does
`set` (`:250`), and nothing removes them. A `forget_uri` clearing
only `by_uri` leaves a URI-keyed leak behind, so the store's own
forget path must drop the epoch too.
**And the lens reproduces owner 6 independently.** `lean.lua` writes
`M.file_progress[uri]` from
`pmacs.lsp.on_notification("$/lean/fileProgress", …)`
(`builtin/runtime/lean.lua:648,651`) through a **second, Lua-side
notification dispatch table** (`dispatch_notification`,
`builtin/runtime/lsp.lua:1719`, driven from `:1867`). It is
uncorrelated by the same mechanism, `forget_uri` cannot reach it, and it
is exactly §5's sixth path owner. The census arriving at it from a
different direction is the strongest evidence yet for §5's conclusion:
**the Rust method handles what it can see, and the hook is the
mechanism that scales.**
**The gate: a bounded tombstone, keyed to match the store.**
`forget_uri` records the forgotten URI as tombstoned; an uncorrelated
absorb for a tombstoned URI is **dropped**; the tombstone clears when
that URI is next `did_open`ed, and wholesale at the two server-teardown
sites (`start_generation`, `forget`). Per finding 3 the diagnostics
tombstone is **URI-keyed, not `(sid, uri)`-keyed**, matching
`by_uri`; per finding 4 the forget path also drops the URI's `epochs`
entry.
**Why not the cheaper membership gate.** The tempting version needs no
new state: absorb only if `(sid, uri)` is in `documents`. **It would be
a behaviour regression** — servers legitimately publish diagnostics for
files the editor never opened, a crate-wide push naming a dependency,
and a membership gate drops every one. The tombstone drops **only what
this editor explicitly forgot**. There is precedent for exactly this
shape: `handle_response` already drops late arrivals via
`client.cancelled_rids.remove(&rid)` (`src/lsp.rs:2549`) — a
"forget-then-drop-late-arrivals" set. The tombstone is that pattern with
a URI key instead of a request id.
**Why the existing epoch cannot serve.** `epochs` is bumped
unconditionally by `set` with no epoch parameter and is read only by
`epoch_for` for render-cache invalidation (`src/semantic_render.rs:2107`).
Nothing compares an incoming write's epoch to a stored one, so a late
notification simply bumps it and looks current. `stale_uris` is likewise
a one-bit render-suppression flag that gates the **read** path only. And
`LspClient::attempt` (`:3009`) is a real generation counter but
**per-server**, useless for a closed URI on a live server. **There is no
tombstone in the tree today** — zero occurrences — so this is new state,
and the framing says so rather than implying it reuses something.
**Verified absence of any existing guard**, stated with evidence rather
than as a claim: `grep -rn "documents.contains_key" src/` returns
**zero**, and the only `documents` membership test anywhere is
`inbound_converted` (`src/lsp.rs:1498`), which on a miss returns the
value **unconverted and proceeds** rather than dropping it.
`absorb_publish_diagnostics` (`:2900`) guards only that `uri` is a
string and `diagnostics` is an array, then writes.
**Residue, stated:** a server that legitimately publishes for the old
path *after* we renamed away from it is dropped until the tombstone
clears — the conservative direction, and the same trade `forget_uri`
already makes for the correlated stores. Two further holes are named,
not closed, because they are wider than this lane (§11): the fourteen
`pub fn *_store()` accessors hand out `Arc<Mutex<…>>` clones conferring
unrestricted write access, and the `workspace/*/refresh` handlers
re-pull by iterating `attachments` with no cross-check against
`documents`, so a purge can be followed by a fresh, correlated request
for a URI the editor no longer holds.
**Worth stating because it is surprising, and it is now true twice:** **Worth stating because it is surprising, and it is now true twice:**
*neither* server-scoped teardown clears the fourteen result stores. *neither* server-scoped teardown clears the fourteen result stores.
`start_generation` clears `deferred_notifications`, `pending_routes`, `start_generation` clears `deferred_notifications`, `pending_routes`,
@ -1670,16 +2129,27 @@ pub struct TickOutcome {
} }
``` ```
**One ordered vector, not two fields.** A `renames` and a `deletes` **One vector, not two fields — but NOT because it is ordered** (rev 8,
vector would lose the relative order of operations that settle in the F1). Rev 7 justified the single vector by claiming it preserved the
same tick, and that order is load-bearing: rename `dir``newdir` and relative order of mutations settling in the same tick. **That claim was
delete `dir/child.txt` can settle together, and reconciling the delete false and is withdrawn**: `tick` (`src/async_runtime.rs:1003`) is
first targets a path that no longer exists while reconciling it second `while let Ok(env) = self.main.try_recv()`, a drain of the reply bus
targets `newdir/child.txt`. Only one of those is right, and only an with **no execution token**, so `resources` is in **bus-arrival order,
ordered sequence can express which. which is not filesystem-mutation order** — a worker can complete, be
descheduled before sending, and have a later mutation's reply arrive
first.
The vector stays because it is one homogeneous list of settled
mutations that consumers dispatch on by kind, which keeps
`PendingJob.resource` and the outcome the same shape. **Nothing in the
reconciliation may depend on its sequence**, and §6 states the contract
that makes that safe.
`resources` carries **only** jobs that settled `PendingState::Complete` `resources` carries **only** jobs that settled `PendingState::Complete`
— a failed or cancelled mutation reconciles nothing, and fires no hook. — a failed or cancelled mutation reconciles nothing, and fires no hook.
Its documentation must say **bus-arrival order, not execution order**,
in those words: a future consumer that reads "in settle order" and
infers causality is the exact mistake rev 7 made.
Settle identity and resource metadata still come out of **one** Settle identity and resource metadata still come out of **one**
transaction, from the loop at `:1074-1108` that already borrows transaction, from the loop at `:1074-1108` that already borrows
`pending` and reads `job.kind`. The ~17 in-crate `let _ = rt.tick();` `pending` and reads `job.kind`. The ~17 in-crate `let _ = rt.tick();`
@ -1794,12 +2264,32 @@ not gain a Lua handle.
`"cannot kill the last remaining buffer"`. Deleting the file behind `"cannot kill the last remaining buffer"`. Deleting the file behind
the only open buffer therefore deletes the file and **keeps** the the only open buffer therefore deletes the file and **keeps** the
buffer — reported, not silently ignored, and returned in `refused`. buffer — reported, not silently ignored, and returned in `refused`.
- **A mid-edit buffer refuses removal.** `BufferRegistry::remove` - **A mid-edit buffer refuses removal — and the refusal is NOT inert
returns `RegistryError::ConcurrentEdit` when `editing_in_progress()`, (rev 8, F2).** `BufferRegistry::remove` returns
leaving the registry untouched. Phase 1 having already redirected `RegistryError::ConcurrentEdit` when `editing_in_progress()` and
windows, a partial kill is possible here; the reconcile must treat a leaves the *registry* untouched — but by then `kill_buffer` has
phase-1 failure as "keep the buffer" and not run phase 2, or callbacks already, in this order, dropped the id from `round_trip_buffers`,
fire for a buffer that still exists. **closed** any side window showing the buffer, and redirected every
remaining window onto a fallback with `text_view`, `cursor`,
`selection`, `overlays`, `view_top` and `goal_col` all reset. Rev 7
said to "treat a phase-1 failure as keep the buffer", which reads as
though skipping phase 2 restored something. **It does not** — it only
avoids firing `on_removed` for a buffer that still exists.
**So `reconcile_delete` preflights `editing_in_progress` before phase
1** and skips the buffer entirely, returning it in `refused`. The
preflight is *sound*, not merely cheap: phase 1 is entirely
`EditorCore`, which holds **no Lua handle** (C1), so nothing between
the check and `BufferRegistry::remove` can re-enter Lua and begin an
edit — the window that would make a preflight racy does not exist on
this path. #186's Q#RD2 moves the same predicate into its validation
phase for the same reason, so both lanes check it before mutating.
A transactional kill was rejected: it needs a compensation path
snapshotting and restoring window layout, side-window collapse and
round-trip membership, and compensation can itself fail. A check that
makes the failure unreachable is smaller than a rollback that handles
it.
- **Neither failure aborts the reconciliation of other buffers.** A - **Neither failure aborts the reconciliation of other buffers.** A
directory delete reaching twelve descendants must not stop at the one directory delete reaching twelve descendants must not stop at the one
that is mid-edit. that is mid-edit.
@ -1845,7 +2335,7 @@ alone.
Rev 2 left this ambiguous, and the two options really do produce Rev 2 left this ambiguous, and the two options really do produce
different primitive contracts. Rev 3 chooses the one symmetric with different primitive contracts. Rev 3 chooses the one symmetric with
rename: **`remove` is harvested in the drain**, through the same rename: **`remove` is harvested in the drain**, through the same
`TickOutcome.resources` sequence, firing **`resource.deleted(path)`**. `TickOutcome.resources` list, firing **`resource.deleted(path)`**.
`PendingJob` carries the path for `JobKind::FsRemove` in the same `PendingJob` carries the path for `JobKind::FsRemove` in the same
`Option<ResourceOp>` field it carries a rename's pair in (§5, R3) — one `Option<ResourceOp>` field it carries a rename's pair in (§5, R3) — one
field, one enum, so the two cannot both be set. field, one enum, so the two cannot both be set.
@ -1856,6 +2346,48 @@ must reconcile too, and dired firing the hook itself after its own
dired's preflight; the mechanism (what to reconcile once the syscall dired's preflight; the mechanism (what to reconcile once the syscall
lands) is the primitive's. lands) is the primitive's.
### Reconciliation is order-independent, and says so (Q#DR29, new in rev 8)
**Each settled mutation reconciles on its own. Nothing depends on the
relative order of two mutations that were in flight simultaneously**, and
the framing promises nothing about it — because `TickOutcome.resources`
is bus-arrival order and the runtime establishes no execution order (§5,
F1).
That is safe rather than merely honest, for three verified reasons:
- **Independent mutations commute.** Disjoint paths and disjoint
subtrees reconcile to the same registry state in either order, which
is every case the shipped consumers can produce.
- **Interdependent concurrent mutations cannot arise from any production
path.** dired **serializes** — one coroutine per batch, awaiting each
op before dispatching the next (§9). `apply_resource_op` is
**synchronous on the main thread** and never enters the drain. And §2
verified `pmacs.fs.rename` and `pmacs.fs.remove` have **zero
production callers** besides tests.
- **The primitive already instructs callers to serialize.**
`fs.lua:155-165`: *"If a package needs at-most-one-pending semantics
for mutations, it should serialize on the package side (await each op
before dispatching the next)."* §9 already cites this as why dired
does. A caller that ignores it owns the result.
**Why no static ordering rule is offered.** It was worked out rather
than waved away: rename `dir`→`newdir` racing delete `dir/child.txt`
needs delete-then-rename if the delete ran first on disk, and
rename-then-delete if the rename did. A fixed "deletes before renames"
rule gets one right and the other wrong — the kill misses, the rename
then rebinds the buffer onto a path whose file is gone, and it survives
pointing at nothing. **There is no rule short of a real execution-order
token**, which §11 defers with a checkable trigger.
**The residue, stated:** a third-party package that fire-and-forgets two
interdependent mutations, against the documented instruction, can leave
a buffer bound to a stale path or kill one that should have been
rebound. Recoverable, visible, and not data loss — but real. §13 pins
the **independent** case in both arrival orders and deliberately pins no
interdependent one, because a test cannot pin an order the mechanism
does not establish.
### The four cases ### The four cases
| Case | Policy | | Case | Policy |
@ -1929,8 +2461,39 @@ Destructive operations confirm: `x`, `D`, and (in 2c) a recursive delete
and an overwriting copy. There is no helper to do it with (C4). and an overwriting copy. There is no helper to do it with (C4).
**Stage 2 adds `builtin/runtime/minibuffer.lua` defining **Stage 2 adds `builtin/runtime/minibuffer.lua` defining
`pmacs.minibuffer.confirm { prompt, on_yes }`**, loaded before `pmacs.minibuffer.confirm { prompt, on_yes, on_no, on_cancel }`**,
`dired.lua` in `editor.rs`'s explicit sequence. loaded before `dired.lua` in `editor.rs`'s explicit sequence.
**Three outcomes, because the substrate already has three** (rev 8,
F5). Rev 7 exposed only `on_yes`, which cannot express §8's copy
contract — where declining an overwrite **continues**, copying the
non-colliding entries. There was no negative continuation to hang that
on. And the underlying primitive is richer than the helper was:
`pmacs.minibuffer.read` takes a required `on_accept` and an optional
`on_cancel` (`src/lua_bindings/mod.rs:13403-13417`), and the session
carries both (`src/minibuffer.rs:403-405`), with `cancel()` returning
the on-cancel callback (`:353`). A prompt therefore has
accept-affirmative, accept-negative and cancel — and rev 7 collapsed all
three into "call `on_yes` or do nothing".
| Outcome | Trigger | Runs |
|---|---|---|
| **yes** | `y` / `yes`, case-insensitive | `on_yes` |
| **no** | any other accepted text, **including empty `RET`** | `on_no` |
| **cancel** | `C-g` / Escape | `on_cancel`**and nothing if it is absent** |
The fail-closed default from Q#DR15 is unchanged: an empty `RET` is
still not affirmative. It now has somewhere to go instead of being
indistinguishable from silence.
**Cancel does NOT fall through to `on_no`, and that is the decision
worth arguing with.** For `x` and `D` the two are equivalent — decline
and cancel both mean "delete nothing". For `C` they are not: declining
means *copy the non-colliding entries*, a partial action, while
cancelling means *abandon the batch*. Defaulting cancel to `on_no`
would make `C-g` perform a partial copy, which is precisely what a user
pressing `C-g` is trying to avoid. So cancel is inert unless a caller
opts in, and §8's `C` flow is the only caller that does.
**That sequence is a real edit to `src/editor.rs`** — around thirty **That sequence is a real edit to `src/editor.rs`** — around thirty
`include_str!` entries at `src/editor.rs:395-660`, each naming its `include_str!` entries at `src/editor.rs:395-660`, each naming its
@ -2049,9 +2612,13 @@ against `handle.path`. `opts.parents` for `create_dir_all`.
asked once, not once per file mid-batch. asked once, not once per file mid-batch.
3. **Confirm.** With no collisions and one source, no prompt — a copy 3. **Confirm.** With no collisions and one source, no prompt — a copy
onto free space is not destructive. With collisions, **one** confirm onto free space is not destructive. With collisions, **one** confirm
naming the count: `Overwrite 2 existing files? (y/n) `. Declining naming the count: `Overwrite 2 existing files? (y/n) `. **Declining**
**skips the colliding entries and copies the rest**, rather than (`on_no`, including an empty `RET`) **skips the colliding entries and
abandoning the batch, which matches §9's per-entry failure rule. copies the rest**, rather than abandoning the batch, which matches
§9's per-entry failure rule. **Cancelling** (`on_cancel`, `C-g`)
**abandons the whole batch and copies nothing** — the distinction §7
exists to preserve, and the reason `C` is the one caller that passes
all three callbacks.
4. **Dispatch** with `opts.overwrite` set only for the entries the user 4. **Dispatch** with `opts.overwrite` set only for the entries the user
confirmed. The primitive still refuses an existing target without it, confirmed. The primitive still refuses an existing target without it,
so the guard is enforced at both layers. so the guard is enforced at both layers.
@ -2202,6 +2769,20 @@ that deserve an undivided reviewer.
but puts N blocking syscalls on the main thread for an N-entry batch. but puts N blocking syscalls on the main thread for an N-entry batch.
Note this is the *only* thing left of rev 6's orphaning story; the Note this is the *only* thing left of rev 6's orphaning story; the
LSP half went away with #186 rather than being solved here. LSP half went away with #186 rather than being solved here.
- **Two wider LSP-store holes the tombstone does not close** (new in
rev 8, F4). The fourteen `pub fn *_store()` accessors
(`src/lsp.rs:1031-1114`) each hand out an `Arc<Mutex<…>>` clone,
conferring unrestricted `set`/`clear`/`mark_stale` on any holder — the
fifteen Lua `clear` bindings already prove the write capability
crosses the FFI boundary, and nothing in the type system stops a
`set`. Separately, the `workspace/inlayHint/refresh` and
`workspace/semanticTokens/refresh` handlers
(`builtin/runtime/lsp.lua:1845,1853`) re-pull by iterating
`attachments` with **no cross-check against `documents`**, so a purge
can be followed by a fresh — and route-correlated, therefore
ungated — request for a URI the editor no longer holds. Both are
pre-existing, both are wider than a dired stage, and both would be
in scope for an LSP-lifecycle lane rather than this one.
- **`pmacs.fs.remove` itself is guarded by neither lane** (new in rev 7, - **`pmacs.fs.remove` itself is guarded by neither lane** (new in rev 7,
round 6). After both land, the refusal exists at the round 6). After both land, the refusal exists at the
`apply_resource_op` primitive (#186) and in dired's policy layer `apply_resource_op` primitive (#186) and in dired's policy layer
@ -2433,9 +3014,15 @@ that deserve an undivided reviewer.
implementation; this does.)* implementation; this does.)*
28. **False prefix**: renaming `/…/foo` does **not** rebind a buffer on 28. **False prefix**: renaming `/…/foo` does **not** rebind a buffer on
`/…/foobar`. `/…/foobar`.
29. **Buffer name** follows the path, so the buffer list and statusline 29. **Buffer name follows the path — tested in BOTH directions** (F3).
show the new filename — and a buffer the user renamed by hand keeps (a) A buffer opened by a **relative** path (name `foo.rs`, stored
its own name. path `/abs/dir/foo.rs`) gets its name updated, because the name
normalizes to the stored path. *(Rev 7's string-equality rule fails
this — it is the case that motivated the rewrite.)* (b) A buffer
with a **genuinely custom** name (`notes`) keeps it. *(A rule that
updated unconditionally, or matched on basename, fails this — it is
what stops the fix becoming a name-clobberer.)* Both arms are
required; either alone admits a wrong rule.
30. **An attached LSP buffer with diagnostics present before the rename, 30. **An attached LSP buffer with diagnostics present before the rename,
shown in at least TWO windows** (H3): afterwards both windows render shown in at least TWO windows** (H3): afterwards both windows render
the **new** URI's diagnostics, the old URI's store is empty, and each the **new** URI's diagnostics, the old URI's store is empty, and each
@ -2448,6 +3035,22 @@ that deserve an undivided reviewer.
gone, and **a response already in flight at rename time does not gone, and **a response already in flight at rename time does not
repopulate the old key** — the `pending_routes` purge and awaiter repopulate the old key** — the `pending_routes` purge and awaiter
drain, without which the clear is undone by arrival. drain, without which the clear is undone by arrival.
31b. **A late `publishDiagnostics` for the OLD URI does not resurrect
it** (F4): after the rename completes, feed the manager a
`textDocument/publishDiagnostics` notification naming the **old**
URI; the old key stays empty and the new URI's diagnostics are
unaffected. *(This is uncorrelated — it carries no request id — so
the `pending_routes` purge cannot see it, and item 31 passes with
the bug present. Fails against a `forget_uri` with no tombstone.)*
Its companion asserts the tombstone **does not over-reach**: a
`publishDiagnostics` for a **different**, never-opened URI is still
absorbed, which is what a membership gate would have broken.
31c. **`pmacs.lsp.forget_uri`'s error contract** (P2): it **raises** for
an unknown server id, and **succeeds** for a URI with no state under
a known server. *(The second arm is the one that matters — the
subscriber fires for every renamed path, including buffers that
never attached, so an over-strict binding would turn the common case
into an error inside a hook.)*
32. A rename **across project roots** re-runs `ensure_server` and the 32. A rename **across project roots** re-runs `ensure_server` and the
buffer ends up attached to a **different** server; a same-root rename buffer ends up attached to a **different** server; a same-root rename
reuses the existing one (#161's affinity key). reuses the existing one (#161's affinity key).
@ -2466,11 +3069,18 @@ that deserve an undivided reviewer.
**2b — the shared helpers** **2b — the shared helpers**
39. **`pmacs.minibuffer.confirm`** (Q#DR15, F5): an **empty `RET` does 39. **`pmacs.minibuffer.confirm` — all three outcomes** (Q#DR15, F5).
not call `on_yes`**; `y`, `Y`, `yes`, `YES` all do; `n` and arbitrary (a) An **empty `RET` does not call `on_yes`**; `y`, `Y`, `yes`,
text do not. *(A typed-`n` test alone would not catch a completion `YES` all do; `n` and arbitrary text do not. *(A typed-`n` test
source being reintroduced — the empty-`RET` arm is the one that alone would not catch a completion source being reintroduced — the
detects it.)* empty-`RET` arm is the one that detects it.)* (b) **`on_no` runs**
for `n`, for arbitrary text, and for empty `RET` — the negative
continuation §8's `C` flow needs, which rev 7's helper could not
express and rev 7's acceptance could not observe. (c) **`on_cancel`
runs for `C-g`, and `on_no` does NOT**; with `on_cancel` omitted,
cancelling runs **nothing**. *(Fails against an implementation that
routes cancel through `on_no` — which would make `C-g` perform a
partial copy.)*
40. **Serialization** (Q#DR16, F5): in a batch of N mutations, the second 40. **Serialization** (Q#DR16, F5): in a batch of N mutations, the second
is **not dispatched until the first has settled**. Asserted by is **not dispatched until the first has settled**. Asserted by
observing at most one in-flight fs job at any pump step — *not* by observing at most one in-flight fs job at any pump step — *not* by
@ -2532,6 +3142,48 @@ that deserve an undivided reviewer.
(R4): deleting the file behind the **only** open buffer keeps the (R4): deleting the file behind the **only** open buffer keeps the
buffer and says so; and a delete reaching a directory of buffers buffer and says so; and a delete reaching a directory of buffers
where one refuses removal still reconciles the rest. where one refuses removal still reconciles the rest.
53b. **A mid-edit refusal leaves editor state UNCHANGED — three
separate assertions** (F2). With the buffer `editing_in_progress`,
displayed in an ordinary window, shown in a side window, and present
in `round_trip_buffers`, a delete reconciling it must leave **each**
of the following provably untouched, asserted individually rather
than as one compound check:
| # | Assertion | Bite — the mutation that must falsify it |
|---|---|---|
| i | the ordinary window still shows the buffer, with its `cursor`, `selection` and `view_top` intact | drop the preflight, so `kill_buffer` redirects the window to the fallback before `BufferRegistry::remove` refuses |
| ii | the **side** window is still open and still shows the buffer | drop the preflight, so `remove_side_window` collapses it first |
| iii | the buffer is still in `round_trip_buffers` (a semantic frontend still round-trips its keys) | drop the preflight, so `round_trip_buffers.remove` runs first — this is the **first** thing `kill_buffer` does and the easiest to miss |
Each bite is the same one-line deletion, but each assertion fails
independently, which is the point: a single compound assertion can
pass on two of the three and hide the third. *(Rev 7 specified none
of this — it said to treat the refusal as "keep the buffer", which
reads as though skipping phase 2 restored something. It does not.)*
54. **Two INDEPENDENT concurrent mutations reconcile correctly in
either arrival order** (F1, Q#DR29): dispatch a rename and a delete
on **disjoint** paths fire-and-forget, pump, and assert the end
state; then repeat with the replies arriving in the opposite order
and assert the **same** end state. *(Pins that the contract really
is order-independent rather than accidentally order-sensitive.
Fails against a reconciliation that, say, resolves delete targets
against paths already rebound by a rename in the same drain.)*
55. **`resource.renamed` and `resource.deleted` are `all-must-succeed`,
not short-circuit** (Q#DR28): with **two** subscribers registered
and the **first one raising**, the second still runs, and the error
is reported rather than swallowed. *(Fails against a `short-circuit`
registration, where the first subscriber's return would stop the
fan-out and silently prevent every later one from reconciling —
which no test asserting only "the hook fired" would catch.)*
**No acceptance pins interdependent ordering, deliberately.** A test
cannot pin an order the mechanism does not establish (§6, F1): the
runtime records bus-arrival order and no execution token exists, so an
"interdependent mutations reconcile in execution order" test would
either be flaky or would pass by accident on a scheduler that happens to
cooperate. This is the same discipline item 20 applies to H1's open
dispatch-to-syscall interval — **state the gap, do not fake a pin for
it.**
**Bite obligations.** Each of these must fail against a stated mutation: **Bite obligations.** Each of these must fail against a stated mutation:
@ -2658,10 +3310,19 @@ mark, operation and subscriber items.
swept over `core.windows.values_mut()`, chosen over `set_uri` or swept over `core.windows.values_mut()`, chosen over `set_uri` or
re-attach because it reaches passive windows and **preserves overlay re-attach because it reaches passive windows and **preserves overlay
order by mutating in place**.*) (§5) order by mutating in place**.*) (§5)
- **Q#DR15** Confirmation is `pmacs.minibuffer.confirm` in a new - **Q#DR15** *(widened in rev 8, F5)* Confirmation is
`builtin/runtime/minibuffer.lua`, with **no completion source**; `pmacs.minibuffer.confirm { prompt, on_yes, on_no, on_cancel }` in a
new `builtin/runtime/minibuffer.lua`, with **no completion source**;
affirmative is `y`/`yes` case-insensitively and everything else — affirmative is `y`/`yes` case-insensitively and everything else —
including empty `RET` — is no. (§7) including empty `RET` — is no. **Three outcomes, because
`pmacs.minibuffer.read` already has three**: accept-affirmative,
accept-negative and cancel. Rev 7 exposed only `on_yes` and so could
not express §8's copy contract, where declining **continues**.
**Cancel does not fall through to `on_no`** — with `on_cancel`
omitted, `C-g` runs nothing — because for `C` declining means *copy
the non-colliding entries* while cancelling means *abandon*, and
defaulting cancel to decline would make `C-g` perform a partial copy.
(§7, §8, §13 item 39)
- **Q#DR16** Batches **serialize** (await each op), a per-entry failure - **Q#DR16** Batches **serialize** (await each op), a per-entry failure
does not abort, successful marks clear while failed marks persist, and does not abort, successful marks clear while failed marks persist, and
the listing reverts **once** at the end. (§9) the listing reverts **once** at the end. (§9)
@ -2810,7 +3471,74 @@ mark, operation and subscriber items.
needs `&Lua`, so `reconcile_delete` returns the killed ids and its needs `&Lua`, so `reconcile_delete` returns the killed ids and its
caller runs phase 2; `EditorCore` gains no Lua handle. Both refusals caller runs phase 2; `EditorCore` gains no Lua handle. Both refusals
(last buffer, mid-edit `ConcurrentEdit`) are reported and neither (last buffer, mid-edit `ConcurrentEdit`) are reported and neither
aborts the rest of the batch. (§6, §13 items 5153) aborts the rest of the batch. **And the mid-edit case is preflighted,
not caught**: `kill_buffer` clears `round_trip_buffers`, closes side
windows and redirects ordinary windows **before**
`BufferRegistry::remove` can refuse, so a caught `ConcurrentEdit`
leaves editor state already damaged. `reconcile_delete` therefore
checks `editing_in_progress` **before phase 1** and skips the buffer
— sound because phase 1 is pure `EditorCore` and holds no Lua handle,
so nothing can re-enter and begin an edit between check and removal.
(§6, §13 items 5153, 53b)
- **Q#DR28** *(new in rev 8, from the round-7 sweep)* Both new hooks
register **`all-must-succeed`**, not `short-circuit`. `src/hook.rs`
defines three `HookKind`s and every declared hook picks one in
`builtin/hooks/default.lua`; rev 7 asserted only that the mechanism
existed and never said which. It matters: registered `short-circuit`,
a single `resource.renamed` subscriber returning falsey would stop the
fan-out and silently prevent every later subscriber from reconciling
— the typed-edit chain's trap arriving through an unlabelled door.
`all-must-succeed` reports a failing subscriber and still runs the
rest, and lets no subscriber claim the event. (§13 item 55)
- **Q#DR29** *(new in rev 8, F1)* **Reconciliation is
order-independent, and the framing promises nothing about the relative
order of two mutations in flight simultaneously.**
`TickOutcome.resources` is **bus-arrival order, not execution order**
`tick` is a `try_recv` drain with no execution token — so rev 7's
ordered-sequence justification is withdrawn. This is safe because
independent mutations commute, no production path can produce
interdependent concurrent ones (dired serializes; `apply_resource_op`
is synchronous; the fs primitives have zero production callers), and
`fs.lua:155-165` already instructs packages needing at-most-one-pending
semantics to serialize on their own side. **An execution-order token
under a mutation lock was rejected**: it would serialize every fs
mutation through one lock to close a hazard with no production
reachability and a documented caller-side remedy. Deferred with a
checkable trigger (§11). No static ordering rule is offered because
none works — the correct order depends on which mutation actually ran
first, which is exactly what is unknown. (§5, §6, §13 item 54)
- **Q#DR30** *(new in rev 8, F3)* A buffer's name is **path-derived —
and therefore updated by a rename — iff the stored name, parsed as a
path and normalized, equals the buffer's stored normalized old path.**
Not string equality against the path, which rev 7 used: names are set
from `path.display()` **as given** while only `file_path` is
normalized, so a relative open leaves a short name that rev 7 would
have mistaken for user-chosen. The new name is written as the
normalized new path, so a relatively-opened buffer acquires an
absolute name — stated rather than hidden, and confined to the
statusline and buffer list. (§5, §13 item 29)
- **Q#DR31** *(new in rev 8, F4)* Uncorrelated writers are gated by a
**bounded per-server tombstone**, not by document membership.
`forget_uri` records the forgotten `(sid, uri)`; an uncorrelated
absorb for a tombstoned URI is dropped; the tombstone clears on the
next `did_open` of that URI and at both server-teardown sites. The
census establishes that `publishDiagnostics` is the only uncorrelated
**notification** writer, but **not** the only uncorrelated writer —
`pub fn mark_document_stale` takes no `LspServerId` and creates URI
keys across three stores for every server. Two consequences the
tombstone must respect: **`diag_store` has zero correlated writers**,
so the route purge protects it not at all; and
**`DiagnosticStore.by_uri` is keyed by URI alone**, so the
diagnostics tombstone is URI-keyed rather than `(sid, uri)`-keyed, and
the forget path must also drop the URI's never-pruned `epochs` entry.
A membership gate (`absorb only if in documents`) was rejected because
servers legitimately publish for files never opened, and it would drop
all of them; the precedent for the chosen shape is
`client.cancelled_rids` (`src/lsp.rs:2549`), the same
forget-then-drop-late-arrivals set with a request id instead of a URI.
`DiagStore`'s existing `epochs` cannot serve: `set()` bumps it on
every write with no epoch parameter, so a late notification looks
current. (§5, §13 items 31b31c)
## 16. Branch and PR plan ## 16. Branch and PR plan
@ -2840,29 +3568,28 @@ LSP-authored delete that destroys unsaved work. That is **PR #186's**,
and 2a's body should say so and cite it rather than appearing to claim and 2a's body should say so and cite it rather than appearing to claim
it.)* it.)*
**Ledger note (corrected in rev 5, W6):** this framing branch **Ledger note (rewritten in rev 8 — P2; the rev 5 text was stale and
deliberately touches **only** this file. Rev 4 said the durable records self-contradictory).** Two things it got wrong and this corrects:
were held by open PR #169; **#169 merged** as `74301d1`, and its
successor **#185 merged as `ad41cf1` during this re-scout**, so
`docs/active-work.md`, `docs/agent-handoff.md`, and `COHERENCE.md` are
now unheld. This branch still does not touch them — the ops lesson is
that a standalone docs-refresh PR restarts the contention treadmill, and
the ledger's own protocol puts the lane refresh with the work.
**Two things the landed ledger now needs, and this PR is not the place - **This branch no longer touches only the framing file.** It has
for either.** `docs/active-work.md`'s dired Stage 2 lane still records carried `docs/active-work.md`'s dired Stage 2 lane since **rev 6**,
this branch at head `ab42a79`, describes the document as *1,570 lines*, which is when the ledger PR (#185) merged and the lane moved onto this
says *"the re-scout is under way"*, and states the rename census as PR. The rev 5 text still claimed single-file scope while the very same
**five** path owners. Rev 5 makes all four stale: the head has moved, revision was editing the ledger. The reason the lane rides this PR
the document is longer, the re-scout is done, and **the census is six** rather than a standalone refresh is unchanged: with several PRs open,
(§5, W5). That is the standing lesson restated — *a census is a reading, a separate ledger PR re-conflicts on every merge, and the ledger's own
not a constant* — and it applies to the ledger's copy of this protocol puts a lane refresh with the work.
framing's numbers exactly as it applied to the framing's copy of the - **The line counts were quoted, not measured.** Rev 5 described the
tree's. Whoever refreshes the lane should take the six-owner table from document as *1,570 lines* — a figure from two revisions earlier — and
§5 rather than re-deriving it. Rev 6 removes the other half of what rev the ledger in turn reported *~2,630*. **Measured at this revision:
5 said here: Q#DR25 **left** this lane rather than adding scope to it `docs/dired-stage2-framing.md` is 3,624 lines and
(R1), and the ledger already records that at `docs/active-work.md:507` `docs/active-work.md` is 981.** *A census is a reading, not a
— which is how round 5 caught the framing contradicting it. constant*, and that applies to a framing's count of its own size
exactly as it applies to its count of the tree. Neither number above
is copied from anywhere; both were run against the tree being pushed.
`docs/agent-handoff.md` and `COHERENCE.md` remain untouched by this
branch.
### Ownership warning: 2a must not run concurrently with Journey Stage 1b ### Ownership warning: 2a must not run concurrently with Journey Stage 1b