diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 6490296..09ad280 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -137,8 +137,8 @@ local probe = { -- table cardinality cannot tell "once per buffer" -- from "every tick for one buffer" fallback_installed = false, - fallback_watch = nil, -- fallback sid being polled for die-before-init - fallback_failed = false, + fallback_watches = {}, -- sid key -> sid, each polled die-before-init + fallback_done = {}, -- sid key -> initialized or terminally handled saw_initialized = false, } @@ -286,23 +286,36 @@ end -- 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. --- Only servers this module's config produced. `ensure_server` labels --- every auto-attached server `default-`, so that label is the --- derivation discriminator: a server the USER spawned from `init.lua` --- carries their own label, is not derived from `pmacs.lsp.config.lean4`, --- and must not be stopped because our config changed. Selecting on --- `language_id` alone swept those up too — a destructive side effect on --- state this module does not own. -local DERIVED_LABEL = "default-lean4" +-- Only servers the config-driven path itself produced. A server's label, +-- language, command, and root are all caller-supplied public values; none +-- is an ownership discriminator. `lsp.lua` records the successful spawn +-- in a private origin table, which is the fact this lifecycle may act on. +local function is_derived_server(sid) + local ok, owned = pcall(pmacs.lsp._is_default_server, sid, "lean4") + return ok and owned == true +end local function retire_derived_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.label == DERIVED_LABEL then ids[#ids + 1] = info.id end + if is_derived_server(info.id) then ids[#ids + 1] = info.id end end - for _, id in ipairs(ids) do retire_server(id) end + for _, id in ipairs(ids) do + -- These ids predate the fallback spawn. Mark them handled before + -- retirement so the discovery poll cannot mistake their terminal + -- state for a fallback that failed to initialize. + probe.fallback_done[tostring(id)] = true + retire_server(id) + end +end + +local function watch_fallback_server(sid) + if not sid or not is_derived_server(sid) then return end + local key = tostring(sid) + if probe.fallback_done[key] then return end + probe.fallback_watches[key] = sid end -- Rebuild the ACTIVE buffer's attachment if it is Lean and stale. @@ -358,33 +371,44 @@ local function repair_active_if_stale() end -- **A successful SPAWN is not a successful START.** The once-per- -- buffer bound stops `_attach_buffer` being called again, but it says - -- nothing about the server it produced: `ensure_server` never forwards - -- `cfg.restart`, so the fallback inherits `OnCrash`, and an executable - -- that dies before `initialize` is respawned by the manager forever - -- with no attempt ceiling — silently, because `latched` has already - -- disabled the primary's failure poll. Watch this one too, once. - if not probe.fallback_watch and not probe.fallback_failed then - probe.fallback_watch = fresh.server - end + -- nothing about the server it produced. Arm this id immediately; the + -- poll below also discovers servers created through lsp.lua's own + -- after-load and command paths. + watch_fallback_server(fresh.server) end --- The fallback's own die-before-initialize poll. One shot: on failure it --- retires the server (which is what actually ends the respawn loop) and --- reports, and never re-arms. -local function poll_fallback() - local sid = probe.fallback_watch - if not sid then return end - local kind = server_state_kind(sid) - if kind == "initialized" then - probe.fallback_watch = nil - return +-- Every fallback server gets its own die-before-initialize poll. A scalar +-- watch cannot cover Q#LN15's simultaneous per-root servers, and a server +-- may be created by lsp.lua's after-load or command path without passing +-- through `repair_active_if_stale`. Discovery from the private ownership +-- table closes both holes. +local function poll_fallbacks() + if not probe.fallback_installed then return end + local ok, rows = pcall(pmacs.lsp.list) + if not ok or not rows then return end + + local by_key = {} + for _, info in ipairs(rows) do + local key = tostring(info.id) + by_key[key] = info + if not probe.fallback_done[key] and is_derived_server(info.id) then + probe.fallback_watches[key] = info.id + end end - if kind == nil or kind == "crashed" or kind == "stopped" then - probe.fallback_watch = nil - probe.fallback_failed = true - if kind ~= nil then retire_server(sid) end - report("LSP: lean4 fallback " .. fallback_name() - .. " started but did not stay up") + + for key, sid in pairs(probe.fallback_watches) do + local info = by_key[key] + local kind = info and info.state and info.state.kind + if kind == "initialized" then + probe.fallback_watches[key] = nil + probe.fallback_done[key] = true + elseif info == nil or kind == "crashed" or kind == "stopped" then + probe.fallback_watches[key] = nil + probe.fallback_done[key] = true + if info ~= nil then retire_server(sid) end + report("LSP: lean4 fallback " .. fallback_name() + .. " started but did not stay up") + end end end @@ -394,10 +418,10 @@ local function fire_latch(sid, why) probe.watching = nil 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_derived_lean_servers() + -- No shared config changed, so only the server whose failure + -- triggered this verdict is invalid. Sweeping every root here stops + -- healthy instances of a root-sensitive command for no reason. + if sid and is_derived_server(sid) then retire_server(sid) end return end retire_derived_lean_servers() @@ -551,22 +575,66 @@ function M.wait_for_diagnostics(sid, uri, version, fn) return rid end +local function when_server_ready(sid, fn) + local function state_kind() + local ok, state = pcall(pmacs.lsp.status, sid) + if not ok or not state then return nil end + return state.kind + end + + local kind = state_kind() + if kind == "initialized" then + fn(nil) + return + end + if kind == nil or kind == "crashed" or kind == "stopped" then + fn("server did not initialize") + return + end + + -- A command may have just healed a dead attachment, in which case the + -- replacement is still starting. Requests are not queued before + -- initialize, so issue this one after the lifecycle reaches ready + -- rather than replacing the attachment and immediately failing on it. + pmacs.async(function() + for _ = 1, 300 do + pmacs.async.yield_to_next_tick() + kind = state_kind() + if kind == "initialized" then + fn(nil) + return + end + if kind == nil or kind == "crashed" or kind == "stopped" then + fn("server did not initialize") + return + end + end + fn("server initialization timed out") + end) +end + pmacs.command.define { name = "lean.wait-for-diagnostics", description = "Wait for the Lean server to finish elaborating this file", fn = function() - local rec = pmacs.lsp.active_attachment() + local rec = pmacs.lsp._attachment_for_command() if not rec or rec.language ~= "lean4" then pmacs.editor.set_status("lean: no Lean server for this buffer") return end pmacs.editor.set_status("lean: elaborating…") - M.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) - if err then - pmacs.editor.set_status("lean: " .. tostring(err)) - else - pmacs.editor.set_status("lean: elaboration complete") + when_server_ready(rec.server, function(init_err) + if init_err then + pmacs.editor.set_status("lean: " .. tostring(init_err)) + return end + M.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) + if err then + pmacs.editor.set_status("lean: " .. tostring(err)) + else + pmacs.editor.set_status("lean: elaboration complete") + end + end) end) end, } @@ -600,13 +668,17 @@ 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 - if not probe.started then - local path = pmacs.editor.file_path() - start_probe(path and M.root_for(path) or nil) - end - local rec = pmacs.lsp.active_attachment() if rec and rec.language == "lean4" then + -- A matching-root server supplied by the user may be adopted by + -- `ensure_server`. Its lifecycle is not evidence about the + -- config-driven command, and neither the version probe nor fallback + -- latch may mutate config because that foreign server changed state. + if not is_derived_server(rec.server) 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 -- **Arm ONCE, capturing buffer and server together.** Setting -- `buf_key` on every Lean load meant a second Lean buffer opened -- before the verdict silently became the rebuild target while the @@ -632,6 +704,10 @@ pmacs.hook.add("buffer.after-load", function() -- that produced no attachment is a failure. local cfg = pmacs.lsp.config.lean4 if not cfg or not cfg.command 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 -- No attachment for a Lean buffer with a configured command means -- `ensure_server` could not spawn at all — a synchronous ENOENT, @@ -662,7 +738,7 @@ pmacs.hook.add("process.after-tick", function() -- 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() - poll_fallback() + poll_fallbacks() end) -- Test seam: acceptance drives the latch deterministically rather than diff --git a/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua index 6081a3d..bf56a4c 100644 --- a/builtin/runtime/lsp.lua +++ b/builtin/runtime/lsp.lua @@ -607,6 +607,12 @@ local function project_root_for(language, path) return dir_of(path), "fallback" end +-- Servers created by the automatic config-driven path. This is the +-- ownership fact a caller-supplied `label` cannot provide: labels are +-- public, unreserved display strings, while entries here are written +-- only after this module itself successfully spawns a server. +local default_servers = {} + local function ensure_server(language, path) local cfg = pmacs.lsp.config[language] if not cfg or not cfg.command then return nil end @@ -660,7 +666,30 @@ local function ensure_server(language, path) cwd = root, root_uri = key_uri, }) - if ok then return sid end + if ok then + default_servers[tostring(sid)] = language + return sid + end + return nil +end + +-- Internal ownership seam for builtins whose lifecycle follows the +-- config-driven server set (currently Lean's one-shot fallback). A +-- user-managed server may deliberately use the same language id, label, +-- command, and root; none of those make it ours. +function pmacs.lsp._is_default_server(sid, language) + local owned_language = default_servers[tostring(sid)] + return owned_language ~= nil + and (language == nil or owned_language == language) +end + +local function server_state_kind(sid) + if not sid then return nil end + for _, info in ipairs(pmacs.lsp.list()) do + if tostring(info.id) == tostring(sid) then + return info.state and info.state.kind + end + end return nil end @@ -669,14 +698,8 @@ end -- forgotten, or was spawned against a now-replaced `pmacs.lsp.config` -- entry — get rebuilt on the next attach attempt. local function server_is_live(sid) - if not sid then return false end - for _, info in ipairs(pmacs.lsp.list()) do - if tostring(info.id) == tostring(sid) then - local kind = info.state and info.state.kind - return kind ~= "crashed" and kind ~= "stopped" - end - end - return false + local kind = server_state_kind(sid) + return kind ~= nil and kind ~= "crashed" and kind ~= "stopped" end local function server_is_initialized(sid) @@ -811,6 +834,15 @@ local function attach_buffer(buf) local existing = attachments[key] if existing and server_is_live(existing.server) then return existing end if existing then + local kind = server_state_kind(existing.server) + if kind == "crashed" or kind == "stopped" then + -- A terminal OnCrash client may still have `next_restart_at` + -- armed. Spawning beside it creates two same-root servers when + -- the old id restarts. `forget` is the terminal-state operation: + -- it removes the client and cancels that pending restart before + -- the replacement is created. + pcall(pmacs.lsp.forget, existing.server) + end attachments[key] = nil -- Unsent edits targeted the dead attachment; the did_open below -- carries the full current text, superseding them. @@ -896,6 +928,14 @@ local function attached_for_active() return attach_buffer(buf) end +-- Internal command-path resolver for builtin request producers outside +-- this module. Unlike `active_attachment` it may replace a dead record; +-- unlike `attachment_for_request` it is called only from an explicit +-- user command, where attach-on-use is the intended policy. +function pmacs.lsp._attachment_for_command() + return attached_for_active() +end + -- Pure, side-effect-free attachment lookup for the active buffer: -- returns the live record (with `.uri`) when a server is already -- attached, else nil. Unlike `attached_for_active`, it never *triggers* @@ -964,8 +1004,10 @@ function pmacs.lsp.attachment_for_request() -- perturb LSP state), so a dead record reads as "no attachment" -- rather than triggering a rebuild. if not server_is_live(rec.server) then - attachments[key] = nil - pending_did_change[key] = nil + -- Preserve the record. A crashed OnCrash server may restart under + -- the SAME id; clearing the map here would orphan that recovered + -- server, while this non-attaching lookup has no authority to + -- cancel the restart or create a replacement. return nil end flush_did_change(key) diff --git a/docs/active-work.md b/docs/active-work.md index 6b99985..b96cc42 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` (36 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (40 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 @@ -359,9 +359,29 @@ If it does not, stop and repair the remote/fetch configuration. assertion counted TABLE KEYS, which cannot distinguish "once per buffer" from "every tick for one buffer" — cardinality stays 1 either way. Now a numeric attempt counter; the bite shows **174 vs 1**. +- **Round-6 review: four P1s and one P2, suite 40/40.** (1) General + point-of-use healing treated a crashed OnCrash server as absent and + spawned beside it while its old id still had `next_restart_at` armed; + `attach_buffer` now forgets a terminal record before replacement. + `attachment_for_request` remains non-attaching and preserves the + record, so a same-id restart can recover instead of being orphaned. + (2) The fallback watch was scalar, while Q#LN15 permits simultaneous + per-root servers and lsp.lua can create them without passing through + Lean's repair function. Watches are now per-SID and discover every + config-driven Lean server from a private origin table. (3) The shipped + `lean.wait-for-diagnostics` command bypassed both safe resolvers and + still consumed a stopped record; it now uses a command-safe resolver, + waits asynchronously for a healed replacement to initialize, and the + test requires the real request to finish. (4) When no config swap + occurred, one failed root still swept a healthy root; that arm now + retires only the SID whose verdict fired. (5) `label` is public and + unreserved, therefore not ownership. lsp.lua records successful + config-driven spawns privately, and every Lean lifecycle decision keys + on that origin fact; the user-server pin deliberately collides on + `default-lean4`. - **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 + discriminates."** Green tests across six rounds repeatedly pinned only + a nearby helper or an absence, and only biting exposed it. **Carry this to `docs/agent-handoff.md` when the lane lands.** The concrete shapes, all from this branch: 1. R1 acceptance 36 asserted "every server is terminal" — pinning the @@ -389,6 +409,11 @@ If it does not, stop and repair the remote/fetch configuration. not the things attempted against (bite: 174 vs 1). 9. A NONEXISTENT executable only exercises synchronous ENOENT. To reach "spawned, then died", the fixture must actually spawn. + 10. Calling the two SAFE HELPERS directly does not pin a shipped + command that bypasses both. Drive the command registry entry and + require its terminal result — replacing a dead record with a + `starting` server is still not success if the request is issued + before initialize. 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 @@ -424,10 +449,10 @@ If it does not, stop and repair the remote/fetch configuration. works. Only a parseable version below 3.1.0 triggers it; the 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 36/36; lean4 stage 1 9/9; dispatch seams 15/15; + workspace Clippy clean; 1,829 default + 2,003 CRDT library tests; + lean4 server 40/40; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,225 across 94 suites, zero failures**; + serial workspace sweep 3,229 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 e28ac8f..86be1d5 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -1438,10 +1438,10 @@ fn r5_a_fallback_that_dies_after_spawning_is_bounded_and_reported() { #[test] fn r5_a_user_spawned_lean_server_is_not_retired_by_the_fallback() { - // `retire_*` selected on `language_id == "lean4"`, which also names - // servers the user spawned themselves from `init.lua`. Those are not - // derived from `pmacs.lsp.config.lean4` and stopping them is a - // destructive side effect on state this module does not own. + // Language id AND label are public caller-supplied values. Even a + // user server that deliberately collides with the automatic path's + // `default-lean4` display label is not derived from + // `pmacs.lsp.config.lean4` and must not be stopped. let fx = Fixture::new(); fx.toolchain("pkg", "v4.9.0\n"); let file = fx.write("pkg/A.lean", "def a := 1\n"); @@ -1453,7 +1453,7 @@ fn r5_a_user_spawned_lean_server_is_not_retired_by_the_fallback() { &format!( r#" _G.mine = pmacs.lsp.spawn({{ - label = "my-own-lean", + label = "default-lean4", language_id = "lean4", command = "{}", args = {{}}, @@ -1642,3 +1642,241 @@ fn r5_a_dead_attachment_is_never_handed_to_a_command() { {rebuilt:?}" ); } + +// --------------------------------------------------------------------------- +// Round-6 review. Each is a direct counterexample against 19f48d4. +// --------------------------------------------------------------------------- + +#[test] +fn r6_the_shipped_lean_command_rebuilds_a_dead_attachment() { + // The round-5 test called `attachment_for_request` and + // `_attach_buffer` directly, while the shipped Lean command read the + // raw `active_attachment` and still handed its request to a stopped + // server. Drive the production command this time. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let mut state = editor(&fx); + open(&state, &file); + settle(&mut state); + + exec( + &state, + r" + local rec = pmacs.lsp.active_attachment() + assert(rec) + pmacs.lsp.stop(rec.server) + ", + ); + tick_for(&mut state, 200); + + exec( + &state, + r#"pmacs.command.invoke("lean.wait-for-diagnostics")"#, + ); + let kind: 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" + "#, + ); + assert!( + kind != "stopped" && kind != "crashed" && kind != "gone" && kind != "none", + "the shipped command must resolve through the command-safe \ + attachment path; saw {kind:?}" + ); + tick_for(&mut state, 500); + let status = state.core.borrow().status.clone(); + assert_eq!( + status, "lean: elaboration complete", + "the rebuilt command path must deliver the request, not merely \ + replace the attachment" + ); +} + +#[test] +fn r6_every_spawned_fallback_server_is_bounded() { + // A scalar fallback watch covers only one Q#LN15 root. The second + // server can also be created directly by lsp.lua's after-load path, + // bypassing `repair_active_if_stale` entirely. + use std::os::unix::fs::PermissionsExt as _; + + let fx = Fixture::new(); + fx.toolchain("one", "v4.9.0\n"); + fx.toolchain("two", "v4.9.0\n"); + let first = fx.write("one/A.lean", "def a := 1\n"); + let second = fx.write("two/B.lean", "def b := 2\n"); + let absent_primary = fx.dir("bin/no-such-lake"); + let dying_fallback = fx.root.join("bin/dying-lean"); + std::fs::create_dir_all(dying_fallback.parent().unwrap()).unwrap(); + std::fs::write(&dying_fallback, "#!/bin/sh\nexit 4\n").unwrap(); + std::fs::set_permissions(&dying_fallback, std::fs::Permissions::from_mode(0o755)).unwrap(); + + 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(&dying_fallback) + ), + ); + + open(&state, &first); + open(&state, &second); + tick_for(&mut state, 1600); + + let worst_attempt: i64 = eval( + &state, + r" + local worst = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if s.language_id == 'lean4' and (s.attempt or 0) > worst then + worst = s.attempt + end + end + return worst + ", + ); + assert!( + worst_attempt <= 1, + "every fallback server must be bounded; an unwatched root \ + reached attempt {worst_attempt}" + ); +} + +#[test] +fn r6_point_of_use_healing_does_not_duplicate_a_restarting_server() { + // A crashed OnCrash server still has `next_restart_at` armed. + // Spawning a fresh id beside it produces two same-root servers when + // the old one restarts. Use Rust so this pins the general lsp.lua + // seam independently of Lean's fallback lifecycle. + let fx = Fixture::new(); + let file = fx.write("A.rs", "fn main() {}\n"); + let mut state = editor(&fx); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.rust = {{ + command = "{}", + args = {{}}, + env = {{ PMACS_FAKE_LSP_MODE = "crash" }}, + }} + "#, + fake_lsp_path() + ), + ); + open(&state, &file); + + let mut crashed = false; + for _ in 0..100 { + state.tick_processes(); + state.tick_lsp(); + crashed = eval( + &state, + r#" + for _, s in ipairs(pmacs.lsp.list()) do + if s.language_id == "rust" + and s.state and s.state.kind == "crashed" then + return true + end + end + return false + "#, + ); + if crashed { + break; + } + std::thread::sleep(Duration::from_millis(5)); + } + assert!(crashed, "precondition: the attached server crashed"); + + exec(&state, "pmacs.lsp.hover_at_cursor()"); + let rust_servers: i64 = eval( + &state, + r#" + local n = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if s.language_id == "rust" then n = n + 1 end + end + return n + "#, + ); + assert_eq!( + rust_servers, 1, + "healing must cancel the old id's armed restart before spawning \ + its replacement" + ); +} + +#[test] +fn r6_no_swap_retires_only_the_failed_root() { + // When config already equals the fallback, no shared config changed. + // One root's failure must not globally retire another root's healthy + // instance of the same cwd-sensitive command. + use std::os::unix::fs::PermissionsExt as _; + + let fx = Fixture::new(); + fx.toolchain("bad", "v4.9.0\n"); + fx.toolchain("good", "v4.9.0\n"); + let bad = fx.write("bad/A.lean", "def a := 1\n"); + let good = fx.write("good/B.lean", "def b := 2\n"); + let wrapper = fx.root.join("bin/root-sensitive-lean"); + std::fs::create_dir_all(wrapper.parent().unwrap()).unwrap(); + std::fs::write( + &wrapper, + format!( + "#!/bin/sh\ncase \"$PWD\" in */bad) exit 4;; esac\nexec \"{}\"\n", + fake_lsp_path() + ), + ) + .unwrap(); + std::fs::set_permissions(&wrapper, std::fs::Permissions::from_mode(0o755)).unwrap(); + + let mut state = editor(&fx); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.lean4.command = "{}" + pmacs.lsp.config.lean4.args = {{}} + pmacs.lean._fallback = {{ command = "{}", args = {{}} }} + "#, + lua_str(&wrapper), + lua_str(&wrapper) + ), + ); + open(&state, &bad); + open(&state, &good); + tick_for(&mut state, 700); + + let good_alive: bool = eval( + &state, + r#" + for _, s in ipairs(pmacs.lsp.list()) do + if s.cwd and s.cwd:match("/good$") then + local k = s.state and s.state.kind + return k ~= "stopped" and k ~= "crashed" + end + end + return false + "#, + ); + assert!( + good_alive, + "one root's failure must not stop another root when no config \ + swap occurred" + ); +}