fix(lsp,lean): bound the fallback's own failure; heal at point of use
Round 5 review: one P1, a frontend scope hole, and three P2s. **1. A fallback that SPAWNS and then dies retried forever.** The once-per-buffer guard bounds calls to `_attach_buffer`, not the server those calls produce. `ensure_server` still never forwards `cfg.restart`, so the fallback inherits `OnCrash`; an executable that exits before `initialize` is respawned by the manager with no attempt ceiling — silently, because `latched` has already disabled the primary's failure poll. The fallback now gets its own one-shot die-before-initialize watch, which retires it (ending the respawn loop) and reports. The prior failing-fallback test used a NONEXISTENT executable, so it only ever exercised synchronous ENOENT. To reach "spawned, then died" the fixture has to actually spawn. **2. Simultaneous frontends.** Both repair triggers read the ambient `pmacs.window.buffer()`, and the daemon restores `active_frontend` to the last-dispatched frontend before `tick_processes` — so a Lean buffer active in ANOTHER frontend receives no `buffer.after-switch` here and stays stale after its server is globally retired. Fixed at the seam that is frontend-agnostic: **make consumption safe.** `attached_for_active` now rebuilds rather than returning a record whose server is dead, and `attachment_for_request` reports none (it must not perturb LSP state, so it cannot rebuild). Whichever frontend runs a command is the active one while it runs, so healing at the point of use reaches every buffer no eager sweep can. This also closes the half where a dead attachment was handed to a command and the request vanished. **3. The retirement sweep stopped user-managed servers.** Selecting on `language_id == "lean4"` also names servers the user spawned from `init.lua`, which are not derived from `pmacs.lsp.config.lean4`. It now keys on the `default-lean4` label `ensure_server` stamps — the derivation discriminator. **4. Repair ran even when no swap occurred.** `swap_to_fallback()` returning false left `latched` true, so the next tick retried the UNCHANGED configuration and reported it as a fallback failure. Split into `probe.fallback_installed`: repair exists to apply a swap, so no swap means nothing to apply. **5. The once-per-buffer assertion counted table keys**, which cannot distinguish "once per buffer" from "every tick for one buffer" — cardinality stays 1 either way. Replaced with a numeric attempt counter; the bite reports 174 attempts against the expected 1. Five bites, each against 7c37bdc: no fallback watch -> attempt reaches 4; retire by language_id -> the user's server is stopped; gate repair on `latched` -> a repair is attempted with no swap; drop the once-per-buffer guard -> 174 vs 1; hand back a dead attachment -> a command receives a `stopped` server. Two more vacuity shapes recorded in the ledger (8 and 9): counting distinct keys cannot bound repeated work, and a nonexistent executable cannot reach any post-spawn failure.
This commit is contained in:
parent
7c37bdc514
commit
19f48d46c0
|
|
@ -133,6 +133,12 @@ local probe = {
|
|||
-- version verdict still has to retire it
|
||||
armed = false, -- the target buffer + primary have been captured
|
||||
repaired = {}, -- buffer key -> repair attempted (at most once)
|
||||
repair_attempts = 0, -- COUNT of attach attempts, not distinct buffers:
|
||||
-- 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,
|
||||
saw_initialized = false,
|
||||
}
|
||||
|
||||
|
|
@ -280,12 +286,21 @@ 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.
|
||||
local function retire_all_lean_servers()
|
||||
-- Only servers this module's config produced. `ensure_server` labels
|
||||
-- every auto-attached server `default-<language>`, 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"
|
||||
|
||||
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.language_id == "lean4" then ids[#ids + 1] = info.id end
|
||||
if info.label == DERIVED_LABEL then ids[#ids + 1] = info.id end
|
||||
end
|
||||
for _, id in ipairs(ids) do retire_server(id) end
|
||||
end
|
||||
|
|
@ -308,7 +323,14 @@ end
|
|||
-- 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
|
||||
-- **`fallback_installed`, not `latched`.** When the swap does not
|
||||
-- happen — the config already names the fallback, or it vanished
|
||||
-- before an asynchronous verdict landed — `fire_latch` returns early
|
||||
-- but `latched` stays true. Gating repair on `latched` then retried
|
||||
-- the UNCHANGED configuration and reported the result as a fallback
|
||||
-- failure, which is both a second pointless spawn and a misleading
|
||||
-- message. Repair exists to apply a swap; no swap, nothing to apply.
|
||||
if not probe.fallback_installed then return end
|
||||
local buf = pmacs.window.buffer()
|
||||
if not buf then return end
|
||||
local key = tostring(buf)
|
||||
|
|
@ -327,10 +349,42 @@ local function repair_active_if_stale()
|
|||
if not stale then return end
|
||||
|
||||
probe.repaired[key] = true
|
||||
probe.repair_attempts = probe.repair_attempts + 1
|
||||
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")
|
||||
return
|
||||
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
|
||||
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
|
||||
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")
|
||||
end
|
||||
end
|
||||
|
||||
|
|
@ -343,10 +397,11 @@ local function fire_latch(sid, 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()
|
||||
retire_derived_lean_servers()
|
||||
return
|
||||
end
|
||||
retire_all_lean_servers()
|
||||
retire_derived_lean_servers()
|
||||
probe.fallback_installed = true
|
||||
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`).
|
||||
|
|
@ -607,6 +662,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()
|
||||
end)
|
||||
|
||||
-- Test seam: acceptance drives the latch deterministically rather than
|
||||
|
|
|
|||
|
|
@ -871,6 +871,21 @@ local function attached_for_active()
|
|||
if not buf then return nil end
|
||||
local key = tostring(buf)
|
||||
local rec = attachments[key]
|
||||
-- A record whose server is dead is worse than no record: every
|
||||
-- command below issues requests against it and gets silence. Rebuild
|
||||
-- instead, which is what `attach_buffer` does for a stale attachment
|
||||
-- anyway — this just stops the dead record short-circuiting that.
|
||||
--
|
||||
-- Load-bearing for anything that retires a server out from under open
|
||||
-- buffers (Arc 8 Stage 3b's fallback latch retires every Lean server
|
||||
-- at once). Buffers in OTHER frontends get no `buffer.after-switch`
|
||||
-- in this one, so an eager repair sweep keyed on the ambient active
|
||||
-- buffer cannot reach them; healing at the point of USE is
|
||||
-- frontend-agnostic, because whichever frontend runs the command is
|
||||
-- the active one while it runs.
|
||||
if rec and not server_is_live(rec.server) then
|
||||
rec = nil
|
||||
end
|
||||
if rec then
|
||||
-- Every interactive command resolves its attachment here before
|
||||
-- issuing requests; flushing now means the server answers those
|
||||
|
|
@ -942,6 +957,17 @@ function pmacs.lsp.attachment_for_request()
|
|||
local key = tostring(buf)
|
||||
local rec = attachments[key]
|
||||
if not rec then return nil end
|
||||
-- Same liveness rule as `attached_for_active`: a record naming a dead
|
||||
-- server is worse than none, because the caller issues a request
|
||||
-- against it and waits for a reply that cannot come. Unlike that
|
||||
-- function this one is deliberately non-attaching (it must not
|
||||
-- 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
|
||||
return nil
|
||||
end
|
||||
flush_did_change(key)
|
||||
return rec
|
||||
end
|
||||
|
|
|
|||
|
|
@ -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` (31 tests).
|
||||
`pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (36 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
|
||||
|
|
@ -334,6 +334,31 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
argument-inclusive attribution was implemented but pinned only by
|
||||
"contains the command name", so a mutation dropping every argument
|
||||
still passed.
|
||||
- **Round-5 review: one P1 plus a frontend scope hole, and four more.**
|
||||
(1) A fallback that SPAWNS and then dies retried forever: the
|
||||
once-per-buffer guard bounds `_attach_buffer`, not the server it
|
||||
produced, and `ensure_server` never forwards `cfg.restart` so the
|
||||
fallback inherits `OnCrash` — respawned by the manager with no
|
||||
ceiling, silently, because `latched` had disabled the primary's poll.
|
||||
The fallback now gets its own one-shot die-before-initialize watch.
|
||||
(2) **Simultaneous frontends**: both repair triggers read the ambient
|
||||
`pmacs.window.buffer()`, and the daemon restores `active_frontend` to
|
||||
the last-dispatched one before `tick_processes`, so a Lean buffer
|
||||
active in ANOTHER frontend gets no `after-switch` and stays stale.
|
||||
Fixed at the right seam — **make CONSUMPTION safe**: both
|
||||
`attached_for_active` and `attachment_for_request` now refuse a record
|
||||
whose server is dead (the former rebuilds, the latter reports none,
|
||||
since it must not perturb LSP state). Healing at the point of use is
|
||||
frontend-agnostic, because whichever frontend runs a command is active
|
||||
while it runs. (3) The retirement sweep selected on `language_id`, so
|
||||
it stopped USER-spawned Lean servers too; it now keys on the
|
||||
`default-lean4` label `ensure_server` stamps, which is the derivation
|
||||
discriminator. (4) `probe.latched` gated repair even when NO swap
|
||||
occurred, so an already-fallback config was retried and misreported.
|
||||
Split out `probe.fallback_installed`. (5) The once-per-buffer
|
||||
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**.
|
||||
- **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
|
||||
|
|
@ -359,6 +384,11 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
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.
|
||||
8. Counting DISTINCT KEYS cannot bound REPEATED WORK: a per-tick retry
|
||||
on one buffer keeps `#repaired == 1` forever. Count the attempts,
|
||||
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.
|
||||
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
|
||||
|
|
@ -395,9 +425,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 31/31; lean4 stage 1 9/9; dispatch seams 15/15;
|
||||
lean4 server 36/36; lean4 stage 1 9/9; dispatch seams 15/15;
|
||||
multi-root 13/13; M4 121; required GPU 155; **isolated-config
|
||||
workspace sweep 3,220 across 94 suites, zero failures**;
|
||||
workspace sweep 3,225 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
|
||||
|
|
|
|||
|
|
@ -1371,3 +1371,274 @@ fn r4_attribution_names_the_exact_command_and_its_arguments() {
|
|||
want substring: {expected}\n saw: {status:?}"
|
||||
);
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Round-5 review. All fail against 7c37bdc.
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
#[test]
|
||||
fn r5_a_fallback_that_dies_after_spawning_is_bounded_and_reported() {
|
||||
// The once-per-buffer guard bounds calls to `_attach_buffer`, not
|
||||
// the server it produced. `ensure_server` never forwards
|
||||
// `cfg.restart`, so the fallback inherits `OnCrash` and a binary
|
||||
// that exits before `initialize` is respawned forever — silently,
|
||||
// because `latched` has already disabled the primary's poll. The
|
||||
// prior failing-fallback test used a NONEXISTENT executable, which
|
||||
// only exercises synchronous ENOENT.
|
||||
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 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, &file);
|
||||
tick_for(&mut state, 1600);
|
||||
|
||||
// Nothing may be respawning: `attempt` counts spawns per server.
|
||||
let worst_attempt: i64 = eval(
|
||||
&state,
|
||||
r"
|
||||
local worst = 0
|
||||
for _, s in ipairs(pmacs.lsp.list()) do
|
||||
local a = s.attempt or 0
|
||||
if a > worst then worst = a end
|
||||
end
|
||||
return worst
|
||||
",
|
||||
);
|
||||
assert!(
|
||||
worst_attempt <= 1,
|
||||
"a dying fallback must not be respawned indefinitely; saw \
|
||||
attempt {worst_attempt}"
|
||||
);
|
||||
let status = state.core.borrow().status.clone();
|
||||
assert!(
|
||||
status.contains("did not stay up") || status.contains("did not start"),
|
||||
"and the second failure is reported; saw {status:?}"
|
||||
);
|
||||
}
|
||||
|
||||
#[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.
|
||||
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);
|
||||
exec(
|
||||
&state,
|
||||
&format!(
|
||||
r#"
|
||||
_G.mine = pmacs.lsp.spawn({{
|
||||
label = "my-own-lean",
|
||||
language_id = "lean4",
|
||||
command = "{}",
|
||||
args = {{}},
|
||||
}})
|
||||
"#,
|
||||
fake_lsp_path()
|
||||
),
|
||||
);
|
||||
settle(&mut state);
|
||||
|
||||
open(&state, &file);
|
||||
tick_for(&mut state, 600);
|
||||
|
||||
let mine_alive: bool = eval(
|
||||
&state,
|
||||
r#"
|
||||
for _, s in ipairs(pmacs.lsp.list()) do
|
||||
if tostring(s.id) == tostring(_G.mine) then
|
||||
local k = s.state and s.state.kind
|
||||
return k ~= "stopped" and k ~= "crashed"
|
||||
end
|
||||
end
|
||||
return false
|
||||
"#,
|
||||
);
|
||||
assert!(
|
||||
mine_alive,
|
||||
"a user-spawned Lean server survives a config-driven fallback — \
|
||||
it was never derived from that config"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn r5_no_swap_means_no_repair_attempts() {
|
||||
// When the config already names the fallback, `swap_to_fallback`
|
||||
// returns false and `fire_latch` returns early — but `latched` is
|
||||
// true, so a repair gated on `latched` retried the UNCHANGED
|
||||
// configuration and reported it as a fallback failure.
|
||||
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-lean");
|
||||
let mut state = editor(&fx);
|
||||
// Config and fallback are the SAME missing command, so no swap is
|
||||
// possible.
|
||||
exec(
|
||||
&state,
|
||||
&format!(
|
||||
r#"
|
||||
pmacs.lsp.config.lean4.command = "{}"
|
||||
pmacs.lsp.config.lean4.args = {{}}
|
||||
pmacs.lean._fallback = {{ command = "{}", args = {{}} }}
|
||||
"#,
|
||||
lua_str(&absent),
|
||||
lua_str(&absent)
|
||||
),
|
||||
);
|
||||
|
||||
open(&state, &file);
|
||||
tick_for(&mut state, 400);
|
||||
|
||||
let attempts: i64 = eval(&state, "return pmacs.lean._probe.repair_attempts");
|
||||
assert_eq!(
|
||||
attempts, 0,
|
||||
"no swap happened, so there is nothing to apply and no repair \
|
||||
should be attempted"
|
||||
);
|
||||
let status = state.core.borrow().status.clone();
|
||||
assert!(
|
||||
!status.contains("falling back"),
|
||||
"and nothing claims a fallback occurred; saw {status:?}"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn r5_repair_is_attempted_at_most_once_per_buffer_by_count() {
|
||||
// Counting keys in the `repaired` table cannot distinguish
|
||||
// "once per buffer" from "every tick for one buffer" — the
|
||||
// cardinality stays 1 either way. Count the ATTEMPTS.
|
||||
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);
|
||||
// Many ticks; a per-tick retry would climb without bound.
|
||||
tick_for(&mut state, 900);
|
||||
|
||||
let attempts: i64 = eval(&state, "return pmacs.lean._probe.repair_attempts");
|
||||
assert_eq!(
|
||||
attempts, 1,
|
||||
"exactly one repair attempt across many ticks for one buffer"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn r5_a_dead_attachment_is_never_handed_to_a_command() {
|
||||
// Buffers live in other frontends get no `buffer.after-switch` here,
|
||||
// so an eager sweep keyed on the ambient active buffer cannot reach
|
||||
// them. Healing at the point of USE is frontend-agnostic:
|
||||
// `attached_for_active` must not return a record whose server is
|
||||
// gone.
|
||||
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);
|
||||
// A working primary, so we get a live attachment first.
|
||||
exec(
|
||||
&state,
|
||||
&format!("pmacs.lsp.config.lean4.command = \"{}\"", fake_lsp_path()),
|
||||
);
|
||||
open(&state, &file);
|
||||
settle(&mut state);
|
||||
let first: String = attached_sid(&state);
|
||||
assert_ne!(first, "none", "precondition: attached");
|
||||
|
||||
// Retire it out from under the buffer, as the latch does globally,
|
||||
// WITHOUT any switch or repair tick.
|
||||
exec(
|
||||
&state,
|
||||
r"
|
||||
local rec = pmacs.lsp.active_attachment()
|
||||
pcall(pmacs.lsp.stop, rec.server)
|
||||
",
|
||||
);
|
||||
for _ in 0..40 {
|
||||
state.tick_processes();
|
||||
state.tick_lsp();
|
||||
std::thread::sleep(Duration::from_millis(5));
|
||||
}
|
||||
|
||||
// Now a command resolves its attachment. It must not get the dead
|
||||
// one; it must rebuild.
|
||||
// `attachment_for_request` is deliberately non-attaching, so a dead
|
||||
// record must read as "no attachment" rather than being handed over.
|
||||
let for_request: String = eval(
|
||||
&state,
|
||||
r#"
|
||||
local rec = pmacs.lsp.attachment_for_request()
|
||||
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_eq!(
|
||||
for_request, "none",
|
||||
"a non-attaching resolve must not hand back a dead server"
|
||||
);
|
||||
|
||||
// And the attaching path rebuilds rather than returning the corpse.
|
||||
let rebuilt: String = eval(
|
||||
&state,
|
||||
r#"
|
||||
pmacs.lsp._attach_buffer()
|
||||
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!(
|
||||
rebuilt != "stopped" && rebuilt != "crashed" && rebuilt != "gone" && rebuilt != "none",
|
||||
"the attaching path rebuilds against a live server; saw \
|
||||
{rebuilt:?}"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue