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.
Levi Neuwirth