fix(lean): repair every buffer and retire every server on fallback
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.
This commit is contained in:
parent
73587b0e37
commit
7c37bdc514
|
|
@ -132,6 +132,7 @@ local probe = {
|
|||
-- when the server initializes, because a late
|
||||
-- version verdict still has to retire it
|
||||
armed = false, -- the target buffer + primary have been captured
|
||||
repaired = {}, -- buffer key -> repair attempted (at most once)
|
||||
saw_initialized = false,
|
||||
}
|
||||
|
||||
|
|
@ -149,6 +150,16 @@ local function configured_command()
|
|||
return "`" .. tostring(cmd) .. "`"
|
||||
end
|
||||
|
||||
-- The fallback command, for status text.
|
||||
local function fallback_name()
|
||||
local args = M._fallback.args or {}
|
||||
if #args > 0 then
|
||||
return "`" .. tostring(M._fallback.command) .. " "
|
||||
.. table.concat(args, " ") .. "`"
|
||||
end
|
||||
return "`" .. tostring(M._fallback.command) .. "`"
|
||||
end
|
||||
|
||||
local function report(msg)
|
||||
-- COHERENCE §1.2: background work must leave an attributed trace.
|
||||
-- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error`
|
||||
|
|
@ -232,8 +243,6 @@ end
|
|||
|
||||
-- Retire the failed server, swap the command, then rebuild the
|
||||
-- attachment on the buffer that started this.
|
||||
local try_reattach
|
||||
|
||||
-- Retire `sid` so it cannot come back. **Which call to use depends on
|
||||
-- the state, and using the wrong one is worse than doing nothing:**
|
||||
--
|
||||
|
|
@ -263,67 +272,85 @@ local function retire_server(sid)
|
|||
end
|
||||
end
|
||||
|
||||
-- Retire EVERY Lean server, not just the one that failed.
|
||||
--
|
||||
-- `pmacs.lsp.config.lean4` is a single global entry, so swapping its
|
||||
-- command invalidates every server spawned from the old one — and
|
||||
-- Q#LN15 gives one server per project root, so there can be several.
|
||||
-- Retiring only the server that happened to fail left the others live
|
||||
-- and every buffer attached to them stranded on a command the config no
|
||||
-- longer names.
|
||||
local function retire_all_lean_servers()
|
||||
local ok, rows = pcall(pmacs.lsp.list)
|
||||
if not ok or not rows then return end
|
||||
local ids = {}
|
||||
for _, info in ipairs(rows) do
|
||||
if info.language_id == "lean4" then ids[#ids + 1] = info.id end
|
||||
end
|
||||
for _, id in ipairs(ids) do retire_server(id) end
|
||||
end
|
||||
|
||||
-- Rebuild the ACTIVE buffer's attachment if it is Lean and stale.
|
||||
--
|
||||
-- `_attach_buffer` is an active-buffer-only seam, so a global config
|
||||
-- swap cannot be applied to every open buffer at once. It is applied
|
||||
-- lazily instead: whenever a Lean buffer becomes the active one, if its
|
||||
-- record points at a server that is gone or terminal, it is rebuilt.
|
||||
--
|
||||
-- **At most one attempt per buffer.** Without that bound a fallback
|
||||
-- that also fails to spawn would retry every tick forever with nothing
|
||||
-- reported — the round-2 defect, which a general repair loop would
|
||||
-- otherwise reintroduce for every buffer instead of just one.
|
||||
--
|
||||
-- A `shutting-down` server is deliberately NOT treated as stale: it is
|
||||
-- still live by `server_is_live`'s reckoning, so `attach_buffer` would
|
||||
-- early-return the stale record and burn this buffer's single attempt
|
||||
-- on a no-op. Skipping leaves the attempt for a later tick, once the
|
||||
-- retirement has actually landed.
|
||||
local function repair_active_if_stale()
|
||||
if not probe.latched then return end
|
||||
local buf = pmacs.window.buffer()
|
||||
if not buf then return end
|
||||
local key = tostring(buf)
|
||||
if probe.repaired[key] then return end
|
||||
local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf)
|
||||
if not ok_lang or lang ~= "lean4" then return end
|
||||
|
||||
local rec = pmacs.lsp.active_attachment()
|
||||
local stale
|
||||
if not rec then
|
||||
stale = true
|
||||
else
|
||||
local kind = server_state_kind(rec.server)
|
||||
stale = (kind == nil or kind == "crashed" or kind == "stopped")
|
||||
end
|
||||
if not stale then return end
|
||||
|
||||
probe.repaired[key] = true
|
||||
local ok, fresh = pcall(pmacs.lsp._attach_buffer)
|
||||
if not ok or not fresh then
|
||||
report("LSP: lean4 fallback " .. fallback_name()
|
||||
.. " did not start either")
|
||||
end
|
||||
end
|
||||
|
||||
local function fire_latch(sid, why)
|
||||
if probe.latched then return end
|
||||
probe.latched = true
|
||||
probe.watching = nil
|
||||
if sid then retire_server(sid) end
|
||||
if not swap_to_fallback() then
|
||||
report("LSP: lean4 " .. why)
|
||||
-- Still retire: the servers are broken whether or not a replacement
|
||||
-- command was installed, and leaving them live would keep the
|
||||
-- restart machinery running against a command known to fail.
|
||||
retire_all_lean_servers()
|
||||
return
|
||||
end
|
||||
report("LSP: lean4 " .. why .. "; falling back to `"
|
||||
.. tostring(M._fallback.command) .. "`")
|
||||
-- **Spawn the replacement and re-point the buffer at it.** Swapping
|
||||
-- the config is not a fallback on its own: nothing re-fires an attach
|
||||
-- on a config change and `attach_buffer` early-returns for a live
|
||||
-- attachment, so without this the buffer stays bound to the server we
|
||||
-- just retired and the user has a config edit and no language server.
|
||||
--
|
||||
-- The rebuild waits for two things, and conflating them is what made
|
||||
-- round 2 wrong in two ways at once:
|
||||
-- 1. the retired server actually reaching a terminal state (or
|
||||
-- being gone) — `stop` leaves `shutting-down`, which
|
||||
-- `server_is_live` counts as LIVE, so attaching before then
|
||||
-- early-returns the stale record and the swap silently no-ops;
|
||||
-- 2. the buffer that started this being the ACTIVE one, because
|
||||
-- `_attach_buffer` is an active-buffer-only seam. The verdict
|
||||
-- arrives asynchronously, so the user may well be somewhere else
|
||||
-- by then — and "some attachment now names a different server"
|
||||
-- is satisfied by an unrelated Rust buffer, which would clear the
|
||||
-- retry while leaving the Lean buffer stale forever.
|
||||
probe.reattach_from = sid and tostring(sid) or false
|
||||
try_reattach()
|
||||
end
|
||||
|
||||
-- Returns true when there is nothing left to do: either the initiating
|
||||
-- buffer is attached to the replacement, or the replacement itself
|
||||
-- failed and that has been reported.
|
||||
function try_reattach()
|
||||
if probe.reattach_from == nil then return true end
|
||||
-- (2) Wait for the initiating buffer to be the active one.
|
||||
local buf = pmacs.window.buffer()
|
||||
if not buf or not probe.buf_key or tostring(buf) ~= probe.buf_key then
|
||||
return false
|
||||
end
|
||||
-- (1) Wait for the retired server to stop counting as live.
|
||||
if probe.reattach_from then
|
||||
local kind = server_state_kind_for_key(probe.reattach_from)
|
||||
if kind ~= nil and kind ~= "crashed" and kind ~= "stopped" then
|
||||
return false
|
||||
end
|
||||
end
|
||||
-- Both conditions met: attempt the replacement EXACTLY ONCE. Cleared
|
||||
-- first so a failing fallback cannot retry every tick forever —
|
||||
-- acceptance 27 promises a second failure surfaces rather than loops.
|
||||
probe.reattach_from = nil
|
||||
local ok, rec = pcall(pmacs.lsp._attach_buffer)
|
||||
if not ok or not rec then
|
||||
report("LSP: lean4 fallback `" .. tostring(M._fallback.command)
|
||||
.. "` did not start either")
|
||||
return false
|
||||
end
|
||||
return true
|
||||
retire_all_lean_servers()
|
||||
report("LSP: lean4 " .. why .. "; falling back to " .. fallback_name())
|
||||
-- Repair what is in front of the user now; everything else is
|
||||
-- repaired lazily as it becomes active (see `repair_active_if_stale`).
|
||||
repair_active_if_stale()
|
||||
end
|
||||
|
||||
local function drain_probe()
|
||||
|
|
@ -566,19 +593,26 @@ pmacs.hook.add("buffer.after-load", function()
|
|||
end
|
||||
end)
|
||||
|
||||
-- A buffer switch is the moment a stale Lean buffer becomes visible, so
|
||||
-- repair immediately rather than waiting for the next tick. lsp.lua's
|
||||
-- own `after-switch` subscription re-pushes views but does NOT rebuild a
|
||||
-- stale attachment, so nothing else covers this.
|
||||
pmacs.hook.add("buffer.after-switch", function()
|
||||
repair_active_if_stale()
|
||||
end)
|
||||
|
||||
pmacs.hook.add("process.after-tick", function()
|
||||
drain_probe()
|
||||
poll_latch()
|
||||
-- Keep trying until the stopped server is really gone; see the note in
|
||||
-- `fire_latch`.
|
||||
if probe.reattach_from ~= nil then try_reattach() end
|
||||
-- Repair the active buffer if the latch invalidated it. Cheap when
|
||||
-- there is nothing to do, and bounded to one attempt per buffer.
|
||||
repair_active_if_stale()
|
||||
end)
|
||||
|
||||
-- Test seam: acceptance drives the latch deterministically rather than
|
||||
-- waiting on real process timing. Not part of the public surface.
|
||||
M._probe = probe
|
||||
M._fire_latch = fire_latch
|
||||
M._try_reattach = try_reattach
|
||||
M._version_below_3_1 = version_below_3_1
|
||||
|
||||
pmacs.lean = M
|
||||
|
|
|
|||
|
|
@ -265,7 +265,7 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in
|
||||
`src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`,
|
||||
a `leanprogress` mode plus `waitForDiagnostics` validation on
|
||||
`pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (28 tests).
|
||||
`pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (31 tests).
|
||||
No protocol change.
|
||||
- **Stage 1's acceptance 12 is half superseded and was rewritten, not
|
||||
deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a
|
||||
|
|
@ -319,6 +319,21 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
are one fact and are now armed together, once. Plus a P2: the failure
|
||||
message hardcoded `lake serve` after the latch became
|
||||
command-agnostic, sending wrapper users to debug the wrong binary.
|
||||
- **Round-4 review: one P1, and it is the same defect a 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 per project root. Rounds 1–3 each fixed the repair
|
||||
for one buffer and one server; round 4 is "repair the armed target,
|
||||
strand the rest". The shape that finally holds: retire ALL `lean4`
|
||||
servers on latch, and repair each buffer **lazily and at most once**
|
||||
when it becomes active (`buffer.after-switch` + the tick), because
|
||||
`_attach_buffer` is active-buffer-only and cannot reach the others.
|
||||
The per-buffer once-only bound is what stops a failing fallback
|
||||
retrying forever — the round-2 defect a naive global repair loop would
|
||||
have reintroduced for every buffer instead of one. Plus a P2: the
|
||||
argument-inclusive attribution was implemented but pinned only by
|
||||
"contains the command name", so a mutation dropping every argument
|
||||
still passed.
|
||||
- **DURABLE LESSON — "the test that passes" vs "the test that
|
||||
discriminates."** Six tests across three rounds were written, run
|
||||
green, and only bite-testing showed they pinned nothing. **Carry this
|
||||
|
|
@ -341,8 +356,20 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
6. A fixture whose `serve` sleeps can never let the primary initialize
|
||||
first, so it cannot reach the ordering where a late verdict must
|
||||
retire a LIVE server.
|
||||
7. Asserting on a field that no longer exists (`_probe.reattach_from`
|
||||
after a refactor) reads as nil and passes for nothing. Assert
|
||||
positive facts — a count, a command string — not absences.
|
||||
Rule: **a test is not evidence until the mutation it targets has been
|
||||
shown to fail it.**
|
||||
- **SECOND DURABLE LESSON — a scope error repeats until the scope is
|
||||
named.** The "fallback silently does not happen" defect came back four
|
||||
times: no re-attach; re-attach cleared by an unrelated buffer;
|
||||
re-attach satisfied by the server being replaced; re-attach of one
|
||||
buffer while the others stay stale. Every fix was locally correct and
|
||||
none asked *what does this config swap invalidate?* — the answer being
|
||||
every Lean buffer and every Lean server, because the config entry is
|
||||
global and servers are per-root. **When a change edits shared state,
|
||||
enumerate everything derived from it before repairing anything.**
|
||||
- **SUBSTRATE BUG FOUND, not fixed here (framing §6).**
|
||||
`LspManager::stop` on an ALREADY-terminal server takes its
|
||||
not-initialized branch, terminates the dead process and sets
|
||||
|
|
@ -368,9 +395,9 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
server-failure latch covers the rest.
|
||||
- Verification on this branch: `cargo fmt --check` clean; strict
|
||||
workspace Clippy clean; 1,826 default + 2,003 CRDT library tests;
|
||||
lean4 server 28/28; lean4 stage 1 9/9; dispatch seams 15/15;
|
||||
lean4 server 31/31; lean4 stage 1 9/9; dispatch seams 15/15;
|
||||
multi-root 13/13; M4 121; required GPU 155; **isolated-config
|
||||
workspace sweep 3,217 across 94 suites, zero failures**;
|
||||
workspace sweep 3,220 across 94 suites, zero failures**;
|
||||
`git diff --check` clean. (Round 1 of
|
||||
this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the
|
||||
fixes were pushed. The ledger's protocol is that verification
|
||||
|
|
|
|||
|
|
@ -1010,9 +1010,19 @@ fn r2_a_failing_fallback_is_reported_once_and_does_not_retry_forever() {
|
|||
"a failing fallback surfaces rather than retrying silently; saw \
|
||||
{status:?}"
|
||||
);
|
||||
// And the retry state is cleared, so it is not looping.
|
||||
let pending: String = eval(&state, "return tostring(pmacs.lean._probe.reattach_from)");
|
||||
assert_eq!(pending, "nil", "the retry is retired, not spinning");
|
||||
// And the repair was ATTEMPTED and recorded, so it is bounded rather
|
||||
// than spinning. Asserting on a field that no longer exists would
|
||||
// read as nil and pass for nothing — the vacuity shape this branch
|
||||
// keeps producing, so the assertion is on a positive count.
|
||||
let attempted: i64 = eval(
|
||||
&state,
|
||||
"local n = 0 for _ in pairs(pmacs.lean._probe.repaired) do n = n + 1 end return n",
|
||||
);
|
||||
assert_eq!(
|
||||
attempted, 1,
|
||||
"exactly one repair attempt was made and recorded, so a failing \
|
||||
fallback cannot retry every tick forever"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
|
|
@ -1240,3 +1250,124 @@ fn r3_a_failing_wrapper_is_named_truthfully_not_as_lake_serve() {
|
|||
"and does not attribute the failure to `lake serve`; saw {status:?}"
|
||||
);
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Round-4 review — the config swap is GLOBAL, so one repaired buffer is
|
||||
// not a fallback. Both fail against 73587b0.
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
#[test]
|
||||
fn r4_every_open_lean_buffer_is_repaired_not_just_the_armed_one() {
|
||||
// `pmacs.lsp.config.lean4` is a single entry; swapping its command
|
||||
// invalidates every buffer attached to the old one. Round 3 repaired
|
||||
// exactly `probe.buf_key` and cleared the retry, leaving every other
|
||||
// open Lean buffer on the retired server while status and config
|
||||
// both said "fell back".
|
||||
let fx = Fixture::new();
|
||||
fx.toolchain("pkg", "v4.9.0\n");
|
||||
let first = fx.write("pkg/A.lean", "def a := 1\n");
|
||||
let second = fx.write("pkg/B.lean", "def b := 2\n");
|
||||
let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0");
|
||||
let mut state = editor(&fx);
|
||||
with_fallback(&state, &lake);
|
||||
|
||||
open(&state, &first);
|
||||
exec(&state, "_G.first_buf = pmacs.window.buffer()");
|
||||
open(&state, &second);
|
||||
exec(&state, "_G.second_buf = pmacs.window.buffer()");
|
||||
tick_for(&mut state, 700);
|
||||
|
||||
// The armed (first) buffer.
|
||||
exec(&state, "pmacs.window.switch_buffer(_G.first_buf)");
|
||||
tick_for(&mut state, 500);
|
||||
assert_eq!(
|
||||
attached_command(&state),
|
||||
fake_lsp_path(),
|
||||
"the armed buffer is repaired"
|
||||
);
|
||||
|
||||
// And the OTHER one, which round 3 stranded.
|
||||
exec(&state, "pmacs.window.switch_buffer(_G.second_buf)");
|
||||
tick_for(&mut state, 500);
|
||||
assert_eq!(
|
||||
attached_command(&state),
|
||||
fake_lsp_path(),
|
||||
"every open Lean buffer ends up on the fallback — repairing only \
|
||||
the armed target leaves this one on the retired server"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn r4_a_second_project_roots_server_is_also_retired() {
|
||||
// Q#LN15 gives one server per project root, so a swap can invalidate
|
||||
// several. `probe.primary` names only the first; retiring only that
|
||||
// leaves the second root's server live on a command the config no
|
||||
// longer names.
|
||||
let fx = Fixture::new();
|
||||
fx.toolchain("one", "v4.9.0\n");
|
||||
fx.toolchain("two", "v4.9.0\n");
|
||||
let a = fx.write("one/A.lean", "def a := 1\n");
|
||||
let b = fx.write("two/B.lean", "def b := 2\n");
|
||||
let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0");
|
||||
let mut state = editor(&fx);
|
||||
with_fallback(&state, &lake);
|
||||
|
||||
open(&state, &a);
|
||||
open(&state, &b);
|
||||
// Two roots, two servers, before any verdict lands.
|
||||
let before: i64 = eval(&state, "return #pmacs.lsp.list()");
|
||||
assert_eq!(before, 2, "precondition: one server per root");
|
||||
|
||||
tick_for(&mut state, 900);
|
||||
|
||||
// No server may still be running the retired command.
|
||||
let stale_live: i64 = eval(
|
||||
&state,
|
||||
&format!(
|
||||
r#"
|
||||
local n = 0
|
||||
for _, s in ipairs(pmacs.lsp.list()) do
|
||||
if tostring(s.command) == "{}" then
|
||||
local k = s.state and s.state.kind
|
||||
if k ~= "stopped" and k ~= "crashed" then n = n + 1 end
|
||||
end
|
||||
end
|
||||
return n
|
||||
"#,
|
||||
lua_str(&lake)
|
||||
),
|
||||
);
|
||||
assert_eq!(
|
||||
stale_live, 0,
|
||||
"every Lean server spawned from the old command is retired, not \
|
||||
just the one the probe happened to name"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn r4_attribution_names_the_exact_command_and_its_arguments() {
|
||||
// Round 3 implemented argument-inclusive attribution but pinned only
|
||||
// "contains my-lean-wrapper" and "does not contain lake serve" — a
|
||||
// mutation dropping every argument still passed.
|
||||
let fx = Fixture::new();
|
||||
fx.toolchain("pkg", "v4.9.0\n");
|
||||
let file = fx.write("pkg/A.lean", "def a := 1\n");
|
||||
let absent = fx.dir("bin/my-lean-wrapper");
|
||||
let mut state = editor(&fx);
|
||||
with_fallback(&state, &absent);
|
||||
exec(
|
||||
&state,
|
||||
"pmacs.lsp.config.lean4.args = { \"serve\", \"--quiet\" }",
|
||||
);
|
||||
|
||||
open(&state, &file);
|
||||
settle(&mut state);
|
||||
|
||||
let status = state.core.borrow().status.clone();
|
||||
let expected = format!("`{} serve --quiet`", absent.display());
|
||||
assert!(
|
||||
status.contains(&expected),
|
||||
"the status names the exact configured command AND its arguments;\n \
|
||||
want substring: {expected}\n saw: {status:?}"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue