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.
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.
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.
CI round 1: both macOS jobs failed on the acceptance case added last
commit. APFS enforces valid UTF-8 in filenames, so `std::fs::write` with
a 0xFF byte in the name fails with EILSEQ ("Illegal byte sequence")
before `pmacs.fs.canonicalize` is ever called. The fixture cannot be
built there.
That is a filesystem refusing to represent the case, not a behavioral
difference: the subject — `to_str()` returning None for a non-UTF-8
resolution — is platform-independent Rust, and the Linux run pins it.
`#[cfg(unix)]` was the wrong granularity; review had asked for unix
gating on the symlink tests and I applied the same gate here without
checking whether the filesystem, rather than the API, was the
constraint.
Gated `#[cfg(target_os = "linux")]` with the reason in place, rather
than skipped at runtime, so a future failure here is a real failure and
not a silent no-op.
Ledger records both CI-round facts: this one, and that
`composition_overhead_under_ten_percent` is load-sensitive under a
parallel workspace sweep (it reported -4.6% realistic overhead in the
same run that tripped its 10% budget at 18.8%, which is noise, not work).
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.
Rev 5 said acceptance 34's second edge was a killed buffer. Implementing
it showed that is false: the Rust core 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**, so lsp.lua never tears an attachment down and the drain keeps
reaching that server. The premise (the drain builds its sid list from
`attachments`) was right; the inference needed attachments to be removed
on kill, and nothing removes them.
The reachable leak has the same root cause by a different path.
`attach_buffer` drops a sid from `attachments` the moment
`server_is_live` reports false and rebuilds against a fresh server — so
`crashed` / `stopped` is the event *least* likely to be drained, and an
event-driven purge leaks in exactly the case it exists for. The purge
therefore polls `pmacs.lsp.list()`, which enumerates the manager
directly. Acceptance 34's second half now exercises a server in **no**
attachment, which is the shape that discriminates: bitten, an
event-driven purge fails it while the attached case still passes.
§0.1 finding 6, Q#LN9, and acceptance 34 all updated; the wrong wording
is left visible with its correction rather than quietly replaced, since
the mistake is the useful part.
Ledger gains the Stage 3a lane: branch, worktree, what ships, both
corrected claims, the `install_async` load-order trap, the recorded
bites, the one knowingly unpinned guard, and gate results.
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.
Two review findings, both revision edits.
**Q#LN8's marker test was wrong in the other direction.** Rev 5 fixed
the directory case by reading a byte and requiring a non-nil read — but
an **empty** `lean-toolchain` reads nil at EOF too, so that rule
declines a marker that exists, silently, falling through to
`pmacs.project.detect`. Marker semantics here are `lean4-mode`'s
`locate-dominating-file` semantics: existence, not content, and a
`lean-toolchain` can legitimately be empty.
The discriminator is `read`'s second return, probed on LuaJIT 2.1:
| Path | `io.open` | `f:read(1)` | Verdict |
|---|---|---|---|
| file with content | handle | `"l"`, no error | marker |
| empty file | handle | `nil`, no error | marker |
| directory | handle | `nil`, `"Is a directory"` | decline |
| missing | `nil` | — | decline |
So `local data, err = f:read(1)`, declining only on a non-nil `err`. The
rule needs no per-platform re-probe: both directory behaviors are
declines, since a platform whose `fopen` refuses a directory fails at
`io.open` and one that opens it fails at `read`. There is no platform on
which a directory both opens and yields a byte.
Acceptance gains **24b** (an empty `lean-toolchain` marks a root) beside
24a, with the obligation that each be shown to fail against the
implementation satisfying only the other. A suite carrying just one is
satisfied by a resolver silently wrong for the other case — which is
precisely how rev 5's first answer got written.
**Citation sweep.** Round 4 stated the `project_root_for` correction in
§0.1 without editing the citation in §2.5; the correction and the fix
are different acts, and noting one is not doing the other. Review caught
a second stale citation (`handle_server_requests` at :1448), which
prompted a sweep of every `file:line` from §2.4 onward. Four more were
stale. All six: `project_root_for` 513 → 592, `ensure_server` 527 → 610,
`handle_server_requests` 1448 → 1549, `take_typed_edit` 12798 → 12827,
`pair.lua` 213 → 229, `compile.lua` 264 → 266. Six others were verified
good and left alone, listed in §0.1 so the next sweep knows what has
already been checked.
Q#LN15's present-tense "the change is small and spans two files" now
reads as past tense with its PR number, since that stage landed. Its
pre-#161 line numbers stay as written — historical record, not
navigation.
Stages 1 and 2 landed (#160, #161). Re-scouting Stage 3 against `main`
@ `46a1b8f` — six merged PRs past the rev-4 snapshot — produced three
findings that change the plan and four that confirm it. Two were
established by running Lua in a fresh `EditorState` rather than by grep,
and are marked *probed* in §0.1.
**Stage 3 violated this document's own splitting rule.** §4 says "no PR
in this arc mixes a cross-cutting substrate change with Lean feature
content" and "a reviewer looking at Stage 3 sees only Lean" — while §4's
own risk column for Stage 3 read "two `lsp.lua` generalizations". Those
cannot both be true. One generalization shipped as Stage 2; the other is
Q#LN9's dispatch seams, which modify `handle_server_requests` —
confirmed the only production drain of LSP events, since
`LspManager::take_all_events` has no non-test caller. By the test that
justified splitting Stage 2 out, that is cross-cutting substrate. Stage
3 is now 3a (seams + canonicalizer, no Lean) and 3b (the Lean server),
strictly sequential.
**The Lean resolver could not satisfy the contract Stage 2 documented.**
#161 established that a configured root reaches `file_uri_for` verbatim
and that the resulting URI is the affinity key. Probed:
`pmacs.editor.file_path()` is not canonical — opening
`<tmp>/linkpkg/sub/./../sub/a.lean` through a symlink yields
`<tmp>/linkpkg/sub/a.lean`, lexical collapse only. No canonicalize
binding is exposed to Lua, and `pmacs.project.detect` canonicalizes but
returns nil without a marker. So one Lake package opened by two
spellings would spawn two `lake serve` processes — the bug Stage 2 was
built to prevent, re-entered through Stage 3's door. New Q#LN20 adds a
synchronous `pmacs.fs.canonicalize`; it rides 3a, and it serves every
future function-valued root rather than only Lean's. Two alternatives
are recorded with why they were rejected — the `detect`-anchored walk in
particular is incorrect, not merely inelegant.
**`pmacs.fs.stat` is unusable in the resolver.** It is async and the
resolver runs synchronously inside `ensure_server` ← `attach_buffer` ←
`buffer.after-load`, with no coroutine to await on. Probed: `io` and
`os` are exposed in the sandbox, so the marker walk uses `io.open` — the
opposite of what a reader would assume, hence Q#LN8 now says so. One
edge, also probed: `io.open` succeeds on a directory, so the walk reads
a byte rather than testing for a handle, and acceptance 24a bites the
version that does not.
Confirmed rather than changed: Q#LN7's stop-before-respawn is necessary
(default policy is OnCrash, the termination handler never consults the
exit code, and `maybe_restart` has no attempt ceiling — a broken `lake`
respawns forever; `stop()` setting `restart = Never` is what disarms
it); the response seam works as specified, since `Response` events are
pushed unconditionally and `send_request` returns the keying id.
One confirmation narrowed the design. `handle_server_requests` builds
its sid list from `attachments` and `push_event` is uncapped, so
subscribers fire only for servers with a live attachment. That turns
acceptance 34 into a reachable leak: killing the buffer with a request
outstanding strands the registration behind a drain that no longer runs.
The purge is now driven from both edges and 34 exercises the buffer-kill
path, which is the one a user can reach.
Also: §9 states the lane's coherence impact per COHERENCE §20 (journey
steps, interaction islands, config registry, background attribution),
including the honest note that 3b makes §2's step-3 grade marginally
worse by adding one more instance of the silent-spawn-failure class.
Three items are named in §6 rather than paid: the uncapped event queue,
the dropped `cfg.restart`, and surfacing the spawn failure itself.
Acceptance keeps every rev-4 number. The two split sections are
bulleted with literal labels because a markdown ordered list renumbers
from its first item, and 3b's criteria are non-contiguous; round 3's
finding 4 was stale references surviving a renumber, and not renumbering
is the cheaper way to not repeat it. Stale cross-references from the
split were reconciled in the same pass, and `project_root_for`'s
citation was corrected from 513 to 592 per COHERENCE §25.
Rides this PR per COHERENCE.md §25 ("when a PR changes any audited claim
here, updating this file rides that PR").
§0 and §7: multi-root LSP affinity moves from in-flight-branch to PR
#161, and §7 gains the rule the slice actually establishes — a
*fallback* root is deliberately NOT an identity, so markerless files
keep sharing one server per language. That is the part a reader would
otherwise assume went the other way.
§1.2 gains the finding this PR turned up, which sharpens the audit
rather than restating it. The section recorded that background failures
produce "no `*errors*` entry"; the sharper fact is that **the channel
does not exist**. Fifteen call sites — `async.lua` (5), `syntax.lua`
(4), and one each in `lsp.lua`, `mcp.lua`, `fs.lua`, `editops.lua`,
`autosave.lua`, `commands/default.lua` — report through `pmacs.error`,
each guarded `if pmacs.error then ...`. It is defined nowhere in
production; the only assignment in the tree is a test stub
(`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. All fifteen are dead, and the
guard is what kept it unnoticed — it makes the silence read as
deliberate.
Hence the corollary now recorded beside the rule: report through a
channel with a **test that observes it**, or the guard is
indistinguishable from the silence it was meant to fix.
Also a frequency note: per-root affinity makes the
preconfigured-but-missing-server failure fire once per project root
rather than once per language per session. Unchanged in kind, strictly
more frequent. Surfacing it stays Priority 1 work needing its own
framing — it is user-visible product behavior (what message, where,
with what guidance), not a substrate fix to smuggle into an affinity PR.
Line-number citations in the touched sections re-verified per §25;
symbols are authoritative where they drifted.
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.
Lands the approved dired framing on main as its own docs PR, and brings
the two required docs current after find-file merged as #162.
The framing was approved after two review rounds (seven findings, then
six) and revised twice more since: revision 4 recorded what implementing
Stage 0 falsified in the approved text, and revision 5 adds the coherence
impact statement that #163 made mandatory for every framing.
The coherence statement is new work, not a restatement. COHERENCE.md
section 20 Priority 1 already names this arc -- a find-file surface and
directory-argument handling -- so the framing now states which journey
steps it touches (7, and partially 3), that it adds no interaction island
because its keys are a mode-scoped keymap through the ordinary registry
and wdired is a mode swap rather than a modal layer, that it adopts the
config registry for dired.kill-when-opening, and that it inherits the
worker-attribution gap for its read_dir jobs without worsening it. It
also draws the boundary against the adjacent Journey Stage 1 arc: CLI
directory handling belongs there, the two meet at resolve_target_buffer,
and dired supplies the buffer a directory should resolve to rather than
growing a second directory surface.
One convergence worth recording: section 2 grades the golden journey
broken at step 3 because pmacs on a directory exits 1, and the mechanism
it cites -- File::open succeeding on a directory, then read_to_end
returning EISDIR -- is the same one Stage 0 pinned in its
accepting-a-directory test, where the pcall turns it into a status
message instead.
The handoff snapshot was stale through eight merges. It now anchors on
main at 2af1ab3, records COHERENCE.md as required reading and a required
framing input, and carries the two minibuffer facts find-file
established: a custom completion source cannot descend directories, and
a selected candidate shadows typed text -- both of which apply to M-x and
switch-buffer, not just find-file.
The ledger gains the dired lane with Stage 1's scope, the reason its one
Rust change cannot be done in Lua, and the rebase note for the dired
branch, whose framing commits become redundant when this lands.
COHERENCE.md states the product-coherence thesis (pmacs should be
immediately excellent, progressively understandable, completely
inspectable, and ultimately replaceable) and, per-section, the audited
ground truth of how the codebase measures against it: a scorecard
across 19 concerns, the golden-journey verdict table (breaks at "open a
real project" -- `pmacs .` exits 1), the six hardcoded key-interception
shadows with no transient-keymap mechanism to migrate them to, the
discoverability substrate-without-surface gap, the package/worker
identity gap, and three cross-cutting patterns (substrate without
surface, the silence asymmetry, per-arc coherence debt) that explain
most of the individual findings.
CLAUDE.md and AGENTS.md now list it as required reading alongside
agent-handoff.md and active-work.md, and ask new framing docs to state
their coherence impact. No runtime code changes.
Three of the five review findings land here; the other two are recorded
as named deferrals in the framing on the dired branch.
Finding 1: the command comment cited "acc4", a name from a draft scheme
that no test carries. It now names the real test, and the comment splits
the shadowing consequence into the two cases that actually exist -- a new
bare name that matches an entry (shadowed) versus one that matches
nothing (creates normally) -- each pointing at its test.
Finding 2: the everyday new-file flow had no test. Typing a bare name
that is not a subsequence of any entry is the path users hit first, and
the only route combining free text with a relative join; every existing
new-file test used a name containing a separator.
find_file_bare_new_name_creates_in_the_root covers it, asserting the
parent is the prompt's root so the join itself is pinned.
Finding 3: the failure arm was never exercised, and as the review noted,
deleting the pcall would have passed the whole suite. Accepting a
directory candidate reaches display_file, whose load fails because
File::open on a directory succeeds and the read returns EISDIR;
find_file_accepting_a_directory_reports_instead_of_raising pins that this
surfaces as the command's status message, leaves the active buffer alone,
and closes the prompt. Verified by manual revert: with the pcall replaced
by a direct call, that test and only that test fails. scripts/bite could
not isolate it, since the guard and its test have no separating commit.
Finding 4 is documented at the command rather than left implicit:
accepting on empty input opens the first-sorted candidate, because
fuzzy_score returns Some(0) for an empty needle and filter_and_sort
breaks the tie lexicographically, so dotfiles lead and a directory can
lead. M-x and switch-buffer share the mechanism, so it is inherited
rather than introduced, and it is listed in the framing beside the
accept-semantics change that would close it.
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.
Stage 1 merged as #160 (`main` @ `0827dd1`); the Lean lane header and
branch line now say so, and Stage 2 gets its own subsection.
Edits stay inside the Lean lane. PR #156 is still open against both this
file and `docs/agent-handoff.md`, and it rewrites the snapshot header,
the canonical-base line, and the whole bottom-panel lane — so those are
left alone rather than merged twice. `agent-handoff.md` is untouched for
the same reason plus its own: §1 describes what is on `main`, so it
updates at merge, not during review.
Records the one finding this stage turned up but did not fix:
`ensure_server` never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
`restart` in `pmacs.lsp.config[lang]` is silently dropped on the
auto-attach path. Pre-existing, and out of scope for a PR whose
acceptance 16 pins existing attach behavior as unchanged.
Dired arc Stage 0 (docs/dired-framing.md section 10, Q#DR11). Until now
pmacs had no discoverable way to open a file by path: no find-file
command and no C-x C-f binding, so a file entered a session only from
the CLI, an LSP jump, a project-search visit, or C-x C-r, whose prompt
does pass free text through but completes only over the recent list.
The command prompts with completion rooted at the active buffer's
directory, or the process cwd when the buffer has no backing path, and
opens the result through pmacs.window.display_file. A path that does not
exist yet creates a buffer bound to it with the "[new file]" status,
which is Emacs parity and comes from resolve_target_buffer rather than
anything added here. Nothing is written to disk until the user saves.
Two substrate facts shape the design and are documented at the command
rather than left to be rediscovered.
Completion is flat: the files source lists one directory and yields bare
basenames, and a custom function source could not do better, because
sources are called with no arguments and run synchronously outside any
coroutine, so a callback can neither see the input to re-root on nor
await a directory listing. Hierarchical completion is a named Rust
change in the framing.
A selected candidate shadows typed text: recompute_candidates selects
index 0 whenever the candidate list is non-empty, and
resolve_accepted_value returns the candidate over the typed contents. So
typed text reaches the accept handler exactly when the input filters
every candidate away, which for basename candidates under a subsequence
filter means when it contains a separator. That makes the deeper-path
case work verbatim and leaves one hole: a new bare name that is a
subsequence of an existing entry opens the existing file. The acceptance
pins that as a decision rather than an accident; closing it needs a Rust
change to accept semantics that Stage 0 deliberately does not make.
A leading tilde is expanded before the path reaches the core, because
get_or_load_buffer normalizes the path it stores but loads from the raw
one -- so an unexpanded tilde path deduplicates against an already-open
buffer yet fails to load a file that is not open yet.
The prompt field starts empty and names its root in the prompt string
instead: any prefill would contain a separator and silently disable
completion.
Acceptance is dispatch-driven throughout -- a real C-x C-f, real typing,
a real RET -- so a dead binding cannot pass vacuously and the Lua
lifecycle accept(), which bypasses the path interactive input takes, is
not used.
`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.
Review round 1 flagged that neither ledger knew about this branch, and
`docs/active-work.md`'s stated job is exactly the volatile open lanes.
Records the branch, base, framing revision, what Stage 1 ships, the
discharged Q#LN1 obligation, the Q#LN4 blast radius, and the four
implementation findings that are not in the framing (the `warning`
colour collision with `number`, `Some(1)` resolving to `@function`
rather than `@constructor`, the `module > declaration > def` nesting,
and `injection_aliases` being a write-only proxy). Also carries forward
the two Stage 2 corrections the framing already holds, since that lane
starts next.
Deliberately ADDITIVE ONLY -- one new section, zero deleted lines. PR
#156 is open against both this file and `docs/agent-handoff.md` and owns
the snapshot header, the canonical-base line, and the bottom-panel
lane's status. Touching those here would collide with a PR already in
review, which is the "frozen reviewed PRs do not absorb moving
overlapping work" lesson from #135/#137.
`docs/agent-handoff.md` is deliberately untouched: its §1 snapshot
describes what is ON `main`, so it gets updated when this merges, not
while it is in review.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review finding: acc12's server-list assertion could not fail for the
regression class it was written to catch. The shared `editor()` helper
runs `pmacs.lsp.config = {}` before any buffer opens, so
`#pmacs.lsp.list() == 0` holds for every language regardless of what
Stage 1 ships -- a Stage-3 front-run that added
`pmacs.lsp.config.lean4` in a builtin runtime file would have slipped
straight past it. The same vacuous-assertion shape as #155 R2.
acc12 now asserts the actual claim against a PRISTINE `EditorState`,
before any config wipe: no builtin runtime file defines
`pmacs.lsp.config.lean4`. A non-vacuity check pins that the same lookup
finds `pmacs.lsp.config.rust`, so this cannot pass merely because the
table is empty or absent.
Bite-verified: adding `pmacs.lsp.config.lean4 = ... { command = "lake",
args = { "serve" } }` to `builtin/runtime/lsp.lua` fails the test; the
stub was reverted.
The process-list half is kept and its comment now says why it survives
the wipe: a direct probe spawn from a future `lean.lua` shows up there
whatever `pmacs.lsp.config` contains.
Also fixes a stale column in a `highlight.rs` comment -- the Lua table
brace in `local t = {}` is at col 10, which is what the code already
used.
Gates rerun: fmt and strict workspace clippy clean; 1,826 default +
2,003 CRDT library tests; lean4 Stage 1 9/9; M4 121; required GPU 152;
isolated-config workspace sweep 3,150 across 90 suites; diff check clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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>
`constructor`, `character`, `keyword.conditional`, and `warning` are the
captures the Lean query uses that the global theme table lacked. Three of
them are not Lean-only, so this is a deliberate retro-paint of already
shipped languages -- the #146 lesson applied on purpose rather than
discovered afterwards.
The blast radius, measured rather than assumed:
* `constructor` reaches SEVEN language entries, not four. The emitting
crates are rust, lua, python and javascript, but
`tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated base-first
into javascriptreact, typescript and typescriptreact as well.
* Its shape is not "constructors". rust/python/javascript tag every
capitalized identifier (`#match? "^[A-Z]"`); lua tags every
table-constructor brace. So this recolors `None`, every class-cased
name, and every Lua `{}` -- all of which rendered as unstyled default
text before.
* `character` reaches zig only; `keyword.conditional` reaches cmake and
zig, which previously flattened it to `keyword`; `warning` reaches no
other grammar and exists for Lean's `sorry`.
The alternative was an in-repo overlay renaming the captures (the #144
LaTeX pattern), which forks a 213-line query we would then own and
hand-merge on every crate bump. There is no middle option: styling Lean's
constructors without touching the other seven entries requires renaming
the capture, which requires the overlay.
Pinned in both directions, per #146:
* the positive breadth pin asserts all seven entries emit
`@constructor` at the QUERY level -- chosen over per-fixture checks
because the base-query composition is the fragile part; if someone
stops concatenating the JS base into `typescript`, this fails while
any single-language fixture still passes;
* two grid pins prove the theme entry reaches painted cells, and a
third records that a variant in CALL position keeps `@function` --
the difference between "capitalized identifiers recolor" and "enum
variants recolor", only the first of which is true;
* the negative pin asserts ten languages (markdown, json, yaml, html,
css, c, cpp, go, toml, bash) emit none of the four names, with a
non-vacuity check that the same predicate finds each name where it
does occur.
Rev 1 of the framing named Lua and Python in that negative pin, which was
a self-contradiction -- both are retro-painted by `constructor`, so the
assertion would have been vacuous in the #155 R2 shape. Review round 1
caught it.
Full lib suite (1,824) and the required-GPU gate (152) pass unchanged, so
no existing assertion depended on these captures being unstyled.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds `arborium-lean` 2.18 and one `BUILTIN_LANGUAGES` entry, closing the
framing's open verification obligation on the crate choice.
Why this crate and not `tree-sitter-lean4` (Q#LN1): the latter depends on
`tree-sitter = "0.25"` directly rather than the shared
`tree-sitter-language` ABI crate, and `^0.25` excludes our 0.26, so it
would fork the graph exactly as the dead `tree-sitter-dockerfile` does.
It also exports only `pub fn language()` while its README advertises a
`LANGUAGE` const that does not exist, and its package `include` omits
`queries/` so it ships no highlights at all. `arborium-lean` uses
`tree-sitter-language 0.1` as its sole runtime dep, ships a pre-generated
ABI-15 parser plus scanner, and exports real query constants.
`cargo tree -d` reports no duplicate `tree-sitter`.
The entry is named `lean4`, not `lean` (Q#LN2): `ensure_server` passes
`LanguageEntry.name` through as the `didOpen` language_id, and the Lean
ecosystem's id is `lean4` -- `lean` is Lean 3, which is end-of-life. It
claims `.lean` only; `.olean` is a compiled binary and `.ilean` is JSON
metadata (Q#LN3).
Four tests. The load-bearing one is `lean4_grammar_loads_and_parses`,
which discharges the half of Q#LN1 that could not be settled by reading:
`arborium-lean` exports `const fn language() -> LanguageFn` rather than
the `LANGUAGE` const every other entry uses, and its README demonstrates
usage against a patched tree-sitter core. Neither is supposed to matter,
but "supposed to" is not evidence. The fixture parses without error, and
-- the part that actually guards a misbuild -- its Unicode operators
produce structure rather than degrading silently: the grammar must see a
`(arrow)` for the arrow, a `(forall)` for the universal quantifier, and a
`(comparison)` for the inequality.
The error-free claim is deliberately scoped to the committed fixture.
Lean's syntax is user-extensible via macros, so a static grammar
mis-parses some legal input by construction; the framing scores that as
bet 3 rather than the doc overselling it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The approved framing for Arc 8, revision 4, after three review rounds.
Seven stages: grammar/mode, multi-root LSP affinity, the Lean language
server, the Unicode input method, the goal view, the #eval output
channel, and module hierarchy. 19 decisions, 64 acceptance criteria.
Committed as this branch first commit per the house workflow; the
implementation of Stage 1 follows.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`dominant_line_shape` averages only the lines in a bucket that have
content, then guarded the result with `bool::then_some`. `then_some`
takes its argument by value, so the `MinimapLineShape` literal --- and
with it `indent_sum / count` --- is evaluated before the `count > 0`
guard is ever consulted. When a bucket holds no contentful lines the
division panics and takes the GPU frontend down.
This is reachable in ordinary use, not at an edge: the bucketing branch
runs whenever a file has more lines than the minimap has pixel rows, and
it is exactly then that a run of blank lines can fill a whole downsampled
row. A whitespace-only line counts as blank too --- `minimap_line_shape`
subtracts the indent from the total, so `content_cols` is zero.
Switch to `bool::then`, which defers the body into a closure so the zero
case short-circuits to `None`. The call site already treats `None` as
"draw no stroke for this row", so no other change is needed.
Three tests, two of which fail against the previous line:
* a 10,000-line all-blank file driven through `minimap_rects`, which
reproduces the original panic through the real downsampling path;
* `dominant_line_shape` on an empty bucket;
* a mixed bucket, asserting the average still ignores blank lines ---
a companion guard so the fix cannot regress into counting the whole
slice.
A comment records why this must not be "simplified" back: clippy's
`unnecessary_lazy_evaluations` pushes in precisely the wrong direction
here, and does not fire on a body that can panic.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
PR #155 review round 2, self-review of the round-2 commit.
The round-2 change labelled "minor" — resolving both arms of
pmacs.window.buffer() through the acting frontend for uniformity — made
the NO-ARGUMENT arm fallible. `acting_frontend` follows the interactive
origin, which can name a frontend that has no registered view: a bare
`dispatch_key` from an unattached peer does exactly that. `selected_window`
then raises "acting frontend has no layout" instead of answering.
Nothing surfaced that error, because the runtime callers do not pcall it.
killring, syntax, autosave, pair, indent and comment all read
pmacs.window.buffer() on ordinary edits, so the raise silently dropped
the operation: kill_ring_acceptance went 30/30 to 25/5, with
frontend_detached_drops_per_frontend_state reporting only "B has kill
state". main is 30/30, and reverting this one file restored it.
The no-arg arm is back on ambient active_buffer_id() and now documents
why that is deliberate rather than an oversight: dispatch sets
active_frontend to the acting frontend before running a command, so the
two agree on every real path, while only the ambient resolver has the
fallback that makes it total. The explicit-window arm keeps its Q#BP11
layout validation, which is what the arc actually needed.
acc19c pins it through the real path — a buffer.after-edit subscriber
reading pmacs.window.buffer() during a viewless peer's dispatch_key —
rather than by calling the binding directly. Bite-verified:
scripts/bite bbe4152 src/lua_bindings/mod.rs --test
bottom_panel_stage1_acceptance -- acc19c goes red with the exact
"acting frontend has no layout" traceback.
The ledger also records two gating facts found on the way: the workspace
sweep must run with an isolated XDG_CONFIG_HOME, because the real user
init.lua installs a local package and the losing race leaks a status
message into painted-frame comparisons; and a latent pre-existing main
bug in the buffer CRDT undo path, which is not this branch's and whose
proptest seed is deliberately not committed here.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012j4omtTMn9v1UfmHQb9ap6
The round-2 peer press landed in the peer's CONTENT area, so it never
reached `arm_window_drag` — the exact path Finding 5 names — and the
case bit nothing. It now presses the peer's own mode-line row, where a
single global drag slot is overwritten (and, since that lone window owns
no boundary, cleared outright).
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>
`TerminalViewStatus.scroll_offset` is the retained rows between the
VIEWPORT and the live tail, so it necessarily tracks viewport height: an
assertion that it survives a panel height change unchanged is either
vacuous or wrong, and it went red once under a loaded sweep for exactly
that reason. Q#BP7's invariant is that the ANCHOR is frozen, so acc32
and acc33 now compare the first visible row's text across the change,
and additionally pin the follow behavior that distinguishes them: a
shrink never re-arms follow, growth reaching the tail does, and growth
with a frozen selection does not.
Both also wait for the child's last line before sampling, so neither
races further output.
Also records the round in docs/active-work.md.
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>
Review finding, verified: rev 2's "no new build cost" was true only under
an unstated condition. ttf-parser re-exports `math` behind
`#[cfg(feature = "opentype-layout")]`, and it is compiled today only
because fontdb requests that feature — with `default-features = false` and
a set that is NOT ttf-parser's own default (fontdb's adds no-std-float and
omits std). A plain `ttf-parser = "0.25"` therefore unions std in and
forces a one-time rebuild of ttf-parser, fontdb, cosmic-text and glyphon.
Record the zero-rebuild spelling, `default-features = false, features =
["opentype-layout"]`, in Tier 3 §A and in the component table, so the
Tier 3 implementer declares it deliberately rather than tripping over it.
The C1 row points at the detail rather than repeating it.
Also note in the header that every anchor was re-checked at f07b75b. The
scout pin stays at ddaa80d because that is when the scouting happened;
#153 landed between the two and is test-only, moving no anchor cited here.
Framing only; no implementation, no runtime code.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Levi Neuwirth