diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index dd98892..5f74792 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -125,7 +125,8 @@ local probe = { started = false, -- the `lake --version` probe has been spawned latched = false, -- the fallback has fired (or been ruled out) proc = nil, -- process id of the running probe - buf = "", -- accumulated probe stdout + out = "", -- accumulated probe stdout + buf_key = nil, -- tostring() of the buffer that started this watching = nil, -- sid we are waiting to see fail before initialize saw_initialized = false, } @@ -142,9 +143,9 @@ 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) +-- State kind for the server whose `tostring(id)` is `skey`, or nil if +-- the manager has forgotten it (which is itself a terminal answer). +local function server_state_kind_for_key(skey) local ok, rows = pcall(pmacs.lsp.list) if not ok or not rows then return nil end for _, info in ipairs(rows) do @@ -155,6 +156,10 @@ local function server_state_kind(sid) return nil end +local function server_state_kind(sid) + return server_state_kind_for_key(tostring(sid)) +end + local function version_below_3_1(text) local major, minor = text:match("(%d+)%.(%d+)") if not major then return false end @@ -163,11 +168,25 @@ 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" } } +-- What the latch falls back TO. +-- +-- **Underscored: a test seam, not supported user configuration.** It is +-- a table only 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. Presenting it as public config would owe framing, +-- documentation, validation and mutation semantics that nothing here +-- provides; users configure Lean through `pmacs.lsp.config.lean4`. +M._fallback = { command = "lean", args = { "--server" } } + +local function same_args(a, b) + a, b = a or {}, b or {} + if #a ~= #b then return false end + for i = 1, #a do + if a[i] ~= b[i] then return false end + end + return true +end -- Swap `command`/`args` ONLY. A wholesale table replacement would -- silently discard a user's `env` / `settings` / `init_options` / `root` @@ -181,81 +200,111 @@ M.fallback = { command = "lean", args = { "--server" } } local function swap_to_fallback() local cfg = pmacs.lsp.config.lean4 if not cfg then return false end - if cfg.command == M.fallback.command then return false end - cfg.command = M.fallback.command - cfg.args = M.fallback.args + -- Idempotence compares command AND args: the same command with + -- different arguments is not "already applied", and treating it as + -- such would silently skip a swap that still needed to happen. + if cfg.command == M._fallback.command + and same_args(cfg.args, M._fallback.args) then + return false + end + cfg.command = M._fallback.command + cfg.args = M._fallback.args return true end --- Fire the fallback: stop the failing server FIRST, then swap, then let --- the next attach spawn afresh. --- --- Stopping first is load-bearing, not defensive. The spec default is --- `LspRestartPolicy::OnCrash`, the termination handler never consults --- the exit code, and `maybe_restart` has no attempt ceiling — so a --- broken `lake` respawns forever on a backoff, underneath the latch, --- 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. +-- 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:** +-- +-- * TERMINAL (`crashed` / `stopped`) -> `forget`. It requires a +-- terminal state and removes the client outright, which also drops +-- the `next_restart_at` the crash scheduled. `stop` here would take +-- its not-initialized branch and set `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 it sits in `ShuttingDown` forever: +-- `server_is_live` reads that as LIVE so `attach_buffer` never +-- rebuilds, and `forget` then refuses it for not being terminal. +-- * NON-TERMINAL -> `stop`. `forget` rejects it, and `stop` disables +-- restart and drives the polite shutdown. +-- +-- Round 1 skipped the call entirely for terminal servers. That avoided +-- the corruption but left `next_restart_at` armed, so the crashed +-- primary respawned 500ms later and kept respawning underneath the +-- live fallback — invisible to a test that stopped ticking first. +local function retire_server(sid) + local kind = server_state_kind(sid) + if kind == nil then return end + if kind == "crashed" or kind == "stopped" then + pcall(pmacs.lsp.forget, sid) + else + pcall(pmacs.lsp.stop, sid) + end +end + local function fire_latch(sid, why) if probe.latched then return end probe.latched = true 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 sid then retire_server(sid) 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. + .. 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. -- - -- **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. + -- 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 once the active Lean buffer is attached to a server that --- is not the one the latch stopped. +-- 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 - 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 + -- (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 end @@ -265,7 +314,7 @@ local function drain_probe() if not ok or not evs then return end for _, ev in ipairs(evs) do if ev.kind == "stdout" or ev.kind == "stderr" then - probe.buf = probe.buf .. tostring(ev.bytes) + probe.out = probe.out .. tostring(ev.bytes) elseif ev.kind == "exited" or ev.kind == "signaled" or ev.kind == "crashed" then local proc = probe.proc @@ -279,7 +328,7 @@ local function drain_probe() -- question failure detection would otherwise answer slowly: an -- old-but-working lake that starts a useless server. if ev.kind == "exited" and ev.code == 0 - and version_below_3_1(probe.buf) then + and version_below_3_1(probe.out) then fire_latch(probe.watching, "lake is older than 3.1.0") end end @@ -296,10 +345,20 @@ local function start_probe(root) probe.started = true local cfg = pmacs.lsp.config.lean4 if not cfg or not cfg.command then return end + -- **Only probe something actually named `lake`.** `version_below_3_1` + -- parses the first `x.y` it finds anywhere in the output, which is a + -- rule about LAKE's output contract and nothing else. Run against a + -- user's wrapper it is a category error: a working `my-lean-wrapper` + -- reporting "wrapper 1.0" would be replaced despite its server having + -- initialized fine. The FAILURE latch stays command-agnostic — that + -- one keys on the server actually not starting, which is true of any + -- command — but the version rule only applies where its contract + -- holds. + local base = cfg.command:match("([^/]+)$") or cfg.command + if base ~= "lake" 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). + -- "lake": a user pointing `command` at an absolute path to lake should + -- have THAT probed, not whatever `lake` resolves to on PATH. local spec = { -- COHERENCE §9: `ProcessSpec.label` is the only identity a process -- carries, and it is what `pmacs.process.list` renders. A user @@ -429,6 +488,11 @@ pmacs.hook.add("buffer.after-load", function() local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf) if not ok_lang or lang ~= "lean4" then return end + -- The buffer that started this, remembered for the asynchronous + -- rebuild: `_attach_buffer` acts on whatever is active when the + -- verdict lands, which may be a different buffer entirely. + probe.buf_key = tostring(buf) + if not probe.started then local path = pmacs.editor.file_path() start_probe(path and M.root_for(path) or nil) @@ -444,14 +508,21 @@ pmacs.hook.add("buffer.after-load", function() 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. + -- **Unconfigured is DISABLED, not failed.** A user who sets + -- `pmacs.lsp.config.lean4 = nil`, or clears its `command`, has turned + -- the Lean server off; reporting that "nil could not be started" is a + -- false alarm, and latching would poison the session so a later + -- configuration could never take effect. Only a CONFIGURED command + -- that produced no attachment is a failure. + local cfg = pmacs.lsp.config.lean4 + if not cfg or not cfg.command then return end + + -- No attachment for a Lean buffer with a configured command 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") + fire_latch(nil, "`" .. tostring(cfg.command) .. "` could not be started") end end) @@ -467,6 +538,7 @@ end) -- 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 1a1e7ae..4a650da 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` (20 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (25 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 @@ -308,10 +308,14 @@ 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 17/17; lean4 stage 1 9/9; dispatch seams 15/15; + lean4 server 25/25; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,206 across 94 suites, zero failures**; - `git diff --check` clean. + workspace sweep 3,214 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 + describes the pushed tree; recording it late is the #161 fmt-blocker + error in a slower form.) ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index fac090b..ec62980 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1553,10 +1553,14 @@ What remains deferred: 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. + Stage 3b's latch, which works around it by dispatching on state: + `forget` for a terminal server (it requires terminal state, and + removing the client also drops the `next_restart_at` the crash armed), + `stop` for a live one. Merely *skipping* the call is not enough — that + leaves the restart timer running and the broken command respawns + underneath the fallback. 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 diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index 6fe5ed4..cba8792 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -390,7 +390,7 @@ fn with_fallback(state: &EditorState, lake_cmd: &Path) { r#" pmacs.lsp.config.lean4.command = "{}" pmacs.lsp.config.lean4.args = {{ "serve" }} - pmacs.lean.fallback = {{ command = "{}", args = {{}} }} + pmacs.lean._fallback = {{ command = "{}", args = {{}} }} "#, lua_str(lake_cmd), fake_lsp_path() @@ -824,3 +824,248 @@ fn lean_root_is_canonical_so_a_symlinked_open_reuses_one_server() { both spellings produce the same affinity key" ); } + +// --------------------------------------------------------------------------- +// Round-2 review findings. Each of these fails against the code as it +// stood at cdaea66, where the focused suite was already 20/20 — the +// lifecycle defects were invisible to it. +// --------------------------------------------------------------------------- + +/// Tick for at least `ms`, so a 500ms restart backoff actually elapses. +/// The round-2 defect was invisible precisely because the suite stopped +/// ticking as soon as the fallback initialized, ~300ms in. +fn tick_for(state: &mut EditorState, ms: u64) { + let deadline = std::time::Instant::now() + Duration::from_millis(ms); + while std::time::Instant::now() < deadline { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + } +} + +#[test] +fn r2_crashed_primary_does_not_respawn_underneath_the_fallback() { + // The crash schedules `next_restart_at`; `maybe_restart` fires after + // the 500ms backoff with no attempt ceiling. Skipping the retire + // call (round 2) left that armed, so the broken command kept + // respawning under the live fallback — forever, unobserved. + 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\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); + // Well past one backoff. + tick_for(&mut state, 1400); + + // **`attempt`, not liveness.** A respawning server spends most of + // its life in `crashed` waiting out the backoff, so "no live + // non-fallback server" is satisfied while it loops forever — that + // weaker assertion passed against the round-2 code and caught + // nothing. `attempt` increments on every spawn, so it counts the + // respawns directly. A retired server is absent from the list + // entirely (`forget` removes the client); one left with + // `next_restart_at` armed climbs past 1. + let worst_attempt: i64 = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + local live = rec and tostring(rec.server) or "" + local worst = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) ~= live then + local a = s.attempt or 0 + if a > worst then worst = a end + end + end + return worst + "#, + ); + assert_eq!( + worst_attempt, 0, + "the retired primary is gone from the manager, not respawning after the backoff (attempt > 0 means it is still there; > 1 means it respawned)" + ); + assert_eq!( + attached_state(&state), + "initialized", + "and the buffer is on the live fallback" + ); +} + +#[test] +fn r2_reattach_targets_the_originating_buffer_not_whatever_is_active() { + // `_attach_buffer` is an active-buffer-only seam and the latch's + // verdict arrives asynchronously. Round 2 accepted "some attachment + // now names a different server", which an unrelated Rust buffer + // satisfies — clearing the retry and stranding the Lean buffer. + // + // **Driven through the PROBE**, not through a missing executable: a + // missing command fails synchronously inside `buffer.after-load`, + // where the Lean buffer is still active and the rebuild happens + // inline, so the race cannot occur and the test proves nothing. The + // probe's verdict lands on a later tick, which is the whole point. + // The stub's `serve` sleeps, so only the probe can trigger anything. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + fx.write("pkg/Cargo.toml", "[package]\nname = \"p\"\n"); + let lean_file = fx.write("pkg/A.lean", "def a := 1\n"); + let rust_file = fx.write("pkg/src/main.rs", "fn main() {}\n"); + let old_lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + + let mut state = editor(&fx); + with_fallback(&state, &old_lake); + // A working Rust server, so switching away lands on a real + // attachment with a different server id — the decoy. + exec( + &state, + &format!( + "pmacs.lsp.config.rust = {{ command = \"{}\" }}", + fake_lsp_path() + ), + ); + + open(&state, &lean_file); + exec(&state, "_G.lean_buf = pmacs.window.buffer()"); + // Switch away before the probe's verdict can land. + open(&state, &rust_file); + tick_for(&mut state, 500); + + // Come back with a buffer SWITCH, not `find_or_open`. Re-opening + // fires `buffer.after-load`, which re-runs lsp.lua's own attach and + // would repair the record no matter what the latch did. + exec(&state, "pmacs.window.switch_buffer(_G.lean_buf)"); + tick_for(&mut state, 400); + + let lang: String = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + return rec and tostring(rec.language) or "none" + "#, + ); + assert_eq!(lang, "lean4", "we are back on the Lean buffer"); + + // The observable that discriminates: WHICH command the Lean buffer's + // server is running. A retry cleared by the decoy leaves it on the + // original `lake` stub. + let cmd: 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.command) + end + end + return "gone" + "#, + ); + assert_eq!( + cmd, + fake_lsp_path(), + "the ORIGINATING Lean buffer ends up on the fallback — a decoy \ + Rust attachment must not satisfy the retry" + ); +} + +#[test] +fn r2_a_failing_fallback_is_reported_once_and_does_not_retry_forever() { + // Acceptance 27 promises a second failure surfaces rather than + // loops. Round 2 retried `_attach_buffer` every tick with nothing + // reported. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let absent_primary = fx.dir("bin/no-such-lake"); + let absent_fallback = fx.dir("bin/no-such-lean"); + + let mut state = editor(&fx); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.lean4.command = "{}" + pmacs.lsp.config.lean4.args = {{ "serve" }} + pmacs.lean._fallback = {{ command = "{}", args = {{}} }} + "#, + lua_str(&absent_primary), + lua_str(&absent_fallback) + ), + ); + + open(&state, &file); + tick_for(&mut state, 300); + + let status = state.core.borrow().status.clone(); + assert!( + status.contains("did not start either"), + "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"); +} + +#[test] +fn r2_a_working_wrapper_is_not_version_probed_as_lake() { + // `version_below_3_1` encodes LAKE's output contract. Applying it to + // an arbitrary wrapper is a category error: a working wrapper + // reporting its own "wrapper 1.0" would be replaced despite its + // server initializing fine. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + // Named something other than `lake`, reporting a sub-3.1 version, + // but which serves fine. + let wrapper = fx.lake_stub("bin/my-lean-wrapper", "wrapper 1.0"); + let mut state = editor(&fx); + with_fallback(&state, &wrapper); + + open(&state, &file); + tick_for(&mut state, 400); + + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!( + cmd, + wrapper.display().to_string(), + "a wrapper's own version string is not Lake's; the version probe \ + must not run against it" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!(!latched, "and the latch stayed disarmed"); +} + +#[test] +fn r2_an_unconfigured_lean_server_is_disabled_not_failed() { + // Setting `pmacs.lsp.config.lean4 = nil` means "off". Reporting that + // `nil` could not start is a false alarm, and latching poisons the + // session so a later configuration can never take effect. + let fx = Fixture::new(); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let mut state = editor(&fx); + exec(&state, "pmacs.lsp.config.lean4 = nil"); + exec(&state, "pmacs.editor.set_status(\"\")"); + + open(&state, &file); + settle(&mut state); + + assert_eq!( + state.core.borrow().status.clone(), + "", + "an unconfigured Lean server reports nothing — it is disabled" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!( + !latched, + "and the session is not poisoned: a later config must still work" + ); +}