Normalize batch dependency paths through the registry's lexical
canonical form so equivalent URI spellings do not revive the
initial-state preflight bug.
Separate execution-started state from the count of completed plan
items. Preflight failures retain the no-mutation guarantee, while
runtime failures conservatively acknowledge that the failing item may
itself have changed a buffer or the filesystem.
Add real-server-pump acceptance for dot-path dependency aliases,
partial text edits within one item, and resource-operation side
effects, and record the review-round corrections in the framing.
Four findings, all reproduced by the reviewer, all accepted. Two of
them are one defect class — a guard whose scope was REASONED ABOUT
rather than enumerated — so both are recorded in the framing's new §9
together with a sweep of every other place this lane decides something
is "affected".
P1 — the delete preflight broke ordered resource operations
(§9.3). Every delete was judged against the filesystem's INITIAL
state, at plan-construction time, so a valid `create X -> delete X`
was refused with a fabricated NotFound about a path the batch was
about to create; likewise `rename A -> B -> delete B`. This was a
regression this lane introduced, not a pre-existing defect.
Decision: DEFER, do not simulate. A delete whose target is related by
component-aware path containment to a path an EARLIER op in the same
plan creates, renames onto, renames away from, or removes is not
judged at plan time; the primitive judges it when it runs. Q#RD3
already calls this check a filter, not a transaction, so declining to
judge is inside its contract and refusing a legal batch is not.
Simulating instead would mean modelling filesystem presence AND the
registry's path bindings across create/rename/edit — the transaction
Q#RD3 declines to build — and a wrong simulation emits false `clear`
verdicts, which is the dangerous direction. `edit` ops are excluded
from the deferral set on purpose: an edit changes no path's existence,
so it can only turn a plan-time `clear` into a primitive-time
refusal, which Q#RD3 already documents and accepts. The
buffer-and-filesystem half therefore still fires early for any target
no prior op touches, which is what criterion 11c pins.
P1 — the production-boundary acceptances are landed (§9.5).
Criteria 11, 11a-11d, 12 (both directions), 13 and 15 now drive a real
`pmacs_fake_lsp` child over a real transport. One parameterized mode,
`applyeditplan`, replaces the eight the framing named: it reads its
whole WorkspaceEdit from a test-written file and publishes the
client's response to a sink, so each of the eight fixtures sits next
to the assertions that depend on it instead of being mirrored across
two files. Fail-closed — an unreadable plan sends no applyEdit and
reports itself through the sink, so a broken fixture cannot read as a
pass — and the sink is written `.part`-then-rename so a polling reader
never sees a partial record. There is no skip-and-return-ok arm
anywhere: `fake_lsp_path` resolves through `env!("CARGO_BIN_EXE_...")`,
a compile-time constant, so a missing binary is a build failure.
P1 — mid-batch failures were misreported as complete aborts (§9.4).
`apply_workspace_edit` now returns `nil, message, applied_op_count`,
and ONE renderer serves both the user-facing status line and the
server's `failureReason`, so the two cannot disagree. All three
callers are updated, not only the rename one.
P2 — non-recursive deletes inspected descendants (§9.2). `recursive`
is now a parameter of the shared query and descendant matching is
reserved for recursive deletes. The old doc comment argued at length
for the wrong behaviour and is replaced by the counterexample that
falsifies it: a modified buffer at `tree/gone.rs` whose file is
already gone blocked a non-recursive delete of the now-EMPTY `tree/`,
an op that would have succeeded and that removes none of that
buffer's contents. This narrows the Q#RD6 query #171 adopts.
Criterion 3's stated bite: fixed by fixing the SETUP, not the doc.
The first commit's test comment carried a correction saying the
framing's wording was wrong. It was wrong only against that setup —
and §9.2's narrowing would then have left the setup with no bite at
all, since a non-recursive delete no longer inspects a descendant.
So the buffer is now bound to the EXACT deleted path: a file is
opened, then replaced on disk by a non-empty directory, and
`remove_dir` fails with ENOTEMPTY deterministically under any uid.
Both of the framing's stated pre-images now bite, so the framing
needed no amendment there. The correction is recorded in §9.1 rather
than only in a test comment, which is where the review asked for it.
WHY THE SHIPPED SUITE PASSED WHILE FINDINGS 1 AND 4 WERE LIVE — two
coverage facts for the next lane. Every delete criterion drove the
PRIMITIVE directly, so nothing in the suite ever built a multi-op plan
and the preflight's plan-time behaviour had no test at all; the only
batch test, `m4_15`, happens to delete a path no earlier op touches.
And every recursive-delete criterion (7, 8, 9) passes `recursive =
true`, while every non-recursive one binds its buffer to the exact
target, so no test in the suite ever combined a non-recursive delete
with a descendant buffer — the exact cell finding 4 lives in.
Sweep, per the review's request. Seven sites decide something is
"affected"; the table is in framing §9.7. Three were the defects
above. Two are unchanged by design and named so they are not mistaken
for oversights: phase-4 reconciliation compares paths RAW via
`BufferRegistry::find_by_path`, which Q#RD10 pins as "exactly today's
behaviour" and which correcting would widen reconciliation — the one
thing Q#RD5 forbids; and `delete_verdict` stats the raw path while
comparing normalized ones, a latent inconsistency whose every branch
fails safe and which matches the primitive's own `remove_file`. Two
are consistent: the `_delete_verdict` binding defaults `recursive` and
`ignore_if_not_exists` the same way the primitive does, and the
deferral set is enumerated (create: 1 path; rename: 2; delete: 1;
edit: excluded, with the argument written down) rather than reasoned
about. Nothing else in the lane decides an affected set.
Bites. Every row was RUN, with the positive control `scripts/bite`
gained in #192 (merged into this lane), and every ref-based row below
reports `OK (assertion)` rather than `OK (COMPILE)`. `1873be6` is this
lane's own first commit: findings 1, 3 and 4 were introduced by it, so
`main` cannot falsify their pins.
rd11a builtin/runtime/lsp.lua @ main OK (assertion)
rd11b builtin/runtime/lsp.lua @ main OK (assertion)
rd11c builtin/runtime/lsp.lua @ main OK (assertion)
rd11d builtin/runtime/lsp.lua @ main OK (assertion)
rd12a builtin/runtime/lsp.lua @ main OK (assertion)
rd12b builtin/runtime/lsp.lua @ main OK (assertion)
rd13 builtin/runtime/lsp.lua @ main OK (assertion)
rd15 builtin/runtime/lsp.lua @ main OK (assertion)
rd18 src/lua_bindings/mod.rs @ 1873be6 OK (assertion)
rd19a builtin/runtime/lsp.lua @ 1873be6 OK (assertion)
rd19b builtin/runtime/lsp.lua @ 1873be6 OK (assertion)
rd19c builtin/runtime/lsp.lua @ 1873be6 OK (assertion)
rd20 builtin/runtime/lsp.lua @ 1873be6 OK (assertion)
Two rows need their weakness stated rather than hidden.
rd11 is VACUOUS against `main`'s `lsp.lua` and the script says so — a
preflight-less applier passes it, which is expected, because rd11 is
the direction that asserts the guard does NOT over-refuse (the same
shape as criteria 2, 7, 9 and 14). It bites two other ways, both run:
`OK (assertion)` against `main`'s `src/lua_bindings/mod.rs`, where the
primitive's absent-plus-ignore branch destroys the buffer; and against
a hand mutation dropping `ignore_if_not_exists` from the preflight
call, which is the pre-image the framing actually names for it.
rd3's two pre-images are designs never committed, so no ref carries
them and `scripts/bite` cannot be used. Hand-mutated instead:
reconciliation moved ahead of the filesystem mutation makes rd3 fail
on exactly its stated assertion (and rd4 with it). On this setup that
mutation and "validation that removes rather than inspects" are the
same mutation, because the buffer is bound to the exact deleted path —
stated because the first shipped setup could see neither.
The eight rows against `main`'s `lsp.lua` all fail by TIMEOUT rather
than by a value assertion, and that is the pre-image behaviour, not a
flaky harness: on `main` the primitive's raise escapes the applier,
escapes `handle_server_requests`, is swallowed by the
`pcall(handle_server_requests)` at the bottom of the file, and the
server is never answered at all. The sink is therefore never written.
That unanswered request is the defect criterion 13 exists to pin.
Gates: fmt; clippy -D warnings; --lib 1863; --lib --features crdt
2048; m4_acceptance 146 (was 132); lsp_dispatch_seams_acceptance 15;
dired_acceptance 25 and autosave_acceptance 29 (the framing's watch
items); PMACS_REQUIRE_GPU=1 -p pmacs-gpu 202; git diff --check clean.
No protocol change.
Implements the framing merged as #186. On `main` today,
`pmacs.buffer.apply_resource_op`'s delete arm removes a file and then
removes any buffer bound to it, with no dirty check at any link in the
chain — so a server-driven delete destroys unsaved edits, and the
`ignore_if_not_exists` arm destroys them having done no filesystem work
at all.
Layer 1 — the primitive. The delete arm becomes four ordered phases:
stat/no-op decision, enumerate and validate, mutate the filesystem,
reconcile the registry. Validation inspects and removes nothing, so a
filesystem failure leaves every buffer intact automatically rather than
by compensation, and `on_removed` still observes the path already gone
because reconciliation stays last.
`delete_verdict` is the single shared query. It scans *every*
path-bound buffer rather than the first match, because `find_by_path`
is first-match-only and `pmacs.buffer.from_file` makes duplicates
reachable — a clean first match could otherwise hide a modified second.
It normalizes both sides before comparing and uses component-aware
`starts_with`, so `/tree` does not match `/tree-sibling`. It stats with
`symlink_metadata`, not `canonicalize`, which reports a dangling
symlink as absent and would disagree with the primitive on exactly the
input `ignore_if_not_exists` turns on.
Layer 2 — the applier and the server-request boundary.
`apply_workspace_edit` gains a plan-time delete precondition check
driven by the same Rust helper, so the two layers cannot drift. It is a
filter, not a transaction, and the code says so: `documentChanges` are
sequential, so an earlier edit can dirty a buffer a later op deletes.
The applier is now total — every failure becomes `nil, message`, and
the origin buffer is restored on the failure path as well as the
success path. At the boundary, parse *and* apply are wrapped:
`_parse_workspace_edit` sits one line above the applier and is
fallible, so a parse failure previously escaped, was swallowed by
`pcall(handle_server_requests)`, and left the server unanswered — the
defect being fixed, one line out of scope. Failures now also append one
labelled record to `*errors*`.
Scope, stated plainly rather than implied by what is present:
* Acceptance criteria 1-10, 14 and 16 land here — 11 tests driving
the primitive directly. Criteria 11, 11a-11d, 12, 13 and 15 do
NOT: they exercise Layer 2 through a real server pump and need
`pmacs_fake_lsp` modes that do not exist yet. Criterion 13
explicitly rejects a direct-call test as insufficient, so the
Layer 2 code currently has no production-path pin. That is a real
gap and the reason this is not the whole lane.
* The framing's §8 branch plan said the implementation would land on
#186 itself. #186 merged as framing-only, so it gets its own
branch and PR. No decision changes.
* Criterion 3's stated bite in the framing is wrong. It claims to
fail against buffer-first ordering; it does not, because the
deleted path is a directory no buffer is bound to, so the
reordering never fires on that input. It does fail against
validation that removes rather than inspects. Checked by mutation
rather than trusted, and the test comment carries the correction.
Bite: criteria 1, 5, 6, 8 and 10 fail against `githubsucks/main` under
`scripts/bite`. Criteria 3 and 4 pin phase ordering against designs
never committed, so `main` cannot falsify them; both were verified by
hand mutation instead. Criteria 2, 7, 9 and 14 assert preserved or
deliberately-unchanged behaviour and pass against `main` by design —
2 is criterion 1's opposite direction, 9 pins today's imperfect
orphaning so widening cannot happen silently.
Gates: fmt; clippy -D warnings; --lib 1863; --lib --features crdt
2048; m4_acceptance 132; lsp_dispatch_seams_acceptance 15;
dired_acceptance 25 and autosave_acceptance 29 (the framing's watch
items); PMACS_REQUIRE_GPU=1 -p pmacs-gpu 202; git diff --check clean.
No protocol change.
Review round 1 of PR #182. One implementation gap and two stale claims.
**The scope pins the frontend; it does not pin the window.** Framing
§4.4 specified `display{ window = dest:window() }`, but dired's commit
still ended in `pmacs.window.switch_buffer`, which targets whatever
window the scoped frontend has selected. A split or panel that took
focus while `read_dir` was pending therefore received the listing, and
`prev` was captured from it too — with every preflight check passing,
because the captured window was still live and still held its captured
buffer. Both sites now read the captured window: `display` routes to it
with `select = true` (the later `seat_cursor` acts on the active
window), and the `prev` read asks it directly.
N4c pins both halves. The suite's existing routing pins all varied
*frontend* identity; none varied the selected window within one
frontend, which is exactly why 23 green pins missed this. Bite: dired's
`display` back to `switch_buffer` fails N4c alone; `prev` read from the
ambient window fails N4c alone.
Two stale documentation claims, both of which this PR was supposed to
have already fixed:
* **The §0 scorecard still graded §2 "Broken at entry"** while §2's own
ground truth had been rewritten. The scorecard is a second copy of the
same claim and §25's protocol covers both. §19's row and ground truth
were stale the same way — this PR creates the first cross-subsystem
suite, which §19 says should exist and grades as missing — and are
corrected too.
* **P4 still read "leaves exactly one buffer"**, the exact claim rev 6
corrected as false everywhere else in the framing. Restated to what it
actually pins: the file is in the *active window*. The test was
already written correctly; only the framing lied.
Framing rev 8.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 11 put the nesting count in the expander, which is optional. A
consumer at a lower priority can CLAIM and stop the chain before the
expander runs, while that fan-out's deferred-expansion subscriber still
runs — so the nested pass went uncounted, looked like the outermost
one, expanded early, and outer pairing resumed with a record the
replace had invalidated. `\alp(` gave `α(` again.
The count now comes from a no-op consumer registered at the minimum
priority, which runs first in every chain invocation that reaches any
consumer at all. Its guarantee is exactly the ordering contract the
chain already rests on, and it degrades safely: the only thing that can
skip it is a claim ahead of it, which skips the expander too, so
nothing is queued in that fan-out either.
The other plausible home does not work and the comment now says why: a
subscriber registered beside `run_deferred` is too late, because the
whole nested fan-out completes inside the OUTER chain's subscriber,
before either of them runs.
Acceptance 45o pins the short-circuit path — a consumer at 25 that
claims when the record is nil, so the nested pass never reaches the
expander. 45n passes against this bug, which is why both exist.
Counting in the expander fails 45o and nothing else.
Framing rev 12 also names the shape rounds 10–12 share: each fix was
correct about the failure it was shown and wrong about the boundary of
the mechanism it leaned on — the chain's copy semantics, then its
re-entrancy, then its short-circuit. A queue that outlives the thing
that filled it has to name that thing, not approximate it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
`buffer.after-edit` fan-outs NEST — the typed-edit contract supports a
consumer calling `pmacs.hook.run`, and typed_edit.lua's header says so
in its second paragraph. A nested run re-enters every subscriber,
including the deferred expansion's, while the OUTER chain is still
walking its consumer list and pairing has not yet seen the terminator.
So a consumer registered at priority 75 — between the expander at 50
and pairing at 100 — that runs one nested fan-out made `\alp(` yield
`α(` again: the nested pass consumed the queued expansion and edited,
and outer pairing then resumed holding a record the replace had
invalidated. That is round 10's failure reached through the chain's
documented re-entrancy seam rather than through claiming, which is why
deferring alone did not close it.
Deferring work past a fan-out means owning WHICH fan-out it belongs to.
The chain's subscriber and this module's each run exactly once per
fan-out, in that order, so counting invocations of the first and
matching them off in the second identifies the nesting level. Only the
outermost pass expands; a nested one leaves the expansion queued. No
new seam in typed_edit.lua, which is merged Stage 4a substrate.
Both halves bite: removing the level check and never counting
invocations each fail the new acceptance 45n.
Also fixes a test comment that still described the span design round 10
discarded — it claimed the expansion replaces the span "INCLUDING the
terminator". The behaviour asserted was right; the explanation was
stale. Framing rev 11.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Three defects, all about what happens AROUND the expansion rather than
about resolving an abbreviation.
A pair character that TERMINATES an abbreviation never reached
auto-pairing: `\alp(` gave `α(`. Q#LN22 already said the terminator is
not claimed and the implementation claimed it whenever an expansion
succeeded. Merely declining is not enough either — the chain hands each
consumer a copy of the record made before any consumer ran, so
expanding inside the chain invalidates the copy pairing is holding and
the closer is silently lost. Verified by mutation rather than assumed:
expand-then-decline reproduces `α(` exactly.
The expansion therefore runs on its OWN `buffer.after-edit` subscriber,
registered after typed_edit.lua's and before lsp.lua's. A claim stops
the chain but not a separate subscriber, which is the point: pairing
claims the terminator it reacts to. The replaced span now covers only
the leader and the typed text, so pairing's closer lands outside it and
survives. One undo restores the same text either way, because the
terminator was always its own insert.
That second subscriber is a new instance of Q#AP7 — lsp.lua flushes
didChange synchronously on the signature-trigger path, and `(` is a
trigger — so acceptance 45m pins it with the sighelp fake server: no
didChange may ever carry the unexpanded text.
The relevance check is now three-part, as pairing's has been since
#110: buffer, window, AND `ed.cursor() == rec.post_cursor`. A redefined
self-insert can insert the completing character and then move the
point, and expanding over a span the user has left teleports them back
into it.
Cursor placement after the replace is context-guarded, as
`repair_cursor` is. A buffer intercept may switch buffers while
`buf:replace` runs; the unguarded `goto_byte` then translated the Lean
buffer's pre-edit point through the Lean buffer's edit and applied it
to whatever was ambient.
Q#LN22, criterion 38's span wording, and the ledger are corrected to
describe the deferred design rather than the one that shipped — the
rationale's source, not only the sites quoting it. Acceptance 45j/45k/
45l/45m added; framing rev 10.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Journey Stage 1a's core: `pmacs .` opens the directory instead of
exiting 1, and local startup stops being a second implementation of
path resolution.
`EditorState::open` now calls `EditorCore::resolve_target_buffer` --
the primitive whose own doc comment says it exists "so two
path-normalization, dedup, and hook transactions cannot drift apart",
and which local startup had never been a caller of.
`resolve_target_buffer` returns a typed `ResolvedTarget` rather than
`(BufferId, HookKind)`, with a `Directory` arm checked ahead of the
load. Without it the load runs and fails: `File::open` succeeds on a
directory and `read_to_end` returns EISDIR, which is not `NotFound`, so
the `[new file]` arm never fired.
A directory creates no buffer. It dispatches a resolver chain: the
short-circuit `path.open-directory` hook, which no builtin subscribes
to, and then `pmacs.path.directory_handler`, which dired defaults. The
split is forced rather than chosen -- hook callbacks only append and
builtins load before init.lua, so a subscribing builtin would always
claim before any user listener could run. A raising listener stops the
chain and suppresses the fallback.
The listing is async and the daemon bootstrap is not, so the whole
post-await commit runs inside a new `pmacs.window.commit_to`: it
validates the destination -- frontend live, window live, buffer
unchanged, window replaceable -- BEFORE invoking its callback, then
scopes the acting frontend for its extent. Validating at display time
would be four dired mutations too late.
That scope is deliberately not `InteractiveCommandOrigin`, which does
not reach the core-ambient APIs and is authenticated user-command
authority a background continuation must not acquire.
The dedication rule is extracted into one `window_accepts_buffer`
shared by exact display, the display probe, and the new preflight, with
`incoming: Option<BufferId>` -- `None` means "the replacement does not
exist yet" and refuses a dedicated window.
`display_file` keeps its directory-is-an-error contract and does not
enter the chain; find-file's accept arm depends on it.
Framing: docs/journey-stage1a-framing.md rev 5 (Q#JR1-JR15).
Reconciles the handoff and ledger against a main that advanced past
this branch's base: the header, `main` anchor, and canonical-base
description take main's richer versions restamped to 74301d1, main's
new PTY-terminate lane is kept alongside the Lean lane, and main's
Stage 4a/rev-8 lane history is dropped in favour of the Stage 4b lane
that supersedes it — per this ledger's own rule to remove entries when
their PR merges.
Also fixes the coherence census's second count, which still said eight
settings three paragraphs below the nine it now lists.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Typing `\alpha` in a Lean 4 buffer gives `α`; `\<>` gives `⟨⟩` with the
point between them. The abbreviation table is vendored from
vscode-lean4 and the expander is a typed-edit consumer registered on
the Stage 4a chain at priority 50, ahead of auto-pairing.
The ordering is load-bearing. 64 abbreviation keys contain a character
in the `lean4` pair set, so with pairing first, typing `\[` would
insert `[]` and corrupt the pending key to `\[]` before the second `[`
arrives — `\[[]]` becomes unreachable. The consumer therefore claims
every keystroke that EXTENDS a pending abbreviation, not only one that
completes an expansion; claiming only completions would hand each
intermediate `[` to pairing by a different route.
The vendored table is an ORDERED SEQUENCE, not a map. Upstream breaks
equal-length ties by source declaration order — 101 prefixes depend on
it, and `\f` resolves through `f<` rather than `f>` — which a
`pairs`-iterated Lua table cannot express. `scripts/regen-lean-abbrev`
takes a vscode-lean4 commit, emits the file with its provenance header,
and aborts on a duplicate key, invalid UTF-8, or a round-trip mismatch.
Undo is cross-peer-degraded on CRDT frontends and that is accepted and
named, not papered over (Q#LN21): `\alpha` arrives as six source-peer
optimistic inserts while the expansion is one daemon-peer replace.
`set_round_trip_input` would fix it and also makes `dispatch_idle`
report false, so RET would stop inserting a newline.
Round 9 corrects three approved acceptance criteria that the real table
contradicts, found by simulating the state machine over all 1,855
entries and re-reading upstream at the pinned commit rather than
re-reading the prose. `\to` is not eager — `top`, `to0` and `toa`
extend it. `\zzzz` expands to `ζzzz ` because `ze`, `zeta` and
`zsqrtd` exist; only `$ % , ; @ W` open no key at all. And `\alpha`'s
undo does not restore `\alpha ` because `alpha` IS eager, so the
terminator is a separate edit. Criteria 38, 41 and 42 now state both
paths, and the false halves are asserted too: they read as correct
until the table is consulted.
Three implementation traps worth the record. The generator's own
round-trip check was broken twice and failed closed both times:
`str.splitlines()` splits on U+2028, which 53 symbols contain, and
escaping through `chr(byte)` produced a latin-1-shaped string that the
UTF-8 write re-encoded. The first check compared in-memory strings and
agreed with itself; it now stages the file, re-reads the bytes from
disk, and renames into place only on a match. And the expansion SHRINKS
the buffer, so the point must be placed explicitly — pairing's
no-cursor-motion rule holds only for an insert AT the cursor, and
without this every self-insert after the first expansion is silently
rejected and the editor looks dead.
25 acceptance tests plus one `--lib` test for the optimistic CRDT
producer (45f), which is where the gate list's `--features crdt` run
reaches it; a crdt-gated integration test would be dark in CI and in
the gates both. Fifteen mutations bite, each failing its target. Three
of these tests were vacuous when first written and biting is what
found them: the abandonment test asserted text a surviving record
would also produce, the re-arm test used an example that never reaches
the re-arm branch, and both switch tests ran through
`find_or_open`'s fresh-load path rather than `buffer.after-switch`.
No protocol change (Q#LN14). Also reconciles the handoff and ledger
for Stage 4a (#179) and adds `lean.abbrev` to COHERENCE.md's
config-registry adoption census, now nine settings.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Review round 3, on the round-2 primitive itself. One lesson covers all
three findings: a rope write is only half of an edit, and "discard
history" means whichever history the buffer actually has.
P1 — the binding swallowed the edit. `set_generated_contents` returned
`()`, so nothing reached `notify_buffer_edit_to_windows`. Two
consequences, both reproduced by the reviewer. In the default build a
window showing the buffer kept a `TextView` line index describing the
PREVIOUS contents, and the next paint indexed the new rope with stale
ranges — `assertion failed: end <= self.len()` in `src/rope.rs`. In the
CRDT build `pending_crdt_ops` stayed empty, so replica mirrors never
imported the owner's write and their optimistic edits were generated
against content already replaced. The `delete`+`insert` pair this
replaced had done that fan-out for free.
Now applies ONE whole-buffer `Replace`, returns its `Edit`, and notifies
from the binding. The doc comment states the obligation, because the
next owner to adopt the primitive inherits it.
P2 — "discard history" was false in CRDT mode. The v0.1 stacks are
bypassed entirely there; the history lives in loro's `UndoManager`.
`read_only` stops the replay but not the retention, which is the memory
cost the contract claims to eliminate. `UndoManager` exposes no clear,
but needs none: it records only what happens after it is constructed,
the same property `CrdtState::from_bytes` already uses to keep the seed
insert out of undo. `CrdtState::clear_undo_history` rebinds a fresh
manager to the same doc.
P2 — the docs described the pre-fix architecture. Q#TC6a said no Lua
binding sets `read_only` and round-trip input is the only guard; the
acceptance text still said `is_read_only() == false` while 16b had been
flipped to true; `terminal.lua`'s comment repeated the obsolete claim.
The architecture is layered and now says so: rope-level read-only
protects the daemon copy, round-trip input protects the replica's
optimistic mirror, and neither substitutes for the other. Q#TC6a keeps
its analysis under a superseded-in-part box rather than being silently
rewritten — its conclusion survives, two of its premises do not.
New pins. acc16d paints the window after a SHRINKING generated write:
stale offsets then point past the buffer end, so the failure is the
reported crash rather than merely stale pixels. acc16e asserts the
refresh is queued for mirrors, through the real copy-mode path;
`crdt`-gated and therefore dark in CI, which is why 16d drives the
binding rather than the terminal. Plus a CRDT unit test that ten renders
leave the `UndoManager` with nothing recorded.
Bites: dropping the notify panics acc16d at `rope.rs:145` and fails
acc16e with `queued: []`; dropping the `UndoManager` rebind fails the
new unit test on `can_undo`.
Still open, and recorded in COHERENCE.md §14: the fan-out obligation
makes `*compilation*`/listview adoption more than a one-line swap.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Five defects in the chain itself, plus the stale handoff state.
Each consumer now gets its own shallow copy of the typed-edit record.
Handing everyone the same table let a DECLINING consumer rewrite
provenance for the ones behind it, and pairing decides what to close
from `rec.char` — so a forged `char` turned a typed `x` into `x)`.
Every field is a scalar or an opaque id, so a shallow copy is complete.
The fan-out iterates a snapshot of the consumer list. It was iterating
the same array `add_consumer` mutates: a consumer that registered a
lower-priority one shifted itself forward under `ipairs` and ran twice,
and re-registering made that unbounded. Registrations and removals made
during a fan-out now take effect on the next one, stated as a contract
and pinned in both directions.
`tostring` on the caught error moved inside the containment. A Lua
error may be any value, including a table whose `__tostring` throws —
rendering it outside the `pcall` reintroduced exactly the escape the
containment exists to prevent.
Priorities are validated as finite integers in i32 range, matching
`pmacs.completion.register`. NaN is a number and every ordered
comparison with it is false, so a NaN consumer landed wherever the
insertion scan gave up and silently voided the lowest-first ordering
that Q#LN22 depends on.
`add_consumer` returns a handle and `remove_consumer` unregisters it,
reporting whether it was live. Without teardown the chain inherited the
`pmacs.hook.add` callback leak COHERENCE.md §13 already records, and
spread it to every consumer.
Also corrects the rationale the containment was documented with, in the
module, the test, and the framing: an uncontained throw does NOT take
the fan-out's other subscribers down. `run_all_must_succeed`
(src/hook.rs:332) collects errors and continues, so lsp.lua still
flushes didChange. The containment is still required — the throw skips
every later consumer in the chain — but the reason is narrower than
rev 7 claimed.
Criteria 46f (record isolation), 46g (snapshot iteration), and 46h
(lifecycle and priority validation) added; 46d's rationale corrected.
Four new tests, all bite-verified by mutation, each failing only its
target: shared record table (1), live-array iteration (1), unprotected
tostring (1), bare number check (1), no-op removal (2). The suite also
runs green under `--features lua54`.
docs/agent-handoff.md said Stage 4a was awaiting approval while this
branch had it implemented and in review.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Review round 2, P1. Undo could empty the "read-only" snapshot.
`render_snapshot` wrote with bypass_intercept, which leaves ordinary
undo history behind, and `Buffer::undo` reaches the rope through
`ensure_writable` without ever consulting the intercept chain. So a
single `C-/` — or `M-x buffer.undo`, which needs no keymap at all —
replaced a freshly rendered snapshot with an empty buffer.
`set_round_trip_input` does not help: it routes the key into the daemon
command path, which is exactly where undo runs.
Rebinding the undo chords buffer-locally would not have closed this,
and `compile.lua` already says so in a comment: "command/menu undo
stays dispatchable". `*compilation*` and listview panels therefore
carry the same latent defect today.
Adds `Buffer::set_generated_contents` (Lua:
`pmacs.buffer.set_generated_contents`): lift `read_only`, replace the
contents skipping intercepts, discard the resulting history, re-assert
`read_only`. This ships the framing's deferred immutability lane as ONE
primitive rather than exposing the setter — a bare `set_read_only`
would let a caller lock a buffer it can no longer refresh, which is
precisely why that lane was deferred. Discarding history is
load-bearing twice: it removes what undo would replay, and it stops a
periodically refreshed buffer accumulating rope clones that `read_only`
guarantees nothing can ever pop.
New acceptance 16c drives the real M-x path
(`command.invoke_interactive`), the chord, and redo, and asserts the
owner's own refresh still works — the operation plain `read_only` would
have broken. Acceptance 16b flips from asserting `is_read_only()` is
false to true, because the property it documented is the one that was
wrong. Three `buffer.rs` unit tests cover the primitive directly,
including that ten refreshes leave an empty undo stack.
Bite: restoring the delete+insert render reproduces the report exactly
— `left: Some("")` against the full snapshot — failing 16c and 16b.
Still open, and now named in the framing, COHERENCE.md §14 and the
ledger: `*compilation*` and listview have not adopted the primitive and
remain emptiable by `M-x buffer.undo`; a streaming-friendly variant is
needed for the append case. In CRDT mode `read_only` is what refuses
undo, since loro's UndoManager exposes no clear through `CrdtState`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
`pmacs.editor.take_typed_edit()` is one-shot and per-frontend (Q#AP9):
the first `buffer.after-edit` callback to call it clears the slot, and
every later callback in the same fan-out sees nil. That was survivable
only because auto-pairing was the sole consumer — never a property
anyone chose. A second independent caller would get nil or steal the
record from pairing depending on hook registration order, and
registration order is not a contract.
This makes it one. `builtin/runtime/typed_edit.lua` owns the single
after-edit subscriber that reads the record, and offers that one read to
consumers registered through `pmacs.typed_edit.add_consumer{ name,
priority, fn }`: lowest priority first, ties by registration order, and
the first consumer to return truthy claims the edit and stops the chain.
`pair.lua` becomes that chain's only consumer, at priority 100.
No Lean content. Stage 4b's abbreviation expander is what needs the
ordering guarantee (64 of its 1,855 keys contain a `lean4` pair-set
character, so pairing running first corrupts them), but the chain is
substrate every language runs through, which is why it ships alone —
framing Q#LN10, and §4's rule that no PR in this arc mixes a
cross-cutting substrate change with Lean feature content.
Three design points worth review attention:
- Consumers are called even when the record is nil. "This fan-out
carried no typed edit" is information a consumer acts on: it is how
pairing's test seam observes a non-event, and how Stage 4b will
abandon a pending abbreviation an unrelated edit invalidated. Three
existing auto-pairing tests fail if the chain skips consumers on nil.
- The chain pcalls each consumer. `buffer.after-edit` is
all-must-succeed, so a throwing consumer would otherwise fail the
fan-out for every other subscriber, including lsp.lua's didChange
flush. Behavior-preserving for pairing, which already never throws.
- Ordered insertion, not `table.sort`, which is not stable in Lua —
"ties by registration order" is a stated contract, not a coincidence.
`tests/auto_pair_acceptance.rs` is UNCHANGED — zero lines — and its 45
tests pass. That is criterion 46 and the whole no-behavior-change claim;
a suite edited to accommodate the refactor would prove nothing.
`tests/typed_edit_chain_acceptance.rs` adds 9 tests for criteria
46a-46e. Every one is bite-verified by mutation: appending instead of
ordered insert (5 fail), `>=` for the tiebreak (1), re-taking per
consumer (4), ignoring the claim (1), dropping the pcall (1), skipping
nil fan-outs (1 here plus 3 in the untouched auto-pair suite), and
loading the chain after lsp.lua (the Q#AP7 flush test fails, alongside
the two existing pairing ones).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
Four findings, all real, and they rhyme in pairs. Two implementation
defects and two vacuous pins, all four tracing to one root: a name is
not an identity, and a context-free readout is not a state observation.
A foreign buffer carrying the snapshot's name was adopted and then
overwritten. `pmacs.buffer.create` accepts any caller-chosen name and
snapshot writes use bypass_intercept, so found-by-name adoption
clobbered user data — the reviewer reproduced "do not clobber" becoming
23 newlines. Now follows dired's F7 rule: ownership means "in copy
mode's own handle table", never "found by name", and a taken name yields
a `<2>` variant.
Snapshot identity was keyed by terminal NAME.
`TerminalManager::open` uniquifies only the derived name — an explicit
`name = ...` is inserted verbatim — so two valid terminals can share
one, and a name-keyed table handed them a single snapshot: the second
invocation retargeted it, `q` returned to the wrong terminal, and
killing either removed the shared buffer. Identity is now the terminal
buffer, compared in an array, because BufferIdLua implements `__eq` but
each wrapper is a distinct table key: comparison works, hashing does
not. The kill-with-terminal callback now closes over its own record
rather than looking the name up again.
The refresh pins were vacuous. Acceptance 19 compared a quiet
terminal's snapshot against itself and 18 counted buffers, so both
passed with render_snapshot replaced by a no-op. The child is
`exec cat`, so the tests now type a marker into the focused terminal,
require it ABSENT from the existing snapshot, and only then refresh —
via `g` and via re-invocation respectively.
The tail-follow pin could not observe view state.
`TerminalManager::snapshot(buffer_id)` is context-free and always
returns the live screen, so it reported "at the tail" even for a view
forced to the oldest retained row. Now read through
`snapshot_for_view`'s at_bottom and its projected cells.
Adds acceptance 18a (a foreign same-named buffer is never adopted or
clobbered) and 18b (two same-named terminals get two independent
snapshots, each `q` returns to its own source, and killing one leaves
the other's snapshot alive).
Four new 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, which is the vacuity
demonstrated rather than argued; and forcing the view off the tail
fails 20.
Criterion 17 stays a named follow-up, per review agreement, until the
real GPU probe is non-skipping and CI-executed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Stage 2 of docs/terminal-config-and-copy-mode-framing.md (rev 4,
approved). `M-x terminal.copy-mode`, or `C-t` in a terminal buffer —
physically `C-c C-t`, since every unescaped key goes to the child —
materializes the retained scrollback into an ordinary read-only,
path-less buffer, with `g` to re-snapshot and `q` to return.
No protocol change.
Materializing is the whole design. isearch, motion, selection and the
kill ring work with no new substrate because the snapshot is a rope, so
SearchStore and the existing match painting apply unchanged. And "keys
must not reach the child" dissolves structurally rather than being
guarded: the transport arm keys on is_terminal(buffer_id), and a
snapshot is not a terminal, so the arm never fires. The
dispatch-shadow count stays at six and describe-key keeps telling the
truth — asserted directly, since that is the observable difference
between the buffer-local idiom and a shadow.
One serializer, not two (Q#TC7). `copy_retained` builds a whole-range
selection and hands it to `copy_selection_bytes`; a second walk would
re-derive soft-wrap joining, wide-glyph continuation, cluster bytes and
per-row trailing-blank trimming, and the two would drift. Four unit
pins in view.rs assert exact bytes against the same projection fixtures
that pin the serializer itself.
Q#TC6a is implemented as two calls, and the second is the load-bearing
one: an intercept guards dispatch only, and no Lua binding sets
Buffer::read_only, so set_round_trip_input is what keeps a replica
frontend from applying optimistically and emitting an op that would
pass ensure_writable and mutate both sides. Acceptance 16 pins that
UNGATED, because CI never compiles the crdt feature.
Eight of nine criteria. Criterion 17's semantic-frontend end-to-end pin
is deliberately absent: the optimistic apply lives only in
pmacs-gpu/src/main.rs and the headless SemanticClient has no optimistic
path, so a faithful test needs the real GPU binary — the a37
foundation, which CI never compiles, silently returns ok when the
binary is unbuilt, and is load-sensitive. Both halves of the mechanism
are pinned ungated instead (16, and 16b for the hazard); the wire-level
half stays an explicit obligation of the CI crdt-coverage lane.
Substrate fact found while wiring lifecycle: TerminalManager::prune
REACTS to a buffer already gone from the registry rather than removing
one, so a child exiting leaves both the terminal and its snapshot
alive. 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, each failing exactly
one test: removing set_round_trip_input fails acceptance 16 in the
DEFAULT configuration; a naive independent serializer fails all four
unit pins, with the diffs naming each drift mode; making re-invoke
create a fresh buffer fails 18; dropping the kill-with-terminal
teardown fails 18; removing the intercept fails 16b.
COHERENCE.md: §6 gains this as the worked example that a modal-looking
feature need not become a shadow; §11 records the scope="global"
deferral's second live case, making the argument for both registry
deferrals cumulative; §2 step 8 gains copy mode and keeps the
still-missing close command named.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Make command-time attachment healing cancel an armed terminal restart
before replacing the server, while keeping request-only lookup pure and
restart-safe.
Track config-driven server ownership privately, bound every fallback
server per SID, scope no-swap retirement to the failed root, and route
the shipped Lean diagnostics command through the safe resolver while
waiting for initialization.
Add direct acceptance counterexamples for all five review findings and
record the sixth-round verification and vacuity lesson.
Five findings, all real. The blocker and both majors are the same
mistake in three places: a claim asserted somewhere cheaper than where
it actually lives.
COHERENCE.md was stale in four places, not the three reported. Step 8
still read "no keybinding" and §11 still read "five settings", but §6's
dispatch table also still cited `is_terminal_escape_chord` — a symbol
this branch deletes. §25 requires that update to ride the PR, so a PR
changing audited ground truth has to re-grep the audit for its own
symbols, not only for its topic.
Acceptance 5 asserted a registry round-trip, which is a test of the
registry: 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.
Acceptance 8a waited for the session count to fall, which the rejected
editor-side cache map satisfies exactly — a map with no purge hook
leaks while sessions drain. Adds `TerminalManager::escape_caches()`, the
lifetime half of Q#TC4c's contract that `escape_parses` cannot cover.
`table.sort` over `pmacs.terminal.profiles` raised "attempt to compare
number with string" on the unknown-profile path whenever the user's
table held both a string and a numeric key, replacing the exact
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.
Also corrects the framing's status line, and a status message whose
embedded whitespace run had survived a rustfmt reflow.
Three new bites, each falsified by revert: deleting the scrollback
consumer fails acc5 and only acc5; restoring the raw-key sort
reproduces the comparison error verbatim; and implementing the rejected
map fails the new acc8a at left: 2, right: 1 while passing the old
session-count version.
Merges githubsucks/main @ ccf29e3.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gGQC6eqHJVbZJ5Hg7aLer
Round 5 review: one P1, a frontend scope hole, and three P2s.
**1. A fallback that SPAWNS and then dies retried forever.** The
once-per-buffer guard bounds calls to `_attach_buffer`, not the server
those calls produce. `ensure_server` still never forwards `cfg.restart`,
so the fallback inherits `OnCrash`; an executable that exits before
`initialize` is respawned by the manager with no attempt ceiling —
silently, because `latched` has already disabled the primary's failure
poll. The fallback now gets its own one-shot die-before-initialize
watch, which retires it (ending the respawn loop) and reports.
The prior failing-fallback test used a NONEXISTENT executable, so it
only ever exercised synchronous ENOENT. To reach "spawned, then died"
the fixture has to actually spawn.
**2. Simultaneous frontends.** Both repair triggers read the ambient
`pmacs.window.buffer()`, and the daemon restores `active_frontend` to
the last-dispatched frontend before `tick_processes` — so a Lean buffer
active in ANOTHER frontend receives no `buffer.after-switch` here and
stays stale after its server is globally retired.
Fixed at the seam that is frontend-agnostic: **make consumption safe.**
`attached_for_active` now rebuilds rather than returning a record whose
server is dead, and `attachment_for_request` reports none (it must not
perturb LSP state, so it cannot rebuild). Whichever frontend runs a
command is the active one while it runs, so healing at the point of use
reaches every buffer no eager sweep can. This also closes the half where
a dead attachment was handed to a command and the request vanished.
**3. The retirement sweep stopped user-managed servers.** Selecting on
`language_id == "lean4"` also names servers the user spawned from
`init.lua`, which are not derived from `pmacs.lsp.config.lean4`. It now
keys on the `default-lean4` label `ensure_server` stamps — the
derivation discriminator.
**4. Repair ran even when no swap occurred.** `swap_to_fallback()`
returning false left `latched` true, so the next tick retried the
UNCHANGED configuration and reported it as a fallback failure. Split
into `probe.fallback_installed`: repair exists to apply a swap, so no
swap means nothing to apply.
**5. The once-per-buffer assertion counted table keys**, which cannot
distinguish "once per buffer" from "every tick for one buffer" —
cardinality stays 1 either way. Replaced with a numeric attempt counter;
the bite reports 174 attempts against the expected 1.
Five bites, each against 7c37bdc: no fallback watch -> attempt reaches
4; retire by language_id -> the user's server is stopped; gate repair on
`latched` -> a repair is attempted with no swap; drop the
once-per-buffer guard -> 174 vs 1; hand back a dead attachment -> a
command receives a `stopped` server.
Two more vacuity shapes recorded in the ledger (8 and 9): counting
distinct keys cannot bound repeated work, and a nonexistent executable
cannot reach any post-spawn failure.
Round 4 review: one P1, and it is the same defect for the FOURTH time.
`pmacs.lsp.config.lean4` is a single global entry, so swapping its
command invalidates **every** Lean buffer and **every** Lean server —
Q#LN15 gives one server per project root, so there can be several.
Rounds 1-3 each repaired one buffer and retired one server, and round 3
shipped "repair the armed target, strand the rest": status and config
said fallback while a second open Lean buffer stayed on the retired
command, and a second project root's server stayed live.
The shape that actually holds:
* **Retire ALL `lean4` servers on latch**, not the one the probe
happened to name. `probe.primary` identifies the server the VERDICT
is about; it was never the set of servers the swap invalidates.
* **Repair each buffer lazily and at most once**, when it becomes
active — on `buffer.after-switch` and on the tick. `_attach_buffer`
is an active-buffer-only seam, so a global swap cannot be applied to
every open buffer at once; it has to be applied as they surface.
lsp.lua's own `after-switch` re-pushes views but does not rebuild a
stale attachment, so nothing else covered this.
* The **once-per-buffer bound** is load-bearing: without it a fallback
that also fails to spawn would retry every tick forever — the
round-2 defect, which a naive global repair loop would reintroduce
for every buffer instead of just one.
* `shutting-down` is deliberately not treated as stale. It is still
live by `server_is_live`'s reckoning, so attaching would early-return
the stale record and burn that buffer's single attempt on a no-op.
P2: argument-inclusive attribution was implemented in round 3 but pinned
only by "contains the command name", so a mutation dropping every
argument passed. Now asserted against the exact `<command> <args>`
string.
Also fixed a vacuous assertion this refactor created: a test checked
`_probe.reattach_from == nil` for a field that no longer exists, which
reads as nil and passes for nothing. It now asserts a positive count of
recorded repair attempts.
Three bites, each against 73587b0: repair only the armed buffer -> the
second buffer stays on `lake`; retire only the named server -> one live
stale server remains; drop arguments from attribution -> the exact-string
assertion fails.
The ledger records a second durable lesson beside the vacuity one: **a
scope error repeats until the scope is named.** Four rounds of locally
correct fixes, none of which asked what the config swap invalidates.
When a change edits shared state, enumerate everything derived from it
before repairing anything.
Round 3 review: two P1 asynchronous-correlation defects, with the
focused suite at 25/25 while both were live.
**1. A late version verdict retired nothing and claimed success.**
`probe.watching` is cleared the moment the server initializes — it is
failure-polling state. A slow `lake --version` landing after a
successful initialize therefore reached `fire_latch(nil)`, which retires
nothing: `_attach_buffer` found the still-live primary attachment,
early-returned it, and the retry counted that as done. Status said
"falling back", the config named the fallback, and the buffer stayed on
the old server.
**That is the round-1 silent no-op arriving through a third event
ordering** — first as "no re-attach at all", then as "re-attach cleared
by an unrelated buffer", now as "re-attach satisfied by the server we
were supposed to replace". The fix separates the two facts that were
being carried by one field: `probe.primary` is the server the verdict
applies to and survives initialization; `probe.watching` is the
failure poll and is cleared by it.
The existing fixture could not reach this ordering at all — its `serve`
sleeps, so the primary can never initialize before `--version` returns.
The new one execs the fake LSP for `serve` and delays 0.6s before
reporting 3.0.0.
**2. `buf_key` was the most recently loaded Lean buffer.** Written on
every Lean `buffer.after-load`, so a second Lean file opened before the
verdict became the rebuild target while the latch still watched the
FIRST buffer's server. Target buffer and primary server are one fact and
are now armed together, exactly once. Both files in the new test share a
package, so mis-targeting shows up as a stranded buffer rather than as
two unrelated servers.
**3. The failure message hardcoded `lake serve`** after the latch became
command-agnostic, telling a user whose `my-lean-wrapper` failed to go
debug lake. `configured_command()` names what is actually configured,
arguments included.
**4. The ledger** now records all fifteen bites across the three rounds,
both prior review rounds' findings (the round-2 block was lost when an
earlier edit script aborted before writing), and the durable lesson.
That lesson, recorded for the handoff: **six tests across three rounds
were written, ran green, and pinned nothing** — caught only by biting.
The shapes are enumerated in the ledger; the rule is that a test is not
evidence until the mutation it targets has been shown to fail it. Two
of the six are subtle enough to be worth naming here: a bite that
RAISES is swallowed by the hook's pcall and "passes" for the wrong
reason, and a fixture whose `serve` sleeps cannot reach any ordering
where the primary comes up first.
Stage 1 of the terminal config/copy-mode arc. The terminal had no
configuration surface at all: the command hardcoded $SHELL, scrollback
was a per-open argument only, and the escape chord was a literal in
Rust. No protocol change.
Profiles are a raw Lua table, pmacs.terminal.profiles, not a registry
setting: ConfigValue is four scalars with no table kind, so profiles
join pmacs.lsp.config and pmacs.pair.sets until table-valued settings
exist. The registry gains three scalars whose defaults reproduce the
previous behavior exactly.
Field resolution is explicit open argument, then profile field, then
scalar setting, then $SHELL. env MERGES, with explicit entries
overriding the profile's, because first-wins there would silently drop
half a user's environment. An explicitly named profile that does not
exist is an error even when terminal.default-profile is valid, so a typo
cannot silently fall back.
The two open-time settings resolve through the GLOBAL chain, because
they are read before the identity buffer exists and no caller could have
pinned a local override on a buffer that does not yet exist. Only
terminal.escape-key resolves per buffer, which makes a per-terminal
escape a supported feature.
The escape key is parsed at most once per (terminal, config epoch), and
the cache lives on TerminalSession so its lifetime is the terminal's,
with no purge hook to forget. The epoch alone is not a sufficient key:
it does not advance when focus moves between two terminals with
different buffer-local values, so an epoch-only cache serves one
terminal's chord to the other. An unparseable value falls back to C-c
and reports once per terminal per effective invalid value through the
status line, because a terminal with no escape chord cannot be escaped
to fix the setting that broke it.
Repeating the escape now sends THAT chord to the child through the
ordinary key encoder, rather than a hardcoded ETX. With an escape of
C-x, the previous code sent Ctrl-C and made literal Ctrl-X unreachable.
C-c t opens a terminal. COHERENCE Priority 1 names a terminal
keybinding, and section 2 step 8 grades the terminal works-but-
undiscoverable; C-c is already a live global prefix, so this is a new
leaf rather than a shadow. It is unreachable from inside a terminal,
where C-c is the escape.
Acceptance is tests/terminal_config_acceptance.rs, deliberately NOT
crdt-gated so CI actually runs it. Four bites, each against a different
plausible wrong implementation: a hardcoded ETX fails acc6/9; an
epoch-only cache key fails acc7; a single last-entry cache fails acc8's
parse count; removing the invalid-value fallback fails acc10.
Two test-instrument notes worth keeping. cat -v is the echo probe
because the screen rejects C0 controls before they reach cells, so a raw
echoed Ctrl-X would be invisible. And the probe counts occurrences
rather than testing presence, because a single-character probe collides
with the child's own banner text.
Three P1 lifecycle defects and two P2s. The focused suite was 20/20 with
every one of them live, which is the part worth keeping.
**1. The crashed primary respawned forever underneath the fallback.**
Round 2 skipped the retire call for terminal servers to avoid corrupting
them — but the crash had already armed `next_restart_at`, and
`maybe_restart` fires on every elapsed backoff with no attempt ceiling.
The broken command kept respawning under the live fallback.
The right call depends on the state, and each is wrong for the other:
`forget` REQUIRES a terminal state and removes the client outright,
which also drops the restart timer; `stop` is for a live one and
corrupts a terminal one (its not-initialized branch parks it in
`ShuttingDown` forever). `retire_server` now dispatches on state.
**2. Re-attachment targeted whatever buffer was active when the
asynchronous verdict landed.** `_attach_buffer` is an active-buffer-only
seam, and "some attachment now names a different server" is satisfied by
an unrelated Rust buffer — clearing the retry and leaving the Lean buffer
stale forever. The initiating buffer is now captured and the retry waits
for it.
**3. A failing fallback retried every tick forever, silently**,
contradicting acceptance 27's promise that a second failure surfaces.
"Waiting for the old server to go" and "attempting the replacement" are
now separate: once the old one is terminal or gone, the replacement is
attempted EXACTLY once, and a spawn failure is reported.
**4. The Lake version parser was being applied to arbitrary wrappers.**
`version_below_3_1` encodes lake's output contract; a working
`my-lean-wrapper` reporting "wrapper 1.0" would have been replaced
despite its server initializing fine. The version probe is now gated on
the command's basename being `lake`. The FAILURE latch stays
command-agnostic — that one keys on the server actually not starting,
which is true of any command.
**5. An unconfigured Lean server was reported as a failure** and latched,
poisoning the session so a later configuration could never take effect.
Absent config or command now means disabled; only a configured command
that produced no attachment is a failure.
**6. The ledger recorded pre-fix counts** after the fixes were pushed.
Now 25/25 and 3,214. That is the #161 fmt-blocker error in a slower
form: verification must describe the pushed tree.
Sign-offs requested in review: `M.fallback` is now `M._fallback`, an
underscored test seam, and its idempotence check compares args as well as
command — the same command with different arguments is not "already
applied". Dropping the `command ~= "lake"` guard stands for the failure
latch only.
Five regression tests added, and **three of them were too weak on first
write; only bite-testing found it**:
* asserting "no live non-fallback server" misses a respawn loop,
because a respawning server sits in `crashed` most of the time —
`attempt` is the observable that counts respawns;
* returning to a buffer with `find_or_open` re-fires
`buffer.after-load`, which repairs the attachment regardless of the
code under test — `switch_buffer` is the honest return;
* a MISSING command fails synchronously inside `after-load` where the
rebuild happens inline, so the async race cannot occur — only the
probe path exercises it.
Each of the five now fails against the exact round-2 mutation it targets.
Round 1 review, four P1s. All real; the first two mean the fallback did
not work at all.
**1. The latch swapped the config but never spawned or re-attached.**
Nothing re-fires an attach on a config change and `attach_buffer`
early-returns for a live attachment, so the buffer stayed bound to the
server that had just been stopped. The user got a config edit and no
language server. `fire_latch` now rebuilds through a new
`pmacs.lsp._attach_buffer` export.
Two mechanics had to be right for that rebuild to happen at all:
* It is **retried on the tick**, because `pmacs.lsp.stop` leaves the
state `shutting-down`, which `server_is_live` counts as LIVE — an
inline re-attach early-returns the stale record and the swap is a
silent no-op.
* The latch **does not stop an already-terminal server**, and this is
a substrate bug worked around rather than a style choice.
`LspManager::stop` on a `Crashed` client takes its not-initialized
branch, terminates the dead process, and sets `ShuttingDown { ..
None }` on the premise that "the next exit observation cleans up" —
but the exit already happened, which is what made it `Crashed`. No
further event arrives, so the client is stuck in `ShuttingDown`
forever: `server_is_live` reads it as live so `attach_buffer` never
rebuilds, and `forget` refuses it for not being terminal. Stopping a
dead server is what makes it un-replaceable. Named in framing §6; the
fix belongs in `stop` and changes behavior for every language.
**2. A missing `lake` bypassed probe and latch entirely** — the single
most likely real failure. `ensure_server` swallows a synchronous ENOENT
and returns nil, so there was no attachment, and the hook keyed on
`active_attachment()` returned before arming anything. The hook now keys
on the buffer's LANGUAGE and treats a Lean buffer with no attachment as
the failure itself.
**3. `waitForDiagnostics` omitted `version`.** Lean's
`WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0,
`src/Lean/Data/Lsp/Extra.lean`); the request is how a client says which
revision it wants. It looked correct only because the fake server echoes
any payload — so the fake server now validates and returns InvalidParams
without it.
**4. The ledger stated the dangerous stacking order** in one sentence
and the correct rule in the next. Fixed to say BEFORE. A safety rule
written twice with opposite senses is worse than not written.
Also (P2): the probe/latch suite now drives the production path —
`buffer.after-load` -> ticks -> probe drain -> latch -> re-attach — with
real executable stubs, and asserts the originally opened buffer ends up
on a LIVE server. Round 1's acceptance 36 asserted every server was
terminal, i.e. pinned the ABSENCE of the fallback it claimed to test.
`M.fallback` is a table so the suite can point it at a working stand-in;
the probe now spawns `cfg.command --version` rather than a hardcoded
`lake`, which is also more correct for a user who configured a wrapper.
`swap_to_fallback`'s `command ~= "lake"` guard is gone: the latch fires
only when the configured server actually failed, one visible fallback
beats no server, and `probe.latched` is what keeps it to exactly one.
Three new bites, all against the committed tree: no re-attach after the
swap -> three latch tests fail; hook keyed on the attachment -> the
missing-`lake` case fails; `waitForDiagnostics` without `version` ->
acc37 fails with the server's InvalidParams.
Framing Q#LN7, Q#LN8, Q#LN16; acceptance 22–28, 24a/24b, 35, 36, 36a, 37.
Stacked on Stage 3a (#167), whose notification/response seams and
`pmacs.fs.canonicalize` this consumes. No protocol change; the only Rust
outside the test helper is one `include_str!` line.
**The Lake-aware root (Q#LN8).** `pmacs.project.detect` cannot express
this rule — it is innermost-wins by construction, and a Lake package's
`lean-toolchain` sits at the outermost level, so a file under
`<pkg>/.lake/packages/dep/` belongs to `<pkg>`'s server rather than
`dep`'s. The resolver walks up collecting markers and returns the
outermost, stopping at `pmacs.project.search_boundary()` so a stray
marker above a fixture cannot leak in.
Two things about the marker test are easy to get wrong in opposite
directions, and both are pinned. `io.open` **succeeds on a directory**,
so a truthiness check accepts a `lean-toolchain` directory; but
requiring a non-nil read rejects an **empty** `lean-toolchain`, which is
a legitimate marker — `locate-dominating-file` semantics are existence,
not content. The discriminator is `read`'s second return: decline only
on a non-nil error. Acceptance 24a and 24b each fail against the
implementation that satisfies only the other; both bites are recorded.
The root is canonicalized once up front, because a configured root
reaches `file_uri_for` verbatim and that URI is the affinity key (#161).
Canonicalizing the starting directory suffices — every ancestor of a
canonical path is canonical, since the walk only strips components.
**`lake serve` with a lazy probe and a one-shot latch (Q#LN7).** Nothing
runs at init: `pmacs.lsp.config` is declarative, and spawning a process
at startup for every user, Lean-using or not, is the cost rev 1 refused.
Both the probe and the server spawn are gated on a real Lean attachment.
The probe cannot gate the first attach — there is no blocking process
run, so its verdict arrives after `ensure_server` has already decided.
Hence the optimistic spawn, with the probe and latch correcting it. A
non-zero probe exit is deliberately NOT a trigger: §2.9's elan-shim case
makes `lake --version` fail on machines where `lake serve` still works,
and the server-failure latch covers that better. The probe answers only
the question failure detection would answer slowly — an old-but-working
lake that starts a useless server.
The latch stops the failing server **before** spawning the fallback, and
that ordering is load-bearing rather than defensive: the spec default is
`OnCrash`, the termination handler never consults the exit code, and
`maybe_restart` has no attempt ceiling, so a broken `lake` respawns
forever underneath the latch. `pmacs.lsp.stop` sets `restart = Never`,
which is what disarms it. Bitten: removing the stop fails acceptance 36.
The swap rewrites `command` and `args` only, so a user's `env`,
`settings`, `init_options` and `root` survive — a wholesale table
replacement would discard their `init.lua` at the moment they are least
likely to notice.
**`waitForDiagnostics` (Q#LN16)** resolves through Stage 3a's response
seam, with `M-x lean.wait-for-diagnostics` on top. `$/lean/fileProgress`
subscribes on the notification seam and is pinned end-to-end through a
new `leanprogress` mode on the fake server rather than by calling the
handler directly — the wiring is the only part that can break.
**Attribution (COHERENCE §9/§1.2).** The probe spawns as
`lean:lake-version-probe`, so a user wondering why their editor touched
`lake` finds an owner in `pmacs.process.list`. The latch reports through
`pmacs.editor.set_status` — the channel that exists — and acceptance 36a
observes that channel, so a report made only through the undefined
`pmacs.error` would fail it.
**Stage 1's acceptance 12 is updated, half superseded.** It asserted
`pmacs.lsp.config.lean4 == nil` to guard against a Stage-3 front-run;
Stage 3b is that stage, so keeping it would pin the opposite of the
intended behavior. The half that survives is the one about restraint,
and it matters more now: constructing an editor spawns nothing even
though the config exists and names `lake`, and opening a Lean buffer
with no server configured spawns nothing either. That is what holds
Q#LN7's "not at init" promise.
Bites recorded, all against the committed tree: bare `io.open` -> 24a
fails, 24b passes; require-non-nil-read -> 24b fails, 24a passes; no
canonicalization -> the symlink case spawns two servers; no stop before
fallback -> acceptance 36 fails.
Six findings from review, one of them a real defect.
**`canonicalize` could emit a path that exists nowhere.**
`p.display().to_string()` substitutes U+FFFD for non-UTF-8 bytes, so a
resolution landing on such a path returned a plausible-looking string
that does not exist on disk — worse than nil, because this value becomes
a server-affinity key through `file_uri_for` and would silently fail to
round-trip, while the doc promised nil for anything unresolvable. Now
`.and_then(|p| p.to_str().map(str::to_owned))`: unrepresentable is a
decline, matching how the fs layer already treats non-UTF-8 symlink
targets.
Pinned by a new acceptance case that reaches a non-UTF-8 target through
an **ASCII** symlink, so the input is representable and only the
resolved output is not — the case a UTF-8 check on the argument would
miss. Bitten: restoring `display()` fails it.
The other five:
- `on_response`'s doc comment now warns that registering against a
server with no attached buffer is fire-on-death, not fire-on-reply,
because the drain visits only attached sids. It looks exactly like a
hung request while debugging, and 3b is the first caller likely to
hit it.
- `deliver_response`'s comment still carried the pre-correction
rationale ("removed BEFORE invocation ... must not be re-entered") —
the claim the bite disproved. It now says what is true: removal is
unconditional, before-vs-after is unobservable without a re-entrant
drain, and the reachable bug is gating removal on a clean return.
- Dropped `server_attempt`'s unused second return.
- Deleted a vacuous assertion in the no-attachment test (counting `_G`
entries to assert "lua globals are readable") — scaffolding that
pinned nothing, the exact shape the project's own lesson flags.
- `#[cfg(unix)]` on the three symlink-dependent tests.
Gates re-run in full. The sweep's first pass tripped
`composition_overhead_under_ten_percent` at 18.8% against a 10% budget;
it passes 3/3 in isolation here, passes in isolation on main, and the
same run reported the realistic-frame overhead as **-4.6%** — a negative
figure is measurement noise, not added work. Nothing in this diff is on
the render path. Rerun of the full sweep: 3,189 across 93 suites, zero
failures.
The module doc said an uncaught raise inside a `pmacs.async` coroutine
"goes to *errors*, not the status line". #161's COHERENCE finding shows
that is wrong, and in the worse direction: `pmacs.error` is never
defined in production, so `step()`'s guarded report is dead and the raise
falls through to a bare `error()` inside `pmacs._async.tick()` -- whose
result `EditorState::tick_async` discards with `let _ =`. The failure
reaches nowhere at all, and dired would look like it silently did
nothing.
So the per-coroutine `pcall` plus `pmacs.editor.set_status` is
load-bearing, not tidy, and the doc now says which channel is dead, which
is live, and that the acceptance suite observes the live one -- the
corollary COHERENCE draws from that finding.
The ledger records the integration, the reruns on the merged tree, and
the ops lesson that cost three CI runs: a conflicting PR has no merge
ref, so GitHub creates no `pull_request` run and nothing reports the
absence.
Multi-root LSP affinity merged as #161 (`main` @ `46a1b8f`) while this
lane was in review, which made the PR conflict -- and a conflicting PR
has no merge ref, so GitHub silently stopped running CI on it after the
first push. Integrating rather than rebasing, per the #135/#137
precedent: the review anchors stay addressable and every gate is rerun
against the merged tree.
One conflict, in COHERENCE.md's in-flight list, resolved as the union of
both truths -- and #161 is now merged, which its own text still called a
PR.
The overlap to watch is `src/lua_bindings/mod.rs`: #161 widened the
`lsp.list()` row builder while this lane added `pmacs.path` and the
read_dir listing conversion. The merge was textually clean, which the
folding arc's lesson says is not the same as compiling, so the full gate
suite reruns from here.
Two corrections found by bite-testing the suite rather than by reading
it.
**Acceptance 32 was mis-named.** It claimed to pin "the one-shot is
removed BEFORE invocation". Biting that — moving the removal after the
`pcall` — still passes, because `pcall` catches the raise either way and
the removal runs regardless. The before/after ordering is unobservable
unless a handler re-enters the drain, and nothing does. What the test
actually pins is that removal is **unconditional**: the bite that gates
it on `if ok then` fails 2 != 1, because the surviving registration is
invoked a second time by the purge. Renamed and re-commented to say so.
The implementation still removes before invoking, which is the right
defensive order; it is simply not what the assertion proves.
**The purge's generation check is defensive and untested**, now labelled
in place instead of reading as covered. Reaching it needs a crash and
its restart to both land in a gap with no `_async.tick`; the backoff is
500ms, so any tick in that window sees `crashed` and the
absent-or-terminal test fires first. Every attempt to stage it
deterministically exercised the `crashed` path instead. It stays as
insurance for a stalled editor, and says that about itself.
Bites recorded, all against the committed tree:
- removal gated on a clean return -> acc32 fails (2 != 1).
- purge driven by a `crashed`/`stopped` event seen in the drain, the
design the framing originally implied -> the no-attachment case fails
("never called"), while the attached case still passes. That is the
discrimination acceptance 34's second half exists for.
- a resolver without `pmacs.fs.canonicalize` -> two servers, pinned as
34b's own falsification.
Arc 8 Stage 3a (framing Q#LN9, Q#LN20). No Lean content: this changes
the event drain every LSP language runs through, and is split from the
Lean server work for the reason Stage 2 was.
**The seams.** `handle_server_requests` handled five `request` methods
and `initialized`, dropping every `notification` and `response` on the
floor. Dropping responses made `pmacs.lsp.send_request` a write-only API
from Lua — the reply was drained and discarded, so nothing outside
Rust's typed stores could consume one. Two new arms route to
`pmacs.lsp.on_notification(method, fn)` (persistent, method-keyed) and
`pmacs.lsp.on_response(sid, request_id, fn)` (one-shot). Both extend the
existing loop rather than opening a second `events_take` caller, which
would steal events from it.
A one-shot is removed **before** invocation, so a raising handler cannot
be re-entered. Every subscriber is `pcall`ed and a raise reports through
`pmacs.editor.set_status` per COHERENCE §1.2 — not `pmacs.error`, which
is defined nowhere in production. The notification list's length is
captured before the walk so a subscriber registering another cannot
extend the list being iterated.
**The purge is driven off `pmacs.lsp.list()`, not off a death event.**
The framing said acceptance 34's second edge was a killed buffer. That
was wrong, and scouting the implementation is what caught it: pmacs
fires exactly five hooks (`buffer.after-edit`, `buffer.after-load`,
`buffer.after-switch`, `frontend.detached`, `process.after-tick`) and
there is no buffer-kill hook at all, so `lsp.lua` never tears an
attachment down and the drain keeps reaching that server. No leak there.
The real leak is a different path with the same root cause. The drain
builds its sid list from `attachments`, and `attach_buffer` drops a sid
from that table the moment `server_is_live` reports false — rebuilding
against a fresh server. So the `crashed` / `stopped` event that should
trigger the purge is precisely the one most likely to go undrained. A
purge wired to that event leaks exactly when it matters.
`pmacs.lsp.list()` enumerates the manager directly and is unaffected by
attachment bookkeeping, so the purge polls it after each drain: a sid
that is absent, terminal, or running a **new generation** settles its
pending one-shots with an error. The generation check uses the `attempt`
field, because a crash-then-restart reuses the sid — without it a
one-shot would sit waiting on a reply the dead generation owed.
**`pmacs.fs.canonicalize`** (Q#LN20) is the one synchronous function on
`pmacs.fs`, and synchronous is the point: its consumer is a
function-valued `config.root` called from `ensure_server` <-
`attach_buffer` <- `buffer.after-load`, where there is no coroutine and
`pmacs.fs.stat`'s awaitable handle is unusable. It is installed from
`install_async` rather than `install_project` purely for load order —
`make_workspace` runs after `fs.lua` is evaluated, so a canonicalizer
placed there reads nil.
Acceptance: `tests/lsp_dispatch_seams_acceptance.rs`, 14 tests, driven
against `pmacs_fake_lsp` through rust so nothing needs a toolchain.
Dispatch integrity is exercised at real co-occurrence — the fake server
writes `workspace/applyEdit` and the `executeCommand` reply back to
back, so both land in one `events_take` batch. 34b asserts affinity
survives a symlinked open and is paired with its own falsification: the
same resolver minus the canonicalize call spawns two servers, so the
positive case cannot be vacuous.
F1 (real, small-window misbehavior). `dired.revert`'s re-seat runs after
the read settles, and `pmacs.editor.move_to_line` is AMBIENT -- it moves
whatever window is active. A user who switched buffers (or hit `q`)
while the re-read was in flight had an unrelated buffer's cursor moved
to a line index that only means something in the dired listing. The
paint was already safe because it names its buffer; the seat now runs
only while dired is still the active buffer, and `seat_cursor`'s doc
says which callers are unconditionally in the right place and why.
Pinned by a test that starts the revert, switches to a six-line file
before the pump, and asserts that buffer's cursor never moved -- and
that the dired buffer still reverts when it IS active.
F2 (a trap set for Stage 3). `fmt_size` used `%10d`, so a size past ten
digits -- 10 GB and up, ordinary for VM images and core dumps -- widened
the field and shifted mtime and name right on that line alone. Cosmetic
today, but `_layout` is exported as a contract and Stage 3's
column-classifying intercept is planned against it. It now takes
`fmt_mtime`'s discipline: exact bytes while they fit, else a
fixed-width magnitude, so precision yields to the invariant rather than
the other way round. This is not the deferred human-readable column --
the exact count still shows right up to where it cannot. Pinned with a
sparse 12 GB fixture that skips if the filesystem refuses it.
F3 (honesty and a doubled read). The symlink arm claimed the probe cost
"one syscall"; it was a full `read_dir` -- opendir plus one lstat per
child -- and on success `open_directory` immediately read the same
directory again. Since `open_directory` reads before touching editor
state and raises having changed nothing (acceptance 15's invariant), its
failure IS the "not a directory" answer: the probe is gone, one read
remains, and the comment says what it actually does. New test pins both
arms -- a symlink to a directory descends under the path the user walked
(canonicalization is lexical, so the link is not resolved), and a
symlink to a file opens with the target's contents.
F4 (deliberate failure mode). A tolerant listing recorded readdir
iterator errors without bound, and `std::fs::ReadDir` need not terminate
after yielding one. Cancellation is NOT an adequate backstop here --
which is the reason for a constant rather than a comment saying it is: a
dired listing carries no supersede key, so nothing cancels it. A
directory whose iterator produces nothing but errors now fails with the
last error the way an unopenable directory does, after
READDIR_MAX_CONSECUTIVE_ENTRY_ERRORS; the counter resets on any entry
that materializes. Documented as untested and why: faking a failing
iterator needs the walk generic over it, a refactor with no other
consumer.
Smaller notes, all taken: READ_ONLY_LIMIT renamed NAME_VARIANT_LIMIT (it
caps `<2>`..`<99>`, nothing read-only); `fmt_perms`' omission of
setuid/setgid/sticky documented as a decision tied to the M8.3 fixture's
nine-bit parser; `format_outcome` binds the slice in the pattern instead
of re-traversing; and `pmacs.path.canonicalize`'s `to_string_lossy` is
noted as inside the existing non-UTF-8-path deferral rather than an
exception to it.
Process note, learned the hard way twice now: the round-1 dired.lua
fixes were briefly wiped because a mutation-bite helper restores with
`git checkout --`, which reverts to HEAD -- so a fix must be committed
BEFORE it is bitten, not after.
Dired is the file surface, not a rider on one: before Stage 0 (#162)
pmacs had no way to open a file by path, and browsing is the half a
user reaches for when they do not already know the path. Stage 1 ships
the view.
builtin/runtime/dired.lua: one buffer per directory named by the
canonical path (Q#DR2) with an ownership check before any paint (F7);
read-only intercept plus round-trip input (Q#DR3); a `dired` major mode
carrying mode-scoped keys (Q#DR8) -- RET/f visit, ^ parent, n/p, g
revert, q quit, s sort; cursor re-seated by basename across every
wholesale repaint (Q#DR9); file visits through
`pmacs.window.display_file` and directory descent through dired's own
window (Q#DR10); `C-x d` / `C-x C-j`; and `dired.kill-when-opening`
through the config registry.
Two Rust changes, both narrow:
* `read_dir` grows per-entry tolerance behind an opt (Q#DR6). Five
per-entry conditions used to fail the entire listing, so a plain
refresh of a busy directory could just fail; the module doc's claim
that a tolerant wrapper was "the package's job" was false, because
the primitive hands Lua one structured error and no partial vec.
Per-entry readdir/lstat/readlink failures and non-UTF-8 symlink
targets now land in an `errors` channel; parent-level failures and
non-UTF-8 *names* stay fatal. The tolerance travels in the settled
payload, so the Lua boundary keeps the bare-array shape the frozen
M8.2 fixture consumes and never has to look the job back up. The read
ops' opts parsing now rejects unknown keys, so a typo'd `tolerant`
cannot silently degrade to the fatal contract.
* `normalize_buffer_path` is exposed as `pmacs.path.canonicalize`
rather than mirrored in Lua. Q#DR2 named exposure the preferred end
state; it needs no borrow plumbing, so dired's name-dedup and
`display_file`'s `find_buffer_for_path` dedup cannot fork, and the
mirror's Stage 2 removal is not owed.
tests/dired_acceptance.rs covers framing items 1-16 (22 tests), driven
through real key dispatch. Item 17 is the m8_1/m8_2/m8_3 gate.
One framing claim is corrected by the substrate: R2-3 expected a
dedicated dired panel to carry its dedication across a descent, but
`display_buffer` never replaces the buffer in a slot dedicated to
another one -- it discards every side-specific parameter and falls back
to the document window (Q#BP3 2.iii). Dired does not try to unpin the
user's panel; both arms are pinned.
COHERENCE.md §1.2 makes "a `pcall` around background wiring must log
attributed failure, never discard it" a standing rule, and names
`ensure_server`'s swallowed spawn failure as its canonical case — the
exact function this branch modifies. Round 1 deferred the resolver's
silent `pcall` as a Stage 3 concern. Under that rule it is not a
deferral, it is a fresh instance of the named anti-pattern added by a PR
touching the cited function, made worse by the memo: a raised error is
buried permanently for that directory and never observed again.
A resolver that raises, or returns a non-string non-nil, now leaves an
attributed trace naming the language and the directory. Returning nil
remains the documented decline and stays silent — pinned, so "report
failures" cannot be satisfied by reporting every resolution.
The report goes through `pmacs.editor.set_status`, NOT `pmacs.error`,
and that choice is the finding:
**`pmacs.error` does not exist.** Fifteen call sites across `async.lua`
(5), `syntax.lua` (4), `lsp.lua`, `mcp.lua`, `fs.lua`, `editops.lua`,
`autosave.lua`, and `commands/default.lua` report background failures
through it, each guarded `if pmacs.error then ...`. It is defined
nowhere in production; the only assignment in the tree is a test stub at
`src/editor.rs:9881`, and `type(pmacs.error)` is nil in a fresh
`EditorState` (probed, not inferred). `pmacs.errors` (plural) in
compile.lua is an unrelated namespace. So all fifteen reports are dead,
and the guard makes the silence look deliberate — which is why nobody
noticed. Writing the test is what caught it: the first version of this
fix used `pmacs.error` and its pin failed against a working
implementation.
Both bites recorded: dropping the report entirely fails the pin, and so
does reporting ONLY through `pmacs.error` — the dead-channel variant
this nearly shipped.
Not fixed here, deliberately: defining `pmacs.error`, the fifteen dead
sites, and surfacing the spawn failure itself. That last is Priority 1
work and a user-visible product behavior — what message, where, with
what guidance — so it needs its own framing rather than being smuggled
into an affinity PR.
The blocker was process, not design. The test file was committed before
`cargo fmt` ran, so the reflow of five over-width assertions sat
uncommitted in the working tree while the branch as pushed failed the
first gate in CLAUDE.md. The "fmt clean" reported on the PR described
the worktree, not the branch. Gate results are only meaningful run
against the pushed tree, so this commit lands the formatting first and
the gates are re-run against it.
Two pins review asked for, each covering a branch the nine acceptance
tests left untested:
- A **string** `config.root` as an affinity key. acc17 covers only the
function form, so `return configured, "config"` had no test. The bite
puts both files in their own marked project: drop the config arm and
they key on their own detected roots and spawn two servers, so one
server on the configured root is only reachable if the override wins.
- `root = false` reads as unset. Defended by a truthiness check rather
than `~= nil`, previously by comment alone. Under `~= nil` the config
arm returns `false, "config"` and `file_uri_for(false)` returns nil, so
the file lands on a rootless server instead of its detected project.
Each was falsified against exactly the mutation it targets and neither
against the other.
Also documents an asymmetry review caught: `project_root_for`'s
"detected" arm is canonicalized for free because `pmacs.project.detect`
canonicalizes before walking, but a **configured** root — string or
resolver return — is fed to `file_uri_for` exactly as written, and the
affinity key is that URI. On macOS a resolver returning `/var/…` and a
detected `/private/var/…` are therefore different keys for one
directory, silently yielding two servers for one project. There is no
Lua-side canonicalizer to normalize it, and Stage 3's Lean resolver is
the first real consumer, so the obligation is stated in the
`config.root` doc comment where that resolver's author will read it.
`ensure_server` reused any live server whose `language_id` matched,
regardless of project root — its own comment documented this as a known
post-v0.1 limitation. For project-model-strict servers that is a
correctness failure, not a rough edge: `lake serve` is bound to one Lake
package, rust-analyzer and gopls to one workspace, so the second project
a user opens gets a server that cannot resolve its imports.
Server affinity is now keyed on the project root, with one rule that
keeps the change from regressing every other language:
The affinity key is the root only when a root was actually FOUND.
`project_root_for` never returns nil for a file that has a path — its
last resort is the file's own directory — so a naive `(language_id,
root)` key would give every directory of loose scratch files its own
server, for every language: two stray .py files in different directories
would spawn two pyrights where today they share one. It now returns
`root, source` with source one of "config" / "detected" / "fallback",
and only the first two become an affinity key.
Matching is on the spawned spec's `root_uri`, nil matching nil, so the
fallback spawn passes `root_uri = nil` for the key and the stored spec to
agree. `cwd` still carries the directory, and `build_initialize`
(src/lsp.rs) derives the identical `rootUri` from `cwd` when the field is
None — using a percent-encoder with the same allowed set as Lua's
`file_uri_for`. The initialize payload for that case is therefore
byte-identical to before; only what the reuse loop matches on changes.
`build_initialize` is the only reader of `spec.root_uri` in the tree.
Two consequences, both deliberate and both asserted rather than
discovered:
- A server hand-spawned from init.lua with only `cwd` set also reads
back nil, so a root-bearing attach will not adopt it. We cannot know
which root it was meant to serve, and guessing wrongly routes a
project's files to the wrong server.
- Opening files across N project roots spawns N servers. rust-analyzer
has the same property and no editor caps it by default; `pmacs.lsp.stop`
is the manual escape and an LRU reaping policy stays deferred.
`config[language].root` may now be a `function(path) -> string|nil` as
well as a string, for languages whose root rule the shared marker walk
cannot express — an innermost-wins walk cannot find an *outermost*
marker. A resolver returning nil declines and falls through to the marker
walk. Results are memoized per directory because hoisting the root
computation above the reuse loop puts it on every attach rather than
every spawn; the memo is keyed weakly by the resolver function itself, so
replacing `config[lang].root` cannot serve a root the old one computed.
`pmacs.lsp.list()` rows gain `root_uri` and `cwd`. `root_uri` is the spec
field verbatim, deliberately not the URI the server was initialized with.
No protocol change. No Lean content: this is the shared affinity function
for every LSP language, so it ships as its own PR and is exercised
through rust, python, go and typescript against `pmacs_fake_lsp`.
tests/lsp_multi_root_acceptance.rs covers acceptance 13-21. Every fixture
sets `pmacs.project.set_search_boundary` at its own tempdir root:
without it the marker walk climbs to the filesystem root, and a stray
`.git` above the temp directory would turn the markerless cases into
detected ones — the assertions would still pass while testing nothing.
Refs docs/lean4-mode-framing.md Q#LN15, acceptance 13-21.
Completes Arc 8 Stage 1: the Lua-side tables that turn a recognized
grammar into a usable mode, plus the acceptance suite for all twelve
framing criteria.
comment.lua -- `lean4 = "--"` (Q#LN5). Line comments only; Lean's block
comment `/- -/` and docstring `/-- -/` belong to the comment arc's own
named deferral and this lane does not front-run it.
pair.lua -- `⟨⟩`, `⦃⦄`, `⟮⟯` alongside the ASCII brackets (Q#LN6). The
anonymous constructor is among the most-typed constructs in Lean;
omitting it would make the pair set feel broken. The other two ride along
because the Stage 4 input method can produce them, and a bracket the pair
set does not understand is worse than one it does. All three sit outside
the nine built-in pair chars, so per Q#AP1 their undo is
cross-peer-degraded -- the documented, pre-existing limitation of
user-extended pairs. No `''`: Lean uses the prime as an identifier suffix
(`h'`, `foo'`), the same reason Rust excludes it.
syntax.lua -- the `lean` -> `lean4` modeline alias (Q#LN2), so an Emacs
`-*- mode: lean -*-` or a Vim `ft=lean` line is not stranded by the entry
being named `lean4`.
syntax.rs -- the `lean` -> `lean4` injection alias (Q#LN17), so both
```lean and ```lean4 fences highlight. The Lean 3 spelling is mapped
forward deliberately: a ```lean fence is overwhelmingly Lean 4 in
practice.
highlight.rs -- `warning` moves from bold red to bold BRIGHT red. Writing
the test found the collision: `number` is plain `fg(1)`, so `sorry` and
the literal `42` beside it were the same colour, differing only in the
bold flag. `sorry` means "admitted, not proved" and is the one token in a
proof file a reader must never skim past, so it now gets the loudest
entry in the table and the test asserts the full style rather than the
colour.
Twelve criteria, seventeen tests. Notes on the ones that could have been
vacuous:
* acc4 uses a `.txt` fixture, not `.lean` -- on a `.lean` path the
extension alone yields `lean4` and the assertion would pass with the
alias table empty. acc4b removes the alias and pins that the raw name
survives, so acc4 cannot silently stop testing anything.
* acc11 goes through the real `_parse_now` injection path and asserts a
`lean4` CHILD LAYER appears. `pmacs.parse.injection_aliases` is a
documented write-only proxy, so an alias-table read would have proven
nothing about the parser; acc11b pins that a misspelled fence still
resolves to nothing.
* acc12 asserts through the process supervisor and the server list that
opening a Lean buffer spawns nothing. This is not decorative: the
machine this arc was scouted on has elan installed with no default
toolchain, where `lake --version` itself fails, and Stage 1 must be
unaffected by that.
Gates: fmt and strict workspace clippy clean; 1,826 default + 2,003 CRDT
library tests; lean4 Stage 1 9, comment toggle 14, auto-pair 45,
injection 4; M4 121; required GPU 152; isolated-config workspace sweep
3,150 across 90 suites; `git diff --check` clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
PR #155 review round 2.
Finding 1 (must fix): Q#BP7 item 1 — "growth reaching the live tail
re-arms follow (top -> None), only when no selection is active" — was
never implemented. `at_bottom` is the instantaneous geometric readout
`scroll_offset == 0`, which a still-anchored view satisfies whenever it
happens to be tall enough to reach the tail, so the round-1 assertion
could not see the gap: the next rows the child printed pushed the
anchored view back into history.
`rearm_follow_on_growth` now clears `top` when a viewport-size
declaration makes the view cover the tail and no selection is frozen,
and every size-declaring path (`snapshot_for_view`, `record_view_size`,
`view_status_for_size`) routes through one `declare_view_size` helper so
grid and semantic declarations cannot disagree. `scroll_view` and
`begin_selection` deliberately stay out: they write `top` themselves,
and `scroll_view` already owns the scroll-driven arm.
New acc32b is the pin the review asked for: scroll into history, grow
past the tail, then release a SECOND burst of child output through a
filesystem gate and assert the view moved with it.
Finding 2: the PTY fixtures emitted LF-only output, which staircases
rightward until every row clips to blanks past the viewport width — so
the round-1 anchor assertions compared "" with "" and could not fail.
Both fixtures now emit CRLF, and each anchor comparison is guarded by
`assert!(!top_before.is_empty())`.
Finding 3: acc33's contrast case asserted nothing, and the behavior it
claimed was false as coded. With the re-arm in place it is true and now
asserted: clearing the selection at the same geometry re-arms follow and
leaves the frozen anchor.
Finding 4: `start_run` gated the panel branch on `display == "panel" or
already_in_panel(..)`, so an explicit `display = "current"` lost to the
inference — and that value is the documented user-facing opt-out from
the Stage 3 default flip. Now gated on OMISSION. acc19b gains the
explicit-"current" case.
Finding 5: `window_drag` is a `HashMap<FrontendId, WindowDragState>`, so
a peer's mode-line press can no longer steal or clear another
frontend's in-flight gesture, and concurrent drags are legal. Cleared on
detach. acc30c gains the mode-line-press case.
Minor: `pmacs.window.buffer()` resolves both arms through the acting
frontend using the shared `lookup_window` / `selected_window` validators
rather than re-implementing them beside an ambient `active_buffer_id()`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
PR #155 review round 1.
Finding 1 (must fix): `try_split_active` had no production caller —
`pmacs.window.split_horizontal` / `split_vertical`, and therefore
`C-x 2` / `C-x 3`, still went through plain `split_active`. Splitting a
focused panel made the root wrapper's final child a split rather than
`Leaf(side)`, which both `Layout::compute`'s fixed pass and
`document_subtree` key on: the panel band reverted to 1:1 weight
division and an ordinary window ended up living inside it. Both bindings
now route through the guard, and acc26 asserts through the real Lua
path — a direct core call passes with the guard unwired, which is how it
survived the first round.
Finding 2: the armed-drag early return now checks the arming frontend,
so one frontend's in-flight gesture cannot cancel or swallow another's
mouse events. New acc30c.
Finding 3: `paint_mode_line_graphemes`'s doc block was left heading
`paint_divider_segment`; moved back.
Finding 4: a recompile carries no `display`, so it took the raw switch
and duplicated a panel-placed `*compilation*` into the document window.
`start_run` now detects that the buffer already owns the panel slot.
`pmacs.window.buffer` gained an optional window argument so an adopter
can ask without selecting the panel first. New acc19b.
Stage-2 hazard pins the review asked for, both in `src/daemon.rs`:
a fresh attach while LOCAL is focused in a panel inherits LOCAL's
document buffer, and an initial-target bootstrap whose `after-load`
hook creates and selects a panel still reasserts into a document window.
Minor: dropped listview's dead `p.side`; documented `focus_window`'s
caller-validates contract; `jump_back` restores through `focus_window`
so the "every focus change" contract holds; `params` / `resize` default
to the acting frontend's selected window rather than the ambient one;
widened the flexible-division math to u64 intermediates.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
- `listview.open`, `compile.run`, and `pmacs.terminal.open` all take the
same strict `display = "current" | "panel"`, validated before any
buffer, session, process, or wrapper exists. Omission keeps today's
behavior; Stage 3 flips the default.
- `listview.quit` / `compile.quit` delegate to `window.quit` only when
the buffer really is in a side window, so the presentation is deleted
or restored instead of leaving a source buffer stranded in the slot.
- LSP `visit_location`, LSP go-to-definition, and compile `visit_error`
route through `display_file`, so a visit from a panel lands in the
document target and fires its hook with that window active.
- `window.quit`'s Delete arm focuses the revalidated remembered origin.
- Capability fallback discards an accompanying `height` rather than
rejecting the call.
- `window.min-height` clamps a below-floor value on read instead of
refusing the write.
- `tests/bottom_panel_stage1_acceptance.rs`: 42 tests over the framing's
Stage 1 criteria, including the two production `Layout::compute`
callers, the recursive minima, hide/reappear, the final-focus matrix,
quit chains at the depth cap, per-frontend jump origins, the divider,
and a real-PTY pin of Bet B1.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Stage 1 substrate for the bottom-panel arc (docs/bottom-panel-framing.md).
- `WindowParams` (side / fixed_rows / dedicated + implementation-owned
quit action and remembered document origin), `Side`, `QuitAction` with
a bounded replacement history, and the `MIN_WINDOW_OUTER_ROWS` floor.
- `Layout::compute(area, fixed)` allocates fixed rows before dividing the
remainder by weight; both production callers feed the same shared map,
including the peer-presence overlay pass that derives its own rect.
- `subtree_min_rows` / `interactive_min_rows`: the recursive minima, and
`boundary_below` for the shared drag / keyboard resize boundary rule.
- `FrontendView` gains `panel_capable`, `frame_geometry`, and the derived
`panel_hidden`, each spelled explicitly at every construction site.
- `EditorCore`: `primary_document_window`, the non-side target rule,
`display_buffer` + placement policy, `quit_window`, side-window removal
on `kill_buffer`, per-frontend jump entries with origin windows, and the
shared resolve/load-without-switch seam the initial-target bootstrap now
uses too.
- `EditorState`: the panel reconciliation transaction, geometry
declaration, the side-window `dispatch_idle_for` gate, divider paint,
and divider drag.
- `pmacs.window.display / display_file / quit / panel / params /
set_params / resize / display_target`, plus `builtin/runtime/window.lua`
with `window.panel-height`, `window.min-height`, and the resize commands.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The fold engine behind `docs/folding-framing.md` (approved rev 5): a
per-buffer fold store, a structural tree-sitter fold source, the
state-aware Lua command + data-API surface with the Emacs hideshow
`C-c @` bindings, the dispatch-layer pre-edit unfold, and `FoldState`
production. No rendering — Stages 2 (grid) and 3 (GPU) consume the store.
- `src/fold.rs`: `FoldStore` (a buffer-attached `View` that translates
ranges on every edit and drops any whose head/tail the edit crosses,
provenance-blind — Q#FD6), the structural source (nearest block-like
node >= 2 source lines -> introducer<->body -> **derived head line**,
the line immediately above the first hidden line, so wrapped signatures
and `where` clauses stay visible per R3-1 -> **closer-aware tail**, a
closing-delimiter line stays visible per R2-5), injection-layer walk,
`(start, end]` containment, and the state-aware ops (close innermost
open / open outermost closed / org-TAB cycle). Stale/absent tree
refuses (Q#FD10).
- `src/lua_bindings/fold.rs`: `pmacs.fold.*` — explicit-buffer data API
(`fold`/`unfold`/`folds`/`toggle`) + interactive helpers, validation
(Q#FD11: document buffer, UTF-8 boundaries, >= 1 hidden line — Q#FD9
falls out of the last clause), point-moves-to-head (Q#FD3).
- `builtin/runtime/fold.lua`: `fold.toggle/close/open/close-all/open-all`
commands + the `C-c @` prefix set (Q#FD4).
- `src/editor_core.rs`: the six point-anchored edit primitives run the
pre-edit unfold keyed on the authenticated source's point (Q#FD5,
command path); `EditorCore` owns the shared `FoldRegistry`.
- `src/semantic_render.rs`: the `FoldState` producer —
authoritative-empty, diff-suppressed, baseline resets on
`BufferSnapshot` (Q#FD8); the "never emitted" pin split so
`BlockAdornments` stays unproduced.
- `tests/folding_acceptance.rs` (16) over real Rust/Python/markdown
grammars + `fold_state_producer_transitions` + 15 engine unit tests.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Q5BkezMppbpCgGAYk2ftxV
Integrate landed Vterm Stage 2 before the approved modeline merge. Preserve the
active modeline lane in the volatile ledger and record the full integrated gate
results.
Parse bounded Emacs and Vim modelines, normalize common aliases, and give
explicit file metadata precedence over inferred language. Pin one fresh-load
language decision for syntax, LSP, pairing, comments, and initial major mode,
while preserving the LSP path guard and explicit mode overrides.
Cover supported forms, rejection boundaries, precedence, unknown modes,
shebang and modeline pinning, reopen behavior, and pathless buffers.
Store a detected major mode on each buffer and expose it through Lua.
Resolve mode-scoped bindings in dispatch, describe-key, and help links,
including exact encoded mode context after entering the help buffer.
Initialize modes once at buffer load, preserve explicit overrides and
clears across switches, and publish the mode through a per-window
statusline provider. Add daemon acceptance for the complete mode lifecycle.
Levi Neuwirth