From cdaea66203aed112a11e3f3b729a2cc212197904 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 18:03:29 -0400 Subject: [PATCH] fix(lean): make the fallback actually produce a working server MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- builtin/runtime/lean.lua | 163 +++++++++++--- builtin/runtime/lsp.lua | 18 ++ docs/active-work.md | 40 +++- docs/lean4-mode-framing.md | 24 ++- src/bin/pmacs_fake_lsp.rs | 33 +++ tests/lean4_server_acceptance.rs | 350 +++++++++++++++++++++++-------- 6 files changed, 510 insertions(+), 118 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 3fe73da..dd98892 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -142,6 +142,19 @@ end -- `lake serve` below 3.1.0 starts a server that cannot answer, which is -- worse than failing: `lean4-mode` probes for exactly this and falls -- back to `lean --server`. Parses the leading `x.y` of a version line. +-- State kind for `sid`, or nil if the manager has forgotten it. +local function server_state_kind(sid) + local skey = tostring(sid) + local ok, rows = pcall(pmacs.lsp.list) + if not ok or not rows then return nil end + for _, info in ipairs(rows) do + if tostring(info.id) == skey then + return info.state and info.state.kind + end + end + return nil +end + local function version_below_3_1(text) local major, minor = text:match("(%d+)%.(%d+)") if not major then return false end @@ -150,15 +163,27 @@ local function version_below_3_1(text) return major == 3 and minor < 1 end +-- What the latch falls back TO. A table rather than a literal so the +-- acceptance suite can point it at a stand-in server and drive the real +-- latch path end to end, instead of asserting on a config mutation that +-- proves nothing about whether a server ever starts. +M.fallback = { command = "lean", args = { "--server" } } + -- Swap `command`/`args` ONLY. A wholesale table replacement would -- silently discard a user's `env` / `settings` / `init_options` / `root` -- from `init.lua` at exactly the moment they are least likely to notice. -local function swap_to_lean_server() +-- +-- The only guard is idempotence — already-the-fallback means nothing to +-- do. It deliberately does NOT refuse when the command is user-supplied: +-- the latch fires only when the configured Lean server actually failed +-- to start, and one visible fallback attempt beats leaving the user with +-- no server at all. `probe.latched` is what keeps it to exactly one. +local function swap_to_fallback() local cfg = pmacs.lsp.config.lean4 if not cfg then return false end - if cfg.command ~= "lake" then return false end - cfg.command = "lean" - cfg.args = { "--server" } + if cfg.command == M.fallback.command then return false end + cfg.command = M.fallback.command + cfg.args = M.fallback.args return true end @@ -172,16 +197,66 @@ end -- producing a loop the latch cannot see the end of. `pmacs.lsp.stop` -- sets `restart = Never` on the way out, which is what disarms it. The -- fallback is therefore a FRESH server, not a restart of the old one. +local try_reattach + local function fire_latch(sid, why) if probe.latched then return end probe.latched = true - if sid then pcall(pmacs.lsp.stop, sid) end - if swap_to_lean_server() then - report("LSP: lean4 " .. why .. "; falling back to `lean --server`") - else - report("LSP: lean4 " .. why) - end probe.watching = nil + -- **Only stop a server that is not ALREADY terminal**, and this is + -- load-bearing rather than tidy. `LspManager::stop` on a crashed + -- client takes its not-initialized branch: it terminates the + -- (already-dead) process and sets `ShuttingDown { .. None }`, with the + -- comment "the next exit observation cleans up" — but the exit was + -- already observed, which is what made it `Crashed`. No further event + -- arrives, so the client stays in `ShuttingDown` forever: + -- `server_is_live` counts it as LIVE (neither crashed nor stopped) so + -- `attach_buffer` never rebuilds, and `LspManager::forget` refuses it + -- for not being terminal. Stopping a dead server is what makes it + -- un-replaceable. Recorded as a substrate deferral in the framing §6. + if sid then + local kind = server_state_kind(sid) + if kind and kind ~= "crashed" and kind ~= "stopped" then + pcall(pmacs.lsp.stop, sid) + end + end + if not swap_to_fallback() then + report("LSP: lean4 " .. why) + return + end + report("LSP: lean4 " .. why .. "; falling back to `" + .. tostring(M.fallback.command) .. "`") + -- **Spawn the replacement and re-point the buffer at it.** Stopping + -- and rewriting 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 stopped and the user is left with + -- a config edit and no language server. Round 1 shipped exactly that, + -- with an acceptance test that asserted every server was terminal — + -- i.e. that pinned the absence of the fallback it claimed to check. + -- + -- **Retried on the tick, not done inline**, and that is not caution: + -- `pmacs.lsp.stop` sends shutdown+exit and the state becomes + -- `shutting-down`, which `server_is_live` counts as LIVE. So an + -- immediate `_attach_buffer` early-returns the stale record and the + -- swap has no effect — the exact silent no-op this whole path exists + -- to avoid. Retrying until the old server actually reaches a terminal + -- state is what makes the rebuild happen. + probe.reattach_from = sid and tostring(sid) or false + try_reattach() +end + +-- Returns true once the active Lean buffer is attached to a server that +-- is not the one the latch stopped. +function try_reattach() + if probe.reattach_from == nil then return true end + local ok, rec = pcall(pmacs.lsp._attach_buffer) + if not ok or not rec then return false end + if probe.reattach_from and tostring(rec.server) == probe.reattach_from then + return false + end + probe.reattach_from = nil + return true end local function drain_probe() @@ -220,13 +295,17 @@ local function start_probe(root) if probe.started then return end probe.started = true local cfg = pmacs.lsp.config.lean4 - if not cfg or cfg.command ~= "lake" then return end + if not cfg or not cfg.command then return end + -- Probe the binary we would actually run, not the literal string + -- "lake": a user pointing `command` at a wrapper or an absolute path + -- should have THAT probed, and a hardcoded name would silently probe + -- something else (or nothing). local spec = { -- COHERENCE §9: `ProcessSpec.label` is the only identity a process -- carries, and it is what `pmacs.process.list` renders. A user -- wondering why their editor touched `lake` finds an owner here. label = "lean:lake-version-probe", - command = "lake", + command = cfg.command, args = { "--version" }, stdin = "null", } @@ -275,12 +354,20 @@ end -- does not apply. Resolves when the server has finished elaborating. -- Awaited through Stage 3a's response seam. -- +-- **`version` is required, not optional.** Lean's +-- `WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0, +-- `src/Lean/Data/Lsp/Extra.lean`), and the request is how the client +-- says *which* revision of the document it wants elaboration for. +-- Sending only `uri` is a malformed request against a real server; it +-- happened to look fine here because the fake server echoes any +-- payload. Callers pass the attachment's current `version`. +-- -- `fn(err)` is called with nil on success. Registering the one-shot -- requires the server to have an attached buffer — see the note on -- `pmacs.lsp.on_response`; every caller here comes from an attachment. -function M.wait_for_diagnostics(sid, uri, fn) +function M.wait_for_diagnostics(sid, uri, version, fn) local ok, rid = pcall(pmacs.lsp.send_request, sid, - "textDocument/waitForDiagnostics", { uri = uri }) + "textDocument/waitForDiagnostics", { uri = uri, version = version }) if not ok then if fn then pcall(fn, tostring(rid)) end return nil @@ -303,7 +390,7 @@ pmacs.command.define { return end pmacs.editor.set_status("lean: elaborating…") - M.wait_for_diagnostics(rec.server, rec.uri, function(err) + M.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) if err then pmacs.editor.set_status("lean: " .. tostring(err)) else @@ -327,27 +414,53 @@ end) -- Wiring -------------------------------------------------------------- --- Runs after `lsp.lua`'s own `buffer.after-load` subscription, so the --- attachment already exists. The attachment's `language` IS the Lean --- test — no separate major-mode lookup, which would be a second source --- of truth for the same question. +-- Runs after `lsp.lua`'s own `buffer.after-load` subscription. +-- +-- **Keyed on the buffer's LANGUAGE, not on an attachment existing.** +-- Round 1 keyed on `active_attachment()` and returned early when it was +-- nil — which silently excluded the single most likely real-world +-- failure: `lake` not installed. `ensure_server` pcalls the spawn and +-- returns nil on ENOENT, so `attach_buffer` produces no record at all, +-- so the probe never started and the latch never armed. The case the +-- fallback exists for was the one case it could not see. pmacs.hook.add("buffer.after-load", function() - local rec = pmacs.lsp.active_attachment() - if not rec or rec.language ~= "lean4" then return end + local buf = pmacs.window.buffer() + if not buf then return end + local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf) + if not ok_lang or lang ~= "lean4" then return end + if not probe.started then local path = pmacs.editor.file_path() start_probe(path and M.root_for(path) or nil) end - -- Watch only the FIRST Lean server: the latch is per session. - if not probe.latched and not probe.saw_initialized - and probe.watching == nil then - probe.watching = rec.server + + local rec = pmacs.lsp.active_attachment() + if rec and rec.language == "lean4" then + -- Watch only the FIRST Lean server: the latch is per session. + if not probe.latched and not probe.saw_initialized + and probe.watching == nil then + probe.watching = rec.server + end + return + end + + -- No attachment for a Lean buffer means `ensure_server` could not + -- spawn at all — a synchronous ENOENT, already swallowed upstream. + -- That is not something to wait for; it is the failure itself, and + -- the only place it is still observable. + if not probe.latched then + fire_latch(nil, "`" .. tostring( + pmacs.lsp.config.lean4 and pmacs.lsp.config.lean4.command) + .. "` could not be started") end 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 end) -- Test seam: acceptance drives the latch deterministically rather than diff --git a/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua index fd44f1a..0749cfa 100644 --- a/builtin/runtime/lsp.lua +++ b/builtin/runtime/lsp.lua @@ -893,6 +893,24 @@ function pmacs.lsp.active_attachment() return attachments[tostring(buf)] end +-- Re-run the attach for the ACTIVE buffer, rebuilding it against the +-- current `pmacs.lsp.config`. +-- +-- Exists for the Arc 8 Stage 3b fallback latch (Q#LN7): after that latch +-- stops a server that failed to start and rewrites `config.lean4`, +-- something has to actually spawn the replacement and re-point the +-- buffer at it. Nothing else does — `attach_buffer` early-returns for a +-- live attachment, and no hook re-fires on a config change, so without +-- this the buffer stays bound to the stopped server and the "fallback" +-- is a config edit with no effect. +-- +-- Deliberately keyed on the active buffer, matching `attach_buffer`'s +-- own use of `active_buffer_path()`; it is not a general re-attach for +-- arbitrary buffers and must not be used as one. +function pmacs.lsp._attach_buffer() + return attach_buffer(pmacs.window.buffer()) +end + -- Arc 4 stage 3: pure modeline projection. This reads the private -- per-buffer attachment map directly so passive split windows report their -- own buffer instead of the focused window. It never attaches, flushes diff --git a/docs/active-work.md b/docs/active-work.md index 99b54ea..1a1e7ae 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -256,12 +256,17 @@ If it does not, stop and repair the remote/fetch configuration. - Same worktree `../pmacs-lean-stage3`, **branched off `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response - seam and `pmacs.fs.canonicalize`, so it is strictly sequential and its - PR must be retargeted to `main` only after #167 merges. (Kill-ring - lesson: retarget stacked child PRs BEFORE merging the parent.) + seam and `pmacs.fs.canonicalize`, so it is strictly sequential. + **Retarget PR #170 to `main` BEFORE merging #167, not after** — the + kill-ring lesson exactly. (Round 1 of this ledger entry stated the + reverse in its first sentence and the correct rule in the next; the + review caught it. A safety rule written twice with opposite senses is + worse than not written.) - Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in - `src/editor.rs`, a `leanprogress` mode on `pmacs_fake_lsp`, and - `tests/lean4_server_acceptance.rs` (17 tests). No protocol change. + `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` (20 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 Stage-3 front-run; 3b is that stage. What survives is the restraint @@ -274,10 +279,29 @@ If it does not, stop and repair the remote/fetch configuration. an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, not content). Discriminator is `read`'s SECOND return; decline only on a non-nil err. Probed on LuaJIT 2.1. -- Four bites recorded, each against the committed tree: bare `io.open` +- Seven bites recorded, each against the committed tree: bare `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a passes; - no canonicalization → symlinked open spawns two servers; no stop - before fallback → acc36 fails. + no canonicalization → symlinked open spawns two servers; 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. +- **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 + `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.** + Lean works around it by checking the state before stopping. +- Round-1 review found four P1s, all real: the latch swapped the config + but never spawned or re-attached (and acc36 *asserted every server was + terminal*, pinning the absence of the fallback); a missing `lake` + bypassed probe and latch entirely because the hook keyed on an + attachment that ENOENT prevents; `waitForDiagnostics` omitted the + `version` Lean requires; and the ledger stated the dangerous stacking + order. - The probe's non-zero exit is deliberately NOT a fallback trigger — §2.9's elan shim makes `lake --version` fail where `lake serve` still works. Only a parseable version below 3.1.0 triggers it; the diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 4869252..fac090b 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1543,6 +1543,20 @@ What remains deferred: which events may be dropped, which is a policy question with user-visible consequences for diagnostics and progress; Stage 3a states the seam's contract around the behavior rather than changing it. +- **`LspManager::stop` on an already-terminal server strands it.** The + not-initialized branch terminates the (already-dead) process and sets + `ShuttingDown { shutdown_request_id: None }` on the premise that "the + next exit observation cleans up" — but for a `Crashed` client the exit + has already been observed, which is what produced that state. No + further event arrives, so the client sits in `ShuttingDown` + permanently: `server_is_live` counts it as live (neither crashed nor + stopped), so `attach_buffer` never rebuilds against it, and + `LspManager::forget` refuses it for not being terminal. **Stopping a + dead server is what makes it un-replaceable.** Found implementing + Stage 3b's latch, which works around it by checking the state before + stopping. The fix belongs in `stop` (treat an already-terminal client + as a no-op, or drive it straight to `Stopped`) and changes behavior + for every language, so it does not ride a Lean PR. - **Forwarding `cfg.restart` through `ensure_server`** — read by `lua_to_lsp_spec`, never set by the spawn table, so silently dropped on every auto-attach (found landing #161). Fixing it changes behavior for @@ -1722,9 +1736,13 @@ the blast radius. channel a user can actually observe; a report added through `pmacs.error` alone must fail this. - **37.** `textDocument/waitForDiagnostics` resolves through the response seam - (Q#LN16). **PATH-and-success-gated live smoke:** if `lake serve` - starts successfully a real elaboration completes and diagnostics - arrive; skipped otherwise, never failed. + (Q#LN16), **carrying both `uri` and `version`** — Lean's + `WaitForDiagnosticsParams` requires the document version, and a fake + server that echoes any payload will hide its absence, so the fixture + must reject a request that omits it. + **PATH-and-success-gated live smoke:** if `lake serve` starts + successfully a real elaboration completes and diagnostics arrive; + skipped otherwise, never failed. These two sections are bulleted with explicit labels rather than numbered, because the split leaves each stage's criteria non-contiguous diff --git a/src/bin/pmacs_fake_lsp.rs b/src/bin/pmacs_fake_lsp.rs index 5f4fab5..67d6620 100644 --- a/src/bin/pmacs_fake_lsp.rs +++ b/src/bin/pmacs_fake_lsp.rs @@ -1083,6 +1083,39 @@ fn main() { }); write_frame(&mut stdout, &resp); } + ("textDocument/waitForDiagnostics", Some(idv)) => { + // Arc 8 Stage 3b: Lean's `WaitForDiagnosticsParams` is + // `{ uri, version }` (v4.9.0 + // `src/Lean/Data/Lsp/Extra.lean`). Validated here rather + // than echoed, because the generic echo arm below + // accepts anything — which is exactly how a client + // sending only `uri` shipped looking correct. A client + // that omits `version`, or sends a non-integer, gets an + // InvalidParams error the way a real server would. + let uri_ok = params + .get("uri") + .and_then(serde_json::Value::as_str) + .is_some(); + let version_ok = params + .get("version") + .and_then(serde_json::Value::as_i64) + .is_some(); + let resp = if uri_ok && version_ok { + serde_json::json!({ + "jsonrpc": "2.0", "id": idv, "result": serde_json::Value::Null + }) + } else { + serde_json::json!({ + "jsonrpc": "2.0", + "id": idv, + "error": { + "code": -32602, + "message": "waitForDiagnostics requires { uri, version }" + } + }) + }; + write_frame(&mut stdout, &resp); + } (_, Some(idv)) => { // Generic echo response. let resp = serde_json::json!({ diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index 13cfcd0..6fe5ed4 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -347,12 +347,85 @@ fn acc26_did_open_carries_the_lean4_language_id() { } // --------------------------------------------------------------------------- -// Acceptance 28 (probe) — the version predicate. +// Acceptance 27 / 28 / 35 / 36 — the probe and the fallback latch. // -// The parse is unit-tested directly because the spawn path is timing- -// bound; the latch's *effect* is pinned separately below. +// **Driven through the production path**, not by calling internals. +// Round 1's versions poked `_fire_latch` directly and asserted on config +// mutation, which proved nothing about whether a server ever starts — +// and acceptance 36 went further and asserted every server was terminal, +// pinning the ABSENCE of the fallback it claimed to test. These go +// `buffer.after-load` -> ticks -> probe drain -> latch -> re-attach, and +// assert the originally opened buffer ends up on a LIVE server. +// +// The stubs are real executables the fixture writes. `M.fallback` is a +// table precisely so it can point at `pmacs_fake_lsp` here. // --------------------------------------------------------------------------- +impl Fixture { + /// An executable shell stub. `serve` sleeps (so the "server" does not + /// die and only the named failure mode is under test); `--version` + /// prints `version_line`. + fn lake_stub(&self, rel: &str, version_line: &str) -> PathBuf { + use std::os::unix::fs::PermissionsExt as _; + let path = self.root.join(rel); + std::fs::create_dir_all(path.parent().unwrap()).unwrap(); + std::fs::write( + &path, + format!( + "#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n echo '{version_line}'\n exit 0\nfi\nexec sleep 300\n" + ), + ) + .unwrap(); + std::fs::set_permissions(&path, std::fs::Permissions::from_mode(0o755)).unwrap(); + path + } +} + +/// Point `command` at `lake_cmd` and the latch's fallback at the fake +/// LSP server, so a fallback that fires produces a server that works. +fn with_fallback(state: &EditorState, lake_cmd: &Path) { + exec( + state, + &format!( + r#" + pmacs.lsp.config.lean4.command = "{}" + pmacs.lsp.config.lean4.args = {{ "serve" }} + pmacs.lean.fallback = {{ command = "{}", args = {{}} }} + "#, + lua_str(lake_cmd), + fake_lsp_path() + ), + ); +} + +/// The active buffer's attached server id, or "none". +fn attached_sid(state: &EditorState) -> String { + eval( + state, + r#" + local rec = pmacs.lsp.active_attachment() + return rec and tostring(rec.server) or "none" + "#, + ) +} + +/// State kind of the active buffer's attached server, or "none". +fn attached_state(state: &EditorState) -> String { + eval( + state, + r#" + local rec = pmacs.lsp.active_attachment() + if not rec then return "none" end + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) == tostring(rec.server) then + return tostring(s.state and s.state.kind) + end + end + return "gone" + "#, + ) +} + #[test] fn acc28_version_predicate_triggers_only_below_3_1() { let fx = Fixture::new(); @@ -374,36 +447,156 @@ fn acc28_version_predicate_triggers_only_below_3_1() { ); } -// --------------------------------------------------------------------------- -// Acceptance 27 / 35 / 36 — the fallback latch. -// --------------------------------------------------------------------------- +#[test] +fn acc28_an_old_lake_falls_back_and_the_buffer_lands_on_a_live_server() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let old_lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &old_lake); + + open(&state, &file); + settle(&mut state); + // The stub's `serve` sleeps rather than dying, so ONLY the probe can + // have caused a fallback here. That isolation is the point. + for _ in 0..40 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } + + assert_eq!( + attached_state(&state), + "initialized", + "an old lake must leave the buffer on a LIVE fallback server, not \ + merely rewrite the config" + ); + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!(cmd, fake_lsp_path(), "the fallback command is in effect"); +} + +#[test] +fn acc28_a_current_lake_does_not_trigger_the_fallback() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let new_lake = fx.lake_stub("bin/lake", "Lake version 3.1.0"); + let mut state = editor(&fx); + with_fallback(&state, &new_lake); + + open(&state, &file); + for _ in 0..20 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + } + + // Non-vacuity against the test above: same harness, same stub shape, + // only the version differs — so a latch that fired unconditionally + // would be caught here. + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!( + cmd, + new_lake.display().to_string(), + "a current lake keeps its command; the probe must not fall back" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!(!latched, "the latch did not arm"); +} + +#[test] +fn acc27_a_missing_lake_falls_back_and_the_buffer_lands_on_a_live_server() { + // The case round 1 could not see at all: `ensure_server` swallows a + // synchronous ENOENT and returns nil, so there is no attachment to + // key off. This is also the most likely real-world failure — a user + // with `lean` but no `lake`. + 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/no-such-lake"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + + open(&state, &file); + for _ in 0..40 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } + + assert_eq!( + attached_state(&state), + "initialized", + "a missing `lake` must fall back to a live server and re-attach \ + the buffer that was already open" + ); + let status = state.core.borrow().status.clone(); + assert!( + status.contains("lean4"), + "and it says so on the status line; saw {status:?}" + ); +} + +#[test] +fn acc27_the_latch_is_one_shot_and_does_not_re_arm() { + 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/no-such-lake"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + + open(&state, &file); + settle(&mut state); + let after_first: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!(after_first, fake_lsp_path(), "the fallback fired once"); + + // A user who deliberately sets something else after the fallback must + // not have it silently replaced by a second firing. + exec(&state, "pmacs.lsp.config.lean4.command = \"user-choice\""); + exec(&state, "pmacs.lean._fire_latch(nil, \"a second failure\")"); + assert_eq!( + eval::(&state, "return pmacs.lsp.config.lean4.command"), + "user-choice", + "the latch never re-arms within a session" + ); +} #[test] fn acc35_latch_preserves_user_config_and_swaps_only_command_and_args() { let fx = Fixture::new(); - let state = editor(&fx); - // A user's init.lua settings, on the shipped shape. + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let absent = fx.dir("bin/no-such-lake"); + let mut state = editor(&fx); + with_fallback(&state, &absent); exec( &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lsp.config.lean4.env = { MYVAR = "1" } + r" pmacs.lsp.config.lean4.settings = { lean = { verbose = true } } pmacs.lsp.config.lean4.init_options = { hasWidgets = false } _G.root_before = pmacs.lsp.config.lean4.root - pmacs.lean._fire_latch(nil, "test") - "#, + ", ); + open(&state, &file); + settle(&mut state); + let after: String = eval( &state, r#" local c = pmacs.lsp.config.lean4 return table.concat({ - tostring(c.command), - tostring(c.args and c.args[1]), - tostring(c.env and c.env.MYVAR), tostring(c.settings and c.settings.lean and c.settings.lean.verbose), tostring(c.init_options and c.init_options.hasWidgets), tostring(c.root == _G.root_before), @@ -411,78 +604,70 @@ fn acc35_latch_preserves_user_config_and_swaps_only_command_and_args() { "#, ); assert_eq!( - after, "lean|--server|1|true|false|true", - "only command/args change; env, settings, init_options and root \ - survive the swap" - ); -} - -#[test] -fn acc27_the_latch_is_one_shot_and_does_not_re_arm() { - let fx = Fixture::new(); - let state = editor(&fx); - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(nil, "first failure") - _G.after_first = pmacs.lsp.config.lean4.command - -- A second failure must not rewrite the command again; if it did, - -- a user who deliberately set something else after the fallback - -- would have it silently replaced. - pmacs.lsp.config.lean4.command = "user-choice" - pmacs.lean._fire_latch(nil, "second failure") - _G.after_second = pmacs.lsp.config.lean4.command - "#, - ); - assert_eq!(eval::(&state, "return _G.after_first"), "lean"); - assert_eq!( - eval::(&state, "return _G.after_second"), - "user-choice", - "the latch never re-arms within a session" + after, "true|false|true", + "settings, init_options and root survive the swap; only \ + command/args change" ); } #[test] fn acc36_latch_stops_the_failing_server_before_spawning_the_fallback() { + // A stub whose `serve` exits immediately: the server dies before + // `initialize` completes, which is the failure the latch polls for. + // `RestartPolicy::OnCrash` would otherwise respawn it forever + // underneath the latch, with no attempt ceiling. + use std::os::unix::fs::PermissionsExt as _; let fx = Fixture::new(); fx.toolchain("pkg", "v4.9.0\n"); let file = fx.write("pkg/A.lean", "def a := 1\n"); + let dying = fx.root.join("bin/dying-lake"); + std::fs::create_dir_all(dying.parent().unwrap()).unwrap(); + std::fs::write( + &dying, + "#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then echo 'Lake version 9.9.9'; exit 0; fi\nexit 3\n", + ) + .unwrap(); + std::fs::set_permissions(&dying, std::fs::Permissions::from_mode(0o755)).unwrap(); + let mut state = editor(&fx); + with_fallback(&state, &dying); open(&state, &file); - settle(&mut state); - assert_eq!(rows(&state).len(), 1, "precondition: one server is up"); + for _ in 0..60 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } - // Fire the latch against the live server, exactly as `poll_latch` - // would. `pmacs.lsp.stop` sets `restart = Never` on the way out — - // which is what prevents `RestartPolicy::OnCrash` from respawning the - // broken command underneath the latch, forever, with no attempt cap. - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(pmacs.lsp.list()[1].id, "failed to start") - "#, + // The load-bearing assertion: the buffer ends up on a LIVE server. + assert_eq!( + attached_state(&state), + "initialized", + "the failing server is stopped and the buffer re-attached to the \ + fallback — not left terminal" ); - settle(&mut state); - - let terminal: bool = eval( + // And the dead one really is stopped, so nothing is respawning it. + let dying_still_running: bool = eval( &state, r#" + local live = tostring(pmacs.lsp.active_attachment().server) for _, s in ipairs(pmacs.lsp.list()) do - local k = s.state and s.state.kind - if k ~= "stopped" and k ~= "crashed" then return false end + if tostring(s.id) ~= live then + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then return true end + end end - return true + return false "#, ); assert!( - terminal, - "the failing server is stopped, not left to be respawned under \ - the latch" + !dying_still_running, + "the failing server is not respawning underneath the latch" ); + assert_ne!(attached_sid(&state), "none"); } // --------------------------------------------------------------------------- @@ -492,23 +677,24 @@ fn acc36_latch_stops_the_failing_server_before_spawning_the_fallback() { #[test] fn acc36a_latch_leaves_a_status_line_trace() { let fx = Fixture::new(); - let state = editor(&fx); - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(nil, "`lake serve` failed to start") - "#, - ); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let absent = fx.dir("bin/no-such-lake"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + + open(&state, &file); + settle(&mut state); + let status = state.core.borrow().status.clone(); assert!( - status.contains("lean4") && status.contains("lean --server"), - "the fallback names itself and what it fell back to; saw {status:?}" + status.contains("lean4") && status.contains("falling back"), + "the fallback names the language and says it fell back; saw {status:?}" ); // The channel assertion is the point (COHERENCE §1.2): a report made // only through `pmacs.error` — undefined in production — would leave - // this empty while every other assertion here still passed. + // this empty while the fallback itself still worked, so the user + // would silently be on a different server than they configured. assert!(!status.is_empty()); } @@ -550,7 +736,7 @@ fn acc37_wait_for_diagnostics_resolves_through_the_response_seam() { r#" _G.settled = "never" local rec = pmacs.lsp.active_attachment() - pmacs.lean.wait_for_diagnostics(rec.server, rec.uri, function(err) + pmacs.lean.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) _G.settled = tostring(err) end) "#,