diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 8f3b339..546e123 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -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 diff --git a/docs/active-work.md b/docs/active-work.md index 6cdac4f..e4e1064 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -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 diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index db708f1..32cdf3e 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -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:?}" + ); +}