fix(lsp): close round-six Lean fallback gaps
Make command-time attachment healing cancel an armed terminal restart before replacing the server, while keeping request-only lookup pure and restart-safe. Track config-driven server ownership privately, bound every fallback server per SID, scope no-swap retirement to the failed root, and route the shipped Lean diagnostics command through the safe resolver while waiting for initialization. Add direct acceptance counterexamples for all five review findings and record the sixth-round verification and vacuity lesson.
This commit is contained in:
parent
19f48d46c0
commit
786de69d38
|
|
@ -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-<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"
|
||||
-- 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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue