fix(lean): correct the server lifecycle; round 2 review
Three P1 lifecycle defects and two P2s. The focused suite was 20/20 with every one of them live, which is the part worth keeping. **1. The crashed primary respawned forever underneath the fallback.** Round 2 skipped the retire call for terminal servers to avoid corrupting them — but the crash had already armed `next_restart_at`, and `maybe_restart` fires on every elapsed backoff with no attempt ceiling. The broken command kept respawning under the live fallback. The right call depends on the state, and each is wrong for the other: `forget` REQUIRES a terminal state and removes the client outright, which also drops the restart timer; `stop` is for a live one and corrupts a terminal one (its not-initialized branch parks it in `ShuttingDown` forever). `retire_server` now dispatches on state. **2. Re-attachment targeted whatever buffer was active when the asynchronous verdict landed.** `_attach_buffer` is an active-buffer-only seam, and "some attachment now names a different server" is satisfied by an unrelated Rust buffer — clearing the retry and leaving the Lean buffer stale forever. The initiating buffer is now captured and the retry waits for it. **3. A failing fallback retried every tick forever, silently**, contradicting acceptance 27's promise that a second failure surfaces. "Waiting for the old server to go" and "attempting the replacement" are now separate: once the old one is terminal or gone, the replacement is attempted EXACTLY once, and a spawn failure is reported. **4. The Lake version parser was being applied to arbitrary wrappers.** `version_below_3_1` encodes lake's output contract; a working `my-lean-wrapper` reporting "wrapper 1.0" would have been replaced despite its server initializing fine. The version probe is now gated on the command's basename being `lake`. The FAILURE latch stays command-agnostic — that one keys on the server actually not starting, which is true of any command. **5. An unconfigured Lean server was reported as a failure** and latched, poisoning the session so a later configuration could never take effect. Absent config or command now means disabled; only a configured command that produced no attachment is a failure. **6. The ledger recorded pre-fix counts** after the fixes were pushed. Now 25/25 and 3,214. That is the #161 fmt-blocker error in a slower form: verification must describe the pushed tree. Sign-offs requested in review: `M.fallback` is now `M._fallback`, an underscored test seam, and its idempotence check compares args as well as command — the same command with different arguments is not "already applied". Dropping the `command ~= "lake"` guard stands for the failure latch only. Five regression tests added, and **three of them were too weak on first write; only bite-testing found it**: * asserting "no live non-fallback server" misses a respawn loop, because a respawning server sits in `crashed` most of the time — `attempt` is the observable that counts respawns; * returning to a buffer with `find_or_open` re-fires `buffer.after-load`, which repairs the attachment regardless of the code under test — `switch_buffer` is the honest return; * a MISSING command fails synchronously inside `after-load` where the rebuild happens inline, so the async race cannot occur — only the probe path exercises it. Each of the five now fails against the exact round-2 mutation it targets.
This commit is contained in:
parent
cdaea66203
commit
3377db070a
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue