From 1e1be67b49dc1b90783ed3b2fd8df3c776cac8ef Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 17:40:02 -0400 Subject: [PATCH 1/9] feat(lean): the Lean 4 language server (Arc 8 Stage 3b) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Framing Q#LN7, Q#LN8, Q#LN16; acceptance 22–28, 24a/24b, 35, 36, 36a, 37. Stacked on Stage 3a (#167), whose notification/response seams and `pmacs.fs.canonicalize` this consumes. No protocol change; the only Rust outside the test helper is one `include_str!` line. **The Lake-aware root (Q#LN8).** `pmacs.project.detect` cannot express this rule — it is innermost-wins by construction, and a Lake package's `lean-toolchain` sits at the outermost level, so a file under `/.lake/packages/dep/` belongs to ``'s server rather than `dep`'s. The resolver walks up collecting markers and returns the outermost, stopping at `pmacs.project.search_boundary()` so a stray marker above a fixture cannot leak in. Two things about the marker test are easy to get wrong in opposite directions, and both are pinned. `io.open` **succeeds on a directory**, so a truthiness check accepts a `lean-toolchain` directory; but requiring a non-nil read rejects an **empty** `lean-toolchain`, which is a legitimate marker — `locate-dominating-file` semantics are existence, not content. The discriminator is `read`'s second return: decline only on a non-nil error. Acceptance 24a and 24b each fail against the implementation that satisfies only the other; both bites are recorded. The root is canonicalized once up front, because a configured root reaches `file_uri_for` verbatim and that URI is the affinity key (#161). Canonicalizing the starting directory suffices — every ancestor of a canonical path is canonical, since the walk only strips components. **`lake serve` with a lazy probe and a one-shot latch (Q#LN7).** Nothing runs at init: `pmacs.lsp.config` is declarative, and spawning a process at startup for every user, Lean-using or not, is the cost rev 1 refused. Both the probe and the server spawn are gated on a real Lean attachment. The probe cannot gate the first attach — there is no blocking process run, so its verdict arrives after `ensure_server` has already decided. Hence the optimistic spawn, with the probe and latch correcting it. A non-zero probe exit is deliberately NOT a trigger: §2.9's elan-shim case makes `lake --version` fail on machines where `lake serve` still works, and the server-failure latch covers that better. The probe answers only the question failure detection would answer slowly — an old-but-working lake that starts a useless server. The latch stops the failing server **before** spawning the fallback, and that ordering is load-bearing rather than defensive: the spec default is `OnCrash`, the termination handler never consults the exit code, and `maybe_restart` has no attempt ceiling, so a broken `lake` respawns forever underneath the latch. `pmacs.lsp.stop` sets `restart = Never`, which is what disarms it. Bitten: removing the stop fails acceptance 36. The swap rewrites `command` and `args` only, so a user's `env`, `settings`, `init_options` and `root` survive — a wholesale table replacement would discard their `init.lua` at the moment they are least likely to notice. **`waitForDiagnostics` (Q#LN16)** resolves through Stage 3a's response seam, with `M-x lean.wait-for-diagnostics` on top. `$/lean/fileProgress` subscribes on the notification seam and is pinned end-to-end through a new `leanprogress` mode on the fake server rather than by calling the handler directly — the wiring is the only part that can break. **Attribution (COHERENCE §9/§1.2).** The probe spawns as `lean:lake-version-probe`, so a user wondering why their editor touched `lake` finds an owner in `pmacs.process.list`. The latch reports through `pmacs.editor.set_status` — the channel that exists — and acceptance 36a observes that channel, so a report made only through the undefined `pmacs.error` would fail it. **Stage 1's acceptance 12 is updated, half superseded.** It asserted `pmacs.lsp.config.lean4 == nil` to guard against a Stage-3 front-run; Stage 3b is that stage, so keeping it would pin the opposite of the intended behavior. The half that survives is the one about restraint, and it matters more now: constructing an editor spawns nothing even though the config exists and names `lake`, and opening a Lean buffer with no server configured spawns nothing either. That is what holds Q#LN7's "not at init" promise. Bites recorded, all against the committed tree: bare `io.open` -> 24a fails, 24b passes; require-non-nil-read -> 24b fails, 24a passes; no canonicalization -> the symlink case spawns two servers; no stop before fallback -> acceptance 36 fails. --- builtin/runtime/lean.lua | 359 +++++++++++++++++ src/bin/pmacs_fake_lsp.rs | 21 + src/editor.rs | 11 + tests/lean4_server_acceptance.rs | 640 +++++++++++++++++++++++++++++++ tests/lean4_stage1_acceptance.rs | 62 +-- 5 files changed, 1069 insertions(+), 24 deletions(-) create mode 100644 builtin/runtime/lean.lua create mode 100644 tests/lean4_server_acceptance.rs diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua new file mode 100644 index 0000000..3fe73da --- /dev/null +++ b/builtin/runtime/lean.lua @@ -0,0 +1,359 @@ +-- builtin/runtime/lean.lua --- Arc 8 Stage 3b: the Lean 4 language server. +-- +-- Framing: `docs/lean4-mode-framing.md` Q#LN7 (lake serve + probe + +-- fallback latch), Q#LN8 (Lake-aware outermost root), Q#LN16 +-- (waitForDiagnostics). Stage 1 shipped the grammar, mode, comment +-- strings and pair set; Stage 3a shipped the notification/response +-- seams and `pmacs.fs.canonicalize` this file consumes. +-- +-- Loaded after `lsp.lua`, which owns `pmacs.lsp.config` and the drain. + +local M = {} + +-- Q#LN8 — the Lake-aware root ----------------------------------------- +-- +-- `pmacs.project.detect` cannot express this rule. It is innermost-wins +-- by construction, and a Lake package's `lean-toolchain` sits at the +-- OUTERMOST level: a file under `/.lake/packages/dep/Foo.lean` +-- belongs to ``'s server, not to `dep`'s, because `lake serve` is +-- bound to one package and analyzes its dependencies from inside it. +-- Inverting `detect` globally would change Rust/Go/Node roots for every +-- user, so the rule lives here as a function-valued `config.root` — +-- the generalization Stage 2 (#161) added for exactly this. + +-- The marker test, and the two ways to get it wrong. +-- +-- `pmacs.fs.stat` is UNUSABLE here: it returns an awaitable handle +-- (`fs.lua`), and this runs synchronously inside `ensure_server` <- +-- `attach_buffer` <- the `buffer.after-load` hook, where there is no +-- coroutine to await on. The Lua stdlib's `io.open` is the only +-- synchronous existence check available. +-- +-- But `io.open` alone is wrong in BOTH directions: +-- * it SUCCEEDS on a directory (probed), so a truthiness test would +-- accept a `lean-toolchain` directory as a marker; and +-- * requiring a non-nil read rejects an EMPTY `lean-toolchain`, which +-- is a legitimate marker — `locate-dominating-file` semantics are +-- existence, not content. +-- The discriminator is `read`'s SECOND return (probed on LuaJIT 2.1): +-- file with content -> "l", no error -> marker +-- empty file -> nil, NO error -> marker +-- directory -> nil, "Is a directory" -> decline +-- missing -> io.open returns nil -> decline +-- so: decline only on a non-nil `err`. This needs no per-platform +-- re-probe, because both directory behaviors are declines — a platform +-- whose `fopen` refuses directories fails at `io.open` instead. There +-- is no platform where a directory both opens and yields a byte. +local function has_toolchain(dir) + local f = io.open(dir .. "/lean-toolchain", "r") + if not f then return false end + local _, err = f:read(1) + f:close() + return err == nil +end + +local function parent_of(dir) + local up = dir:match("^(.*)/[^/]+$") + if up == nil or up == dir or up == "" then return nil end + return up +end + +-- The walk stops at `pmacs.project.search_boundary()`. Not politeness: +-- `detect_project_within` (`src/project.rs`) exists precisely so a +-- stray marker above a temp fixture cannot leak into detection, and a +-- Lua walk that ignored the boundary would break that contract — and +-- make acceptance 23's outermost assertion non-hermetic against any +-- `lean-toolchain` sitting above the test's tempdir. +local function within_boundary(dir, boundary) + if not boundary then return true end + return dir == boundary or dir:sub(1, #boundary + 1) == boundary .. "/" +end + +-- Returns the OUTERMOST ancestor holding a `lean-toolchain`, or nil to +-- decline (which falls through to `pmacs.project.detect`, then the +-- file's own directory). +-- +-- **The result is canonical, and must be.** A configured root — which +-- this is — reaches `file_uri_for` verbatim and that URI is the +-- server-affinity key (#161). `pmacs.editor.file_path()` collapses `.` +-- and `..` lexically but leaves symlinks intact, so one package opened +-- through a symlink and through its real path would otherwise spawn two +-- `lake serve` processes. Canonicalizing ONCE up front is enough: +-- every ancestor of a canonical path is itself canonical, since the +-- walk only strips trailing components. +-- +-- If canonicalization fails (deleted file, broken symlink) the resolver +-- declines rather than returning a path it cannot vouch for. +function M.root_for(path) + if type(path) ~= "string" then return nil end + local dir = path:match("^(.*)/[^/]*$") + if not dir then return nil end + dir = pmacs.fs.canonicalize(dir) + if not dir then return nil end + local boundary + local ok, b = pcall(pmacs.project.search_boundary) + if ok then boundary = b end + -- The boundary is canonicalized at set time (`set_search_boundary`), + -- so comparing it against a canonical `dir` is apples to apples. + local outermost = nil + local cur = dir + while cur and within_boundary(cur, boundary) do + if has_toolchain(cur) then outermost = cur end + cur = parent_of(cur) + end + return outermost +end + +-- Q#LN7 — `lake serve`, with a lazy probe and a one-shot latch -------- +-- +-- `pmacs.lsp.config.lean4` is declarative and must stay cheap: spawning +-- a process at startup for every user, Lean-using or not, is the cost +-- rev 1 refused. So no probe runs here — it runs on the first `.lean` +-- attach, below. +pmacs.lsp.config.lean4 = pmacs.lsp.config.lean4 or { + command = "lake", + args = { "serve" }, + root = M.root_for, + -- No `init_options`: `hasWidgets?` defaults to false, which is the + -- correct posture for a client reading plain goals out of standard + -- messages rather than driving the `$/lean/rpc/*` widget stack. +} + +-- Session state. The latch is one-shot and never re-arms: a user whose +-- toolchain is broken sees one fallback attempt, not a loop. +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 + watching = nil, -- sid we are waiting to see fail before initialize + saw_initialized = false, +} + +local function report(msg) + -- COHERENCE §1.2: background work must leave an attributed trace. + -- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error` + -- is referenced by fifteen call sites and defined nowhere in + -- production, so it rides along rather than standing alone. + pcall(pmacs.editor.set_status, msg) + if pmacs.error then pcall(pmacs.error, msg) end +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. +local function version_below_3_1(text) + local major, minor = text:match("(%d+)%.(%d+)") + if not major then return false end + major, minor = tonumber(major), tonumber(minor) + if major < 3 then return true end + return major == 3 and minor < 1 +end + +-- Swap `command`/`args` ONLY. A wholesale table replacement would +-- silently discard a user's `env` / `settings` / `init_options` / `root` +-- from `init.lua` at exactly the moment they are least likely to notice. +local function swap_to_lean_server() + local cfg = pmacs.lsp.config.lean4 + if not cfg then return false end + if cfg.command ~= "lake" then return false end + cfg.command = "lean" + cfg.args = { "--server" } + 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. +local function fire_latch(sid, why) + if probe.latched then return end + probe.latched = true + if sid then pcall(pmacs.lsp.stop, sid) end + if swap_to_lean_server() then + report("LSP: lean4 " .. why .. "; falling back to `lean --server`") + else + report("LSP: lean4 " .. why) + end + probe.watching = nil +end + +local function drain_probe() + if not probe.proc then return end + local ok, evs = pcall(pmacs.process.events_take, probe.proc) + 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) + elseif ev.kind == "exited" or ev.kind == "signaled" + or ev.kind == "crashed" then + local proc = probe.proc + probe.proc = nil + pcall(pmacs.process.forget, proc) + -- A non-zero exit is NOT a fallback trigger on its own. §2.9: elan + -- shims make `lake --version` exit non-zero with "no default + -- toolchain configured" on a machine where `lake serve` may still + -- be the right command — the server-failure latch covers that + -- case, and covers it better. The probe answers only the ONE + -- 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 + fire_latch(probe.watching, "lake is older than 3.1.0") + end + end + end +end + +-- The probe cannot gate the first attach. There is no blocking process +-- run (§2.9): `spawn` + `events_take` off a tick is the only shape +-- available, so the verdict arrives AFTER `ensure_server` has already +-- had to decide. Hence the optimistic `lake serve` spawn, with the +-- probe and the latch correcting it. +local function start_probe(root) + if probe.started then return end + probe.started = true + local cfg = pmacs.lsp.config.lean4 + if not cfg or cfg.command ~= "lake" then return end + local spec = { + -- COHERENCE §9: `ProcessSpec.label` is the only identity a process + -- carries, and it is what `pmacs.process.list` renders. A user + -- wondering why their editor touched `lake` finds an owner here. + label = "lean:lake-version-probe", + command = "lake", + args = { "--version" }, + stdin = "null", + } + if root then spec.cwd = root end + local ok, proc = pcall(pmacs.process.spawn, spec) + if ok then probe.proc = proc end + -- A probe that cannot even spawn says nothing the latch will not say + -- more reliably a moment later, so it is not reported here. +end + +-- How the latch observes server failure. +-- +-- There is no event for "died before initialize" — the drain ignores +-- state events. So this polls `pmacs.lsp.list()` on the +-- `process.after-tick` cadence and treats a terminal state reached +-- WITHOUT an intervening `initialized` as the trigger. Watching stops +-- as soon as the server initializes, so an ordinary later crash (a real +-- server dying on a real error) does not silently rewrite the command. +local function poll_latch() + local sid = probe.watching + if not sid or probe.latched then return end + local skey = tostring(sid) + local ok, rows = pcall(pmacs.lsp.list) + if not ok or not rows then return end + for _, info in ipairs(rows) do + if tostring(info.id) == skey then + local kind = info.state and info.state.kind + if kind == "initialized" then + probe.saw_initialized = true + probe.watching = nil + return + end + if kind == "crashed" or kind == "stopped" then + fire_latch(sid, "`lake serve` failed to start") + end + return + end + end + -- Gone from the manager entirely without ever initializing. + fire_latch(nil, "`lake serve` failed to start") +end + +-- Q#LN16 — `textDocument/waitForDiagnostics` -------------------------- +-- +-- A plain request: no position, so Q#LN12's `outbound_position` concern +-- does not apply. Resolves when the server has finished elaborating. +-- Awaited through Stage 3a's response seam. +-- +-- `fn(err)` is called with nil on success. Registering the one-shot +-- requires the server to have an attached buffer — see the note on +-- `pmacs.lsp.on_response`; every caller here comes from an attachment. +function M.wait_for_diagnostics(sid, uri, fn) + local ok, rid = pcall(pmacs.lsp.send_request, sid, + "textDocument/waitForDiagnostics", { uri = uri }) + if not ok then + if fn then pcall(fn, tostring(rid)) end + return nil + end + if fn then + pmacs.lsp.on_response(sid, rid, function(_, err) + fn(err and err.message or nil) + end) + end + return rid +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() + 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, function(err) + if err then + pmacs.editor.set_status("lean: " .. tostring(err)) + else + pmacs.editor.set_status("lean: elaboration complete") + end + end) + end, +} + +-- `$/lean/fileProgress` — the elaboration-in-flight signal. Stage 5's +-- goal view reads it to distinguish "no goals" from "not done yet"; +-- here it is recorded so that consumer has something to read and so the +-- notification seam has its first production subscriber. +M.file_progress = {} + +pmacs.lsp.on_notification("$/lean/fileProgress", function(_, params) + local uri = params and params.textDocument and params.textDocument.uri + if type(uri) ~= "string" then return end + M.file_progress[uri] = params.processing or {} +end) + +-- Wiring -------------------------------------------------------------- + +-- Runs after `lsp.lua`'s own `buffer.after-load` subscription, so the +-- attachment already exists. The attachment's `language` IS the Lean +-- test — no separate major-mode lookup, which would be a second source +-- of truth for the same question. +pmacs.hook.add("buffer.after-load", function() + local rec = pmacs.lsp.active_attachment() + if not rec or rec.language ~= "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 + -- Watch only the FIRST Lean server: the latch is per session. + if not probe.latched and not probe.saw_initialized + and probe.watching == nil then + probe.watching = rec.server + end +end) + +pmacs.hook.add("process.after-tick", function() + drain_probe() + poll_latch() +end) + +-- Test seam: acceptance drives the latch deterministically rather than +-- waiting on real process timing. Not part of the public surface. +M._probe = probe +M._fire_latch = fire_latch +M._version_below_3_1 = version_below_3_1 + +pmacs.lean = M diff --git a/src/bin/pmacs_fake_lsp.rs b/src/bin/pmacs_fake_lsp.rs index 5d50b19..5f4fab5 100644 --- a/src/bin/pmacs_fake_lsp.rs +++ b/src/bin/pmacs_fake_lsp.rs @@ -483,6 +483,27 @@ fn main() { } }); write_frame(&mut stdout, &echo); + // Arc 8 Stage 3b: `leanprogress` mode emits one + // `$/lean/fileProgress` covering line 0, so the Lean + // subscriber can be pinned end-to-end through the real + // drain rather than by calling its handler directly. + if mode == "leanprogress" && uri.is_string() { + let progress = serde_json::json!({ + "jsonrpc": "2.0", + "method": "$/lean/fileProgress", + "params": { + "textDocument": { "uri": uri, "version": 1 }, + "processing": [{ + "range": { + "start": { "line": 0, "character": 0 }, + "end": { "line": 1, "character": 0 } + }, + "kind": 1 + }] + } + }); + write_frame(&mut stdout, &progress); + } // Also push a synthetic `publishDiagnostics` // notification with two entries (one Error, one // Warning) so M4.6 tests can exercise the store. diff --git a/src/editor.rs b/src/editor.rs index 79f1225..5f0f134 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -436,6 +436,17 @@ impl EditorState { include_str!("../builtin/runtime/lsp.lua"), ) .expect("load lsp builtin chunk"); + // Arc 8 Stage 3b: the Lean 4 language server. Loaded after + // lsp.lua because it registers `pmacs.lsp.config.lean4`, + // subscribes on the Stage 3a notification seam, and adds a + // `buffer.after-load` hook that must run AFTER lsp.lua's own + // (it reads the attachment lsp.lua creates). + lua_host + .eval( + Some("@pmacs/builtin/runtime/lean.lua"), + include_str!("../builtin/runtime/lean.lua"), + ) + .expect("load lean builtin chunk"); // Arc 1a: the in-buffer completion popup driver. Loaded after // lsp.lua because it drives `pmacs.lsp.request_completion` / // `pmacs.lsp.attachment_for_request` and after the framework diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs new file mode 100644 index 0000000..13cfcd0 --- /dev/null +++ b/tests/lean4_server_acceptance.rs @@ -0,0 +1,640 @@ +//! Arc 8 Stage 3b acceptance — the Lean 4 language server. +//! +//! `docs/lean4-mode-framing.md` Q#LN7, Q#LN8, Q#LN16; acceptance 22–28, +//! 24a/24b, 35, 36, 36a, 37. +//! +//! No live toolchain required. The server side is `pmacs_fake_lsp` +//! configured under the `lean4` language id; the probe and latch are +//! driven through shell stubs the fixture writes, so nothing here needs +//! `lake`, `lean`, or an elan toolchain on PATH (§2.9). +//! +//! Every fixture sets `pmacs.project.set_search_boundary` at its own +//! tempdir root. Without it the `lean-toolchain` walk climbs to the +//! filesystem root and acceptance 23's outermost assertion stops being +//! hermetic. + +#![cfg(unix)] + +use std::path::{Path, PathBuf}; +use std::time::Duration; + +use pmacs::editor::EditorState; + +fn exec(state: &EditorState, source: &str) { + state.lua_host.lua().load(source.to_owned()).exec().unwrap(); +} + +fn eval(state: &EditorState, source: &str) -> T { + state.lua_host.lua().load(source.to_owned()).eval().unwrap() +} + +fn fake_lsp_path() -> String { + env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned() +} + +fn lua_str(path: &Path) -> String { + path.display() + .to_string() + .replace('\\', "\\\\") + .replace('"', "\\\"") +} + +struct Fixture { + _dir: tempfile::TempDir, + root: PathBuf, +} + +impl Fixture { + fn new() -> Self { + let dir = tempfile::tempdir().unwrap(); + let root = std::fs::canonicalize(dir.path()).unwrap(); + Self { _dir: dir, root } + } + + fn write(&self, rel: &str, contents: &str) -> PathBuf { + let path = self.root.join(rel); + std::fs::create_dir_all(path.parent().unwrap()).unwrap(); + std::fs::write(&path, contents).unwrap(); + path + } + + fn mkdir(&self, rel: &str) -> PathBuf { + let path = self.root.join(rel); + std::fs::create_dir_all(&path).unwrap(); + path + } + + fn dir(&self, rel: &str) -> PathBuf { + self.root.join(rel) + } + + /// A `lean-toolchain` marker file. Content is irrelevant to the + /// resolver by design (existence semantics), which 24b pins. + fn toolchain(&self, rel_dir: &str, body: &str) { + self.write(&format!("{rel_dir}/lean-toolchain"), body); + } + + fn bind(&self, state: &EditorState) { + exec( + state, + &format!( + "pmacs.project.set_search_boundary(\"{}\")", + lua_str(&self.root) + ), + ); + } +} + +/// A fresh editor with every shipped language config cleared, then the +/// `lean4` entry rebuilt against the fake server while KEEPING the real +/// resolver. That combination is the point: the root rule under test is +/// production code, only the command is a stand-in. +fn editor(fx: &Fixture) -> EditorState { + let state = EditorState::new(); + exec(&state, "pmacs.lsp.config = {}"); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.lean4 = {{ + command = "{}", + args = {{}}, + root = pmacs.lean.root_for, + }} + "#, + fake_lsp_path() + ), + ); + fx.bind(&state); + state +} + +fn settle(state: &mut EditorState) { + for _ in 0..10 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(2)); + } +} + +fn open(state: &EditorState, path: &Path) { + exec( + state, + &format!("pmacs.buffer.find_or_open(\"{}\")", lua_str(path)), + ); +} + +/// `language_id|root_uri|cwd` for every live server, sorted. +fn rows(state: &EditorState) -> Vec { + let joined: String = eval( + state, + r#" + local out = {} + for _, s in ipairs(pmacs.lsp.list()) do + out[#out + 1] = table.concat({ + s.language_id or "", s.root_uri or "", s.cwd or "", + }, "|") + end + table.sort(out) + return table.concat(out, "\n") + "#, + ); + if joined.is_empty() { + Vec::new() + } else { + joined.lines().map(str::to_owned).collect() + } +} + +fn resolved_root(state: &EditorState, file: &Path) -> String { + eval( + state, + &format!( + "return tostring(pmacs.lean.root_for(\"{}\"))", + lua_str(file) + ), + ) +} + +// --------------------------------------------------------------------------- +// Acceptance 22 — a Lean file in a Lake package spawns one server rooted +// at the package. +// --------------------------------------------------------------------------- + +#[test] +fn acc22_lean_file_in_a_lake_package_spawns_one_server_at_the_package_root() { + let fx = Fixture::new(); + fx.toolchain("pkg", "leanprover/lean4:v4.9.0\n"); + let file = fx.write("pkg/Pkg/Basic.lean", "def x : Nat := 1\n"); + let mut state = editor(&fx); + open(&state, &file); + settle(&mut state); + + let pkg = fx.dir("pkg").display().to_string(); + assert_eq!( + rows(&state), + vec![format!("lean4|file://{pkg}|{pkg}")], + "one server, rooted and cwd'd at the Lake package" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 23 — outermost wins. +// +// The case `pmacs.project.detect` cannot express: it is innermost-wins by +// construction, so a dependency vendored under `.lake/packages` would get +// its own server and its own (wrong) view of the world. +// --------------------------------------------------------------------------- + +#[test] +fn acc23_nested_toolchains_resolve_to_the_outermost_package() { + let fx = Fixture::new(); + fx.toolchain("pkg", "leanprover/lean4:v4.9.0\n"); + fx.toolchain("pkg/.lake/packages/dep", "leanprover/lean4:v4.8.0\n"); + let inner = fx.write( + "pkg/.lake/packages/dep/Dep/Core.lean", + "def dep : Nat := 2\n", + ); + let state = editor(&fx); + + assert_eq!( + resolved_root(&state, &inner), + fx.dir("pkg").display().to_string(), + "a file under .lake/packages/dep belongs to the outer package" + ); + // Non-vacuity: the inner marker really exists, so "outermost" is a + // choice between two candidates rather than the only one found. + assert!(fx.dir("pkg/.lake/packages/dep/lean-toolchain").exists()); +} + +// --------------------------------------------------------------------------- +// Acceptance 24 — the walk stops at the search boundary. +// --------------------------------------------------------------------------- + +#[test] +fn acc24_walk_stops_at_the_search_boundary() { + let fx = Fixture::new(); + // Boundary is the fixture root; this marker sits INSIDE it. + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + // And this one sits AT the fixture root, i.e. above `pkg` but still + // within the boundary — it must win, being outermost. + fx.toolchain(".", "v4.7.0\n"); + let state = editor(&fx); + assert_eq!( + resolved_root(&state, &file), + fx.root.display().to_string(), + "within the boundary, the outermost marker wins" + ); + + // Now move the boundary IN to `pkg`. The root-level marker is above + // it and must not be reached. + exec( + &state, + &format!( + "pmacs.project.set_search_boundary(\"{}\")", + lua_str(&fx.dir("pkg")) + ), + ); + assert_eq!( + resolved_root(&state, &file), + fx.dir("pkg").display().to_string(), + "a marker above the boundary is not consulted" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 24a / 24b — the marker test, both directions. +// +// These two must each fail against the implementation that satisfies only +// the other. 24a bites the bare `io.open` truth test (which succeeds on a +// directory); 24b bites the read-a-byte-and-require-non-nil rule (which +// rejects an empty file at EOF). +// --------------------------------------------------------------------------- + +#[test] +fn acc24a_a_lean_toolchain_directory_is_not_a_marker() { + let fx = Fixture::new(); + fx.mkdir("pkg/lean-toolchain"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let state = editor(&fx); + assert_eq!( + resolved_root(&state, &file), + "nil", + "a `lean-toolchain` DIRECTORY must not mark a root" + ); +} + +#[test] +fn acc24b_an_empty_lean_toolchain_file_is_a_marker() { + let fx = Fixture::new(); + fx.toolchain("pkg", ""); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let state = editor(&fx); + assert_eq!( + resolved_root(&state, &file), + fx.dir("pkg").display().to_string(), + "marker semantics are existence, not content — an empty \ + `lean-toolchain` still marks the package" + ); + // Non-vacuity: the file really is empty. + assert_eq!( + std::fs::read(fx.dir("pkg/lean-toolchain")).unwrap().len(), + 0 + ); +} + +#[test] +fn acc24_resolver_declines_when_no_marker_exists() { + let fx = Fixture::new(); + let file = fx.write("loose/A.lean", "def a := 1\n"); + let state = editor(&fx); + assert_eq!( + resolved_root(&state, &file), + "nil", + "no marker anywhere is a decline, which falls through to \ + `pmacs.project.detect`" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 25 — a string-valued root still works. +// --------------------------------------------------------------------------- + +#[test] +fn acc25_string_valued_root_still_works() { + let fx = Fixture::new(); + let pkg = fx.mkdir("elsewhere"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let mut state = editor(&fx); + exec( + &state, + &format!("pmacs.lsp.config.lean4.root = \"{}\"", lua_str(&pkg)), + ); + open(&state, &file); + settle(&mut state); + + let want = pkg.display().to_string(); + assert_eq!( + rows(&state), + vec![format!("lean4|file://{want}|{want}")], + "the Q#LN8 generalization is additive; a plain string still wins" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 26 — didOpen carries languageId = "lean4". +// --------------------------------------------------------------------------- + +#[test] +fn acc26_did_open_carries_the_lean4_language_id() { + 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); + + let lang: String = eval( + &state, + "return tostring(pmacs.lsp.list()[1] and pmacs.lsp.list()[1].language_id)", + ); + assert_eq!( + lang, "lean4", + "the grammar entry name is the didOpen language id (Q#LN2)" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 28 (probe) — the version predicate. +// +// The parse is unit-tested directly because the spawn path is timing- +// bound; the latch's *effect* is pinned separately below. +// --------------------------------------------------------------------------- + +#[test] +fn acc28_version_predicate_triggers_only_below_3_1() { + let fx = Fixture::new(); + let state = editor(&fx); + let check = |v: &str| -> bool { + eval( + &state, + &format!("return pmacs.lean._version_below_3_1(\"{v}\")"), + ) + }; + assert!(check("Lake version 3.0.0"), "3.0.0 is below 3.1"); + assert!(!check("Lake version 3.1.0"), "3.1.0 is not below 3.1"); + assert!(!check("Lake version 5.0.0-abc"), "5.0.0 is not below 3.1"); + assert!(check("Lake version 2.9.9"), "2.9.9 is below 3.1"); + assert!( + !check("no default toolchain configured"), + "an unparseable line must NOT trigger the fallback — that is the \ + elan-shim case, which the failure latch handles better" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 27 / 35 / 36 — the fallback latch. +// --------------------------------------------------------------------------- + +#[test] +fn acc35_latch_preserves_user_config_and_swaps_only_command_and_args() { + let fx = Fixture::new(); + let state = editor(&fx); + // A user's init.lua settings, on the shipped shape. + exec( + &state, + r#" + pmacs.lsp.config.lean4.command = "lake" + pmacs.lsp.config.lean4.args = { "serve" } + pmacs.lsp.config.lean4.env = { MYVAR = "1" } + pmacs.lsp.config.lean4.settings = { lean = { verbose = true } } + pmacs.lsp.config.lean4.init_options = { hasWidgets = false } + _G.root_before = pmacs.lsp.config.lean4.root + pmacs.lean._fire_latch(nil, "test") + "#, + ); + + let after: String = eval( + &state, + r#" + local c = pmacs.lsp.config.lean4 + return table.concat({ + tostring(c.command), + tostring(c.args and c.args[1]), + tostring(c.env and c.env.MYVAR), + tostring(c.settings and c.settings.lean and c.settings.lean.verbose), + tostring(c.init_options and c.init_options.hasWidgets), + tostring(c.root == _G.root_before), + }, "|") + "#, + ); + assert_eq!( + after, "lean|--server|1|true|false|true", + "only command/args change; env, settings, init_options and root \ + survive the swap" + ); +} + +#[test] +fn acc27_the_latch_is_one_shot_and_does_not_re_arm() { + let fx = Fixture::new(); + let state = editor(&fx); + exec( + &state, + r#" + pmacs.lsp.config.lean4.command = "lake" + pmacs.lsp.config.lean4.args = { "serve" } + pmacs.lean._fire_latch(nil, "first failure") + _G.after_first = pmacs.lsp.config.lean4.command + -- A second failure must not rewrite the command again; if it did, + -- a user who deliberately set something else after the fallback + -- would have it silently replaced. + pmacs.lsp.config.lean4.command = "user-choice" + pmacs.lean._fire_latch(nil, "second failure") + _G.after_second = pmacs.lsp.config.lean4.command + "#, + ); + assert_eq!(eval::(&state, "return _G.after_first"), "lean"); + assert_eq!( + eval::(&state, "return _G.after_second"), + "user-choice", + "the latch never re-arms within a session" + ); +} + +#[test] +fn acc36_latch_stops_the_failing_server_before_spawning_the_fallback() { + 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); + assert_eq!(rows(&state).len(), 1, "precondition: one server is up"); + + // Fire the latch against the live server, exactly as `poll_latch` + // would. `pmacs.lsp.stop` sets `restart = Never` on the way out — + // which is what prevents `RestartPolicy::OnCrash` from respawning the + // broken command underneath the latch, forever, with no attempt cap. + exec( + &state, + r#" + pmacs.lsp.config.lean4.command = "lake" + pmacs.lsp.config.lean4.args = { "serve" } + pmacs.lean._fire_latch(pmacs.lsp.list()[1].id, "failed to start") + "#, + ); + settle(&mut state); + + let terminal: bool = eval( + &state, + r#" + for _, s in ipairs(pmacs.lsp.list()) do + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then return false end + end + return true + "#, + ); + assert!( + terminal, + "the failing server is stopped, not left to be respawned under \ + the latch" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 36a — attribution (COHERENCE §9 / §1.2). +// --------------------------------------------------------------------------- + +#[test] +fn acc36a_latch_leaves_a_status_line_trace() { + let fx = Fixture::new(); + let state = editor(&fx); + exec( + &state, + r#" + pmacs.lsp.config.lean4.command = "lake" + pmacs.lsp.config.lean4.args = { "serve" } + pmacs.lean._fire_latch(nil, "`lake serve` failed to start") + "#, + ); + let status = state.core.borrow().status.clone(); + assert!( + status.contains("lean4") && status.contains("lean --server"), + "the fallback names itself and what it fell back to; saw {status:?}" + ); + // The channel assertion is the point (COHERENCE §1.2): a report made + // only through `pmacs.error` — undefined in production — would leave + // this empty while every other assertion here still passed. + assert!(!status.is_empty()); +} + +#[test] +fn acc36a_probe_carries_a_lean_owned_process_label() { + // `ProcessSpec.label` is the only identity a process has, and it is + // what `pmacs.process.list` renders. Asserted on the spec the module + // builds rather than on a live `lake`, which CI does not have. + let fx = Fixture::new(); + let state = editor(&fx); + let src = std::fs::read_to_string( + Path::new(env!("CARGO_MANIFEST_DIR")).join("builtin/runtime/lean.lua"), + ) + .unwrap(); + assert!( + src.contains("label = \"lean:lake-version-probe\""), + "the probe process is attributed to Lean by label" + ); + // And it is genuinely lazy: no probe without an attachment. + let procs: i64 = eval(&state, "return #pmacs.process.list()"); + assert_eq!(procs, 0, "configuring Lean does not start the probe"); +} + +// --------------------------------------------------------------------------- +// Acceptance 37 — waitForDiagnostics resolves through the response seam. +// --------------------------------------------------------------------------- + +#[test] +fn acc37_wait_for_diagnostics_resolves_through_the_response_seam() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a : Nat := 1\n"); + let mut state = editor(&fx); + open(&state, &file); + settle(&mut state); + + exec( + &state, + r#" + _G.settled = "never" + local rec = pmacs.lsp.active_attachment() + pmacs.lean.wait_for_diagnostics(rec.server, rec.uri, function(err) + _G.settled = tostring(err) + end) + "#, + ); + settle(&mut state); + + assert_eq!( + eval::(&state, "return _G.settled"), + "nil", + "the reply reaches the callback with no error — this is the \ + Stage 3a response seam carrying its first production caller" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 29, Lean's side — `$/lean/fileProgress` reaches the module. +// +// Driven end-to-end through the real drain: the fake server's +// `leanprogress` mode emits the notification on didOpen. Calling the +// handler directly would pin nothing about the wiring, which is the only +// part that can break. +// --------------------------------------------------------------------------- + +#[test] +fn file_progress_notification_is_recorded_for_its_document() { + 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); + exec( + &state, + "pmacs.lsp.config.lean4.env = { PMACS_FAKE_LSP_MODE = \"leanprogress\" }", + ); + + // Nothing recorded before the server speaks — so the assertion below + // cannot pass on a pre-populated table. + let before: i64 = eval( + &state, + "local n = 0 for _ in pairs(pmacs.lean.file_progress) do n = n + 1 end return n", + ); + assert_eq!(before, 0); + + open(&state, &file); + settle(&mut state); + + let uri: String = eval( + &state, + r#" + for k, v in pairs(pmacs.lean.file_progress) do + if type(v) == "table" and v[1] and v[1].range then return k end + end + return "none" + "#, + ); + assert!( + uri.starts_with("file://") && uri.ends_with("A.lean"), + "the subscriber recorded the processing ranges under the \ + document uri; saw {uri:?}" + ); +} + +// --------------------------------------------------------------------------- +// Q#LN20 in the Lean resolver — a symlinked open reuses one server. +// --------------------------------------------------------------------------- + +#[test] +fn lean_root_is_canonical_so_a_symlinked_open_reuses_one_server() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let real = fx.write("pkg/A.lean", "def a := 1\n"); + std::os::unix::fs::symlink(fx.dir("pkg"), fx.dir("linkpkg")).unwrap(); + let linked = fx.dir("linkpkg").join("A.lean"); + + let mut state = editor(&fx); + open(&state, &real); + settle(&mut state); + assert_eq!(rows(&state).len(), 1, "the real path spawns one server"); + + open(&state, &linked); + settle(&mut state); + assert_eq!( + rows(&state).len(), + 1, + "the symlinked path reuses it — the resolver canonicalizes, so \ + both spellings produce the same affinity key" + ); +} diff --git a/tests/lean4_stage1_acceptance.rs b/tests/lean4_stage1_acceptance.rs index d48a86c..9aafcab 100644 --- a/tests/lean4_stage1_acceptance.rs +++ b/tests/lean4_stage1_acceptance.rs @@ -305,36 +305,50 @@ fn acc11b_an_unknown_fence_name_still_injects_nothing() { // --------------------------------------------------------------------------- #[test] -fn acc12_stage1_ships_no_lsp_config_and_spawns_no_process() { - // Stage 1 is grammar + Lua tables only. Opening a Lean file must not - // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and - // even then it is fallible by design (Q#LN7). +fn acc12_opening_lean_spawns_no_process_without_a_server_config() { + // **Superseded in half by Stage 3b.** This criterion originally also + // asserted `pmacs.lsp.config.lean4 == nil`, guarding against a Stage-3 + // front-run. Stage 3b *is* Stage 3: `builtin/runtime/lean.lua` now ships + // that config deliberately, and its shape is pinned by + // `tests/lean4_server_acceptance.rs`. Asserting the absence here would + // now pin the opposite of the intended behavior, so it is gone rather + // than weakened. + // + // What survives is the half that was always about *restraint*, and it + // matters more now than it did in Stage 1 — it is what holds Q#LN7's + // "not at init" promise. `pmacs.lsp.config` is a declarative table, and + // spawning a process at startup for every user, Lean-using or not, is + // the cost rev 1 refused. Both the `lake serve` spawn and the + // `lake --version` probe are gated on a real Lean attachment. - // The load-bearing assertion, and it must run against a PRISTINE editor. - // The shared `editor()` helper wipes `pmacs.lsp.config` before any - // buffer opens, so an assertion about the server list under that harness - // holds for every language regardless of what Stage 1 ships — it could - // not fail for the regression it names. This checks the real claim - // directly: no builtin runtime file defines a Lean server config. A - // Stage-3 front-run adding `pmacs.lsp.config.lean4` fails here. + // Constructing an editor touches no process, even though the Lean + // config now exists and names `lake`. let pristine = EditorState::new(); - let no_lean_config: bool = eval(&pristine, "return pmacs.lsp.config.lean4 == nil"); - assert!( - no_lean_config, - "Stage 1 defines no `pmacs.lsp.config.lean4`; the LSP is Stage 3" + let at_init: i64 = eval(&pristine, "return #pmacs.process.list()"); + assert_eq!( + at_init, 0, + "constructing an editor must not probe or spawn for Lean" + ); + // Non-vacuity for the assertion above: the config really is present and + // really does name a command, so "nothing spawned" is restraint rather + // than an empty table having nothing to act on. + let names_lake: bool = eval( + &pristine, + "return pmacs.lsp.config.lean4 ~= nil and pmacs.lsp.config.lean4.command == \"lake\"", ); - // Non-vacuity: the same lookup finds the configs that DO ship, so this - // is not passing because `pmacs.lsp.config` is empty or absent. - let rust_config_exists: bool = eval(&pristine, "return pmacs.lsp.config.rust ~= nil"); assert!( - rust_config_exists, - "the config table is populated, so the lean4 absence above is meaningful" + names_lake, + "Stage 3b ships a lean4 config naming `lake`, so the no-spawn \ + assertion above is meaningful" ); - // And nothing is spawned by opening the file. This half retains its - // value under the wiped config: a direct probe spawn from `lean.lua` - // would show up here whatever `pmacs.lsp.config` contains. + // And opening a Lean buffer with no server configured spawns nothing — + // the `editor()` helper wipes `pmacs.lsp.config`, so this catches a + // probe that fires off the mode rather than off an attachment. let s = editor_visiting("Basic.lean", "def x : Nat := 1\n"); let procs: i64 = eval(&s, "return #pmacs.process.list()"); - assert_eq!(procs, 0, "opening a Lean buffer spawns no child process"); + assert_eq!( + procs, 0, + "with no server configured, opening a Lean buffer spawns nothing" + ); } From 914bf3f02f472774e79792347a23ff190d631e34 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 17:40:31 -0400 Subject: [PATCH 2/9] docs: record the Stage 3b lane and its stacking constraint --- docs/active-work.md | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/docs/active-work.md b/docs/active-work.md index aef6edc..99b54ea 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -54,7 +54,7 @@ git status --short --branch The `git log` command must expose `0dd16a5` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; Stage 3a IN REVIEW +## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review round, all twelve checks green). Branch `githubsucks/lean4-stage1` @@ -252,6 +252,43 @@ If it does not, stop and repair the remote/fetch configuration. `#[cfg(unix)]` is NOT sufficient for such a fixture — `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. +### Stage 3b — the Lean language server (branch `lean4-stage3b-server`) + +- Same worktree `../pmacs-lean-stage3`, **branched off + `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response + seam and `pmacs.fs.canonicalize`, so it is strictly sequential and its + PR must be retargeted to `main` only after #167 merges. (Kill-ring + lesson: retarget stacked child PRs BEFORE merging the parent.) +- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in + `src/editor.rs`, a `leanprogress` mode on `pmacs_fake_lsp`, and + `tests/lean4_server_acceptance.rs` (17 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 + Stage-3 front-run; 3b is that stage. What survives is the restraint + half — constructing an editor spawns nothing though the config now + names `lake`, and opening a Lean buffer with no server configured + spawns nothing — which is what holds Q#LN7's "not at init" promise. +- **The marker test is wrong in two opposite directions if done naively** + and both are pinned: `io.open` SUCCEEDS on a directory (so truthiness + accepts a `lean-toolchain` dir), but requiring a non-nil read rejects + an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, + not content). Discriminator is `read`'s SECOND return; decline only on + a non-nil err. Probed on LuaJIT 2.1. +- Four bites recorded, each against the committed tree: bare `io.open` + → 24a fails / 24b passes; require-non-nil → 24b fails / 24a passes; + no canonicalization → symlinked open spawns two servers; no stop + before fallback → acc36 fails. +- The probe's non-zero exit is deliberately NOT a fallback trigger — + §2.9's elan shim makes `lake --version` fail where `lake serve` still + 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 17/17; 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. + ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next - Approved framing: `docs/dired-framing.md` (revision 5), landing as its From cdaea66203aed112a11e3f3b729a2cc212197904 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 18:03:29 -0400 Subject: [PATCH 3/9] fix(lean): make the fallback actually produce a working server MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 1 review, four P1s. All real; the first two mean the fallback did not work at all. **1. The latch swapped the config but never spawned or re-attached.** Nothing re-fires an attach on a config change and `attach_buffer` early-returns for a live attachment, so the buffer stayed bound to the server that had just been stopped. The user got a config edit and no language server. `fire_latch` now rebuilds through a new `pmacs.lsp._attach_buffer` export. Two mechanics had to be right for that rebuild to happen at all: * It is **retried on the tick**, because `pmacs.lsp.stop` leaves the state `shutting-down`, which `server_is_live` counts as LIVE — an inline re-attach early-returns the stale record and the swap is a silent no-op. * The latch **does not stop an already-terminal server**, and this is a substrate bug worked around rather than a style choice. `LspManager::stop` on a `Crashed` client takes its not-initialized branch, terminates the dead process, and sets `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 the client is stuck in `ShuttingDown` forever: `server_is_live` reads it as live so `attach_buffer` never rebuilds, and `forget` refuses it for not being terminal. Stopping a dead server is what makes it un-replaceable. Named in framing §6; the fix belongs in `stop` and changes behavior for every language. **2. A missing `lake` bypassed probe and latch entirely** — the single most likely real failure. `ensure_server` swallows a synchronous ENOENT and returns nil, so there was no attachment, and the hook keyed on `active_attachment()` returned before arming anything. The hook now keys on the buffer's LANGUAGE and treats a Lean buffer with no attachment as the failure itself. **3. `waitForDiagnostics` omitted `version`.** Lean's `WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0, `src/Lean/Data/Lsp/Extra.lean`); the request is how a client says which revision it wants. It looked correct only because the fake server echoes any payload — so the fake server now validates and returns InvalidParams without it. **4. The ledger stated the dangerous stacking order** in one sentence and the correct rule in the next. Fixed to say BEFORE. A safety rule written twice with opposite senses is worse than not written. Also (P2): the probe/latch suite now drives the production path — `buffer.after-load` -> ticks -> probe drain -> latch -> re-attach — with real executable stubs, and asserts the originally opened buffer ends up on a LIVE server. Round 1's acceptance 36 asserted every server was terminal, i.e. pinned the ABSENCE of the fallback it claimed to test. `M.fallback` is a table so the suite can point it at a working stand-in; the probe now spawns `cfg.command --version` rather than a hardcoded `lake`, which is also more correct for a user who configured a wrapper. `swap_to_fallback`'s `command ~= "lake"` guard is gone: the latch fires only when the configured server actually failed, one visible fallback beats no server, and `probe.latched` is what keeps it to exactly one. Three new bites, all against the committed tree: no re-attach after the swap -> three latch tests fail; hook keyed on the attachment -> the missing-`lake` case fails; `waitForDiagnostics` without `version` -> acc37 fails with the server's InvalidParams. --- builtin/runtime/lean.lua | 163 +++++++++++--- builtin/runtime/lsp.lua | 18 ++ docs/active-work.md | 40 +++- docs/lean4-mode-framing.md | 24 ++- src/bin/pmacs_fake_lsp.rs | 33 +++ tests/lean4_server_acceptance.rs | 350 +++++++++++++++++++++++-------- 6 files changed, 510 insertions(+), 118 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 3fe73da..dd98892 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -142,6 +142,19 @@ 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) + local ok, rows = pcall(pmacs.lsp.list) + if not ok or not rows then return nil end + for _, info in ipairs(rows) do + if tostring(info.id) == skey then + return info.state and info.state.kind + end + end + return nil +end + local function version_below_3_1(text) local major, minor = text:match("(%d+)%.(%d+)") if not major then return false end @@ -150,15 +163,27 @@ 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" } } + -- Swap `command`/`args` ONLY. A wholesale table replacement would -- silently discard a user's `env` / `settings` / `init_options` / `root` -- from `init.lua` at exactly the moment they are least likely to notice. -local function swap_to_lean_server() +-- +-- The only guard is idempotence — already-the-fallback means nothing to +-- do. It deliberately does NOT refuse when the command is user-supplied: +-- the latch fires only when the configured Lean server actually failed +-- to start, and one visible fallback attempt beats leaving the user with +-- no server at all. `probe.latched` is what keeps it to exactly one. +local function swap_to_fallback() local cfg = pmacs.lsp.config.lean4 if not cfg then return false end - if cfg.command ~= "lake" then return false end - cfg.command = "lean" - cfg.args = { "--server" } + if cfg.command == M.fallback.command then return false end + cfg.command = M.fallback.command + cfg.args = M.fallback.args return true end @@ -172,16 +197,66 @@ end -- 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. +local try_reattach + local function fire_latch(sid, why) if probe.latched then return end probe.latched = true - if sid then pcall(pmacs.lsp.stop, sid) end - if swap_to_lean_server() then - report("LSP: lean4 " .. why .. "; falling back to `lean --server`") - else - report("LSP: lean4 " .. why) - end 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 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. + -- + -- **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. + 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. +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 + return false + end + probe.reattach_from = nil + return true end local function drain_probe() @@ -220,13 +295,17 @@ local function start_probe(root) if probe.started then return end probe.started = true local cfg = pmacs.lsp.config.lean4 - if not cfg or cfg.command ~= "lake" then return end + if not cfg or not cfg.command 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). local spec = { -- COHERENCE §9: `ProcessSpec.label` is the only identity a process -- carries, and it is what `pmacs.process.list` renders. A user -- wondering why their editor touched `lake` finds an owner here. label = "lean:lake-version-probe", - command = "lake", + command = cfg.command, args = { "--version" }, stdin = "null", } @@ -275,12 +354,20 @@ end -- does not apply. Resolves when the server has finished elaborating. -- Awaited through Stage 3a's response seam. -- +-- **`version` is required, not optional.** Lean's +-- `WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0, +-- `src/Lean/Data/Lsp/Extra.lean`), and the request is how the client +-- says *which* revision of the document it wants elaboration for. +-- Sending only `uri` is a malformed request against a real server; it +-- happened to look fine here because the fake server echoes any +-- payload. Callers pass the attachment's current `version`. +-- -- `fn(err)` is called with nil on success. Registering the one-shot -- requires the server to have an attached buffer — see the note on -- `pmacs.lsp.on_response`; every caller here comes from an attachment. -function M.wait_for_diagnostics(sid, uri, fn) +function M.wait_for_diagnostics(sid, uri, version, fn) local ok, rid = pcall(pmacs.lsp.send_request, sid, - "textDocument/waitForDiagnostics", { uri = uri }) + "textDocument/waitForDiagnostics", { uri = uri, version = version }) if not ok then if fn then pcall(fn, tostring(rid)) end return nil @@ -303,7 +390,7 @@ pmacs.command.define { return end pmacs.editor.set_status("lean: elaborating…") - M.wait_for_diagnostics(rec.server, rec.uri, function(err) + M.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) if err then pmacs.editor.set_status("lean: " .. tostring(err)) else @@ -327,27 +414,53 @@ end) -- Wiring -------------------------------------------------------------- --- Runs after `lsp.lua`'s own `buffer.after-load` subscription, so the --- attachment already exists. The attachment's `language` IS the Lean --- test — no separate major-mode lookup, which would be a second source --- of truth for the same question. +-- Runs after `lsp.lua`'s own `buffer.after-load` subscription. +-- +-- **Keyed on the buffer's LANGUAGE, not on an attachment existing.** +-- Round 1 keyed on `active_attachment()` and returned early when it was +-- nil — which silently excluded the single most likely real-world +-- failure: `lake` not installed. `ensure_server` pcalls the spawn and +-- returns nil on ENOENT, so `attach_buffer` produces no record at all, +-- so the probe never started and the latch never armed. The case the +-- fallback exists for was the one case it could not see. pmacs.hook.add("buffer.after-load", function() - local rec = pmacs.lsp.active_attachment() - if not rec or rec.language ~= "lean4" then return end + local buf = pmacs.window.buffer() + if not buf then return end + 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 - -- Watch only the FIRST Lean server: the latch is per session. - if not probe.latched and not probe.saw_initialized - and probe.watching == nil then - probe.watching = rec.server + + local rec = pmacs.lsp.active_attachment() + if rec and rec.language == "lean4" then + -- Watch only the FIRST Lean server: the latch is per session. + if not probe.latched and not probe.saw_initialized + and probe.watching == nil then + probe.watching = rec.server + end + 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. + if not probe.latched then + fire_latch(nil, "`" .. tostring( + pmacs.lsp.config.lean4 and pmacs.lsp.config.lean4.command) + .. "` could not be started") end end) pmacs.hook.add("process.after-tick", function() drain_probe() poll_latch() + -- Keep trying until the stopped server is really gone; see the note in + -- `fire_latch`. + if probe.reattach_from ~= nil then try_reattach() end end) -- Test seam: acceptance drives the latch deterministically rather than diff --git a/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua index fd44f1a..0749cfa 100644 --- a/builtin/runtime/lsp.lua +++ b/builtin/runtime/lsp.lua @@ -893,6 +893,24 @@ function pmacs.lsp.active_attachment() return attachments[tostring(buf)] end +-- Re-run the attach for the ACTIVE buffer, rebuilding it against the +-- current `pmacs.lsp.config`. +-- +-- Exists for the Arc 8 Stage 3b fallback latch (Q#LN7): after that latch +-- stops a server that failed to start and rewrites `config.lean4`, +-- something has to actually spawn the replacement and re-point the +-- buffer at it. Nothing else does — `attach_buffer` early-returns for a +-- live attachment, and no hook re-fires on a config change, so without +-- this the buffer stays bound to the stopped server and the "fallback" +-- is a config edit with no effect. +-- +-- Deliberately keyed on the active buffer, matching `attach_buffer`'s +-- own use of `active_buffer_path()`; it is not a general re-attach for +-- arbitrary buffers and must not be used as one. +function pmacs.lsp._attach_buffer() + return attach_buffer(pmacs.window.buffer()) +end + -- Arc 4 stage 3: pure modeline projection. This reads the private -- per-buffer attachment map directly so passive split windows report their -- own buffer instead of the focused window. It never attaches, flushes diff --git a/docs/active-work.md b/docs/active-work.md index 99b54ea..1a1e7ae 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -256,12 +256,17 @@ If it does not, stop and repair the remote/fetch configuration. - Same worktree `../pmacs-lean-stage3`, **branched off `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response - seam and `pmacs.fs.canonicalize`, so it is strictly sequential and its - PR must be retargeted to `main` only after #167 merges. (Kill-ring - lesson: retarget stacked child PRs BEFORE merging the parent.) + seam and `pmacs.fs.canonicalize`, so it is strictly sequential. + **Retarget PR #170 to `main` BEFORE merging #167, not after** — the + kill-ring lesson exactly. (Round 1 of this ledger entry stated the + reverse in its first sentence and the correct rule in the next; the + review caught it. A safety rule written twice with opposite senses is + worse than not written.) - Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in - `src/editor.rs`, a `leanprogress` mode on `pmacs_fake_lsp`, and - `tests/lean4_server_acceptance.rs` (17 tests). No protocol change. + `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). + 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 Stage-3 front-run; 3b is that stage. What survives is the restraint @@ -274,10 +279,29 @@ If it does not, stop and repair the remote/fetch configuration. an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, not content). Discriminator is `read`'s SECOND return; decline only on a non-nil err. Probed on LuaJIT 2.1. -- Four bites recorded, each against the committed tree: bare `io.open` +- Seven bites recorded, each against the committed tree: bare `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a passes; - no canonicalization → symlinked open spawns two servers; no stop - before fallback → acc36 fails. + no canonicalization → symlinked open spawns two servers; no re-attach + after the swap → three latch tests fail; hook keyed on the attachment + → the missing-`lake` case fails; `waitForDiagnostics` without + `version` → acc37 fails with the server's InvalidParams. +- **SUBSTRATE BUG FOUND, not fixed here (framing §6).** + `LspManager::stop` on an ALREADY-terminal server takes its + not-initialized branch, terminates the dead process and sets + `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 the client is stuck in + `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so + `attach_buffer` never rebuilds, and `forget` refuses it for not being + terminal. **Stopping a dead server is what makes it un-replaceable.** + Lean works around it by checking the state before stopping. +- Round-1 review found four P1s, all real: the latch swapped the config + but never spawned or re-attached (and acc36 *asserted every server was + terminal*, pinning the absence of the fallback); a missing `lake` + bypassed probe and latch entirely because the hook keyed on an + attachment that ENOENT prevents; `waitForDiagnostics` omitted the + `version` Lean requires; and the ledger stated the dangerous stacking + order. - The probe's non-zero exit is deliberately NOT a fallback trigger — §2.9's elan shim makes `lake --version` fail where `lake serve` still works. Only a parseable version below 3.1.0 triggers it; the diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 4869252..fac090b 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1543,6 +1543,20 @@ What remains deferred: which events may be dropped, which is a policy question with user-visible consequences for diagnostics and progress; Stage 3a states the seam's contract around the behavior rather than changing it. +- **`LspManager::stop` on an already-terminal server strands it.** The + not-initialized branch terminates the (already-dead) process and sets + `ShuttingDown { shutdown_request_id: None }` on the premise that "the + next exit observation cleans up" — but for a `Crashed` client the exit + has already been observed, which is what produced that state. No + further event arrives, so the client sits in `ShuttingDown` + permanently: `server_is_live` counts it as live (neither crashed nor + 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. - **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 @@ -1722,9 +1736,13 @@ the blast radius. channel a user can actually observe; a report added through `pmacs.error` alone must fail this. - **37.** `textDocument/waitForDiagnostics` resolves through the response seam - (Q#LN16). **PATH-and-success-gated live smoke:** if `lake serve` - starts successfully a real elaboration completes and diagnostics - arrive; skipped otherwise, never failed. + (Q#LN16), **carrying both `uri` and `version`** — Lean's + `WaitForDiagnosticsParams` requires the document version, and a fake + server that echoes any payload will hide its absence, so the fixture + must reject a request that omits it. + **PATH-and-success-gated live smoke:** if `lake serve` starts + successfully a real elaboration completes and diagnostics arrive; + skipped otherwise, never failed. These two sections are bulleted with explicit labels rather than numbered, because the split leaves each stage's criteria non-contiguous diff --git a/src/bin/pmacs_fake_lsp.rs b/src/bin/pmacs_fake_lsp.rs index 5f4fab5..67d6620 100644 --- a/src/bin/pmacs_fake_lsp.rs +++ b/src/bin/pmacs_fake_lsp.rs @@ -1083,6 +1083,39 @@ fn main() { }); write_frame(&mut stdout, &resp); } + ("textDocument/waitForDiagnostics", Some(idv)) => { + // Arc 8 Stage 3b: Lean's `WaitForDiagnosticsParams` is + // `{ uri, version }` (v4.9.0 + // `src/Lean/Data/Lsp/Extra.lean`). Validated here rather + // than echoed, because the generic echo arm below + // accepts anything — which is exactly how a client + // sending only `uri` shipped looking correct. A client + // that omits `version`, or sends a non-integer, gets an + // InvalidParams error the way a real server would. + let uri_ok = params + .get("uri") + .and_then(serde_json::Value::as_str) + .is_some(); + let version_ok = params + .get("version") + .and_then(serde_json::Value::as_i64) + .is_some(); + let resp = if uri_ok && version_ok { + serde_json::json!({ + "jsonrpc": "2.0", "id": idv, "result": serde_json::Value::Null + }) + } else { + serde_json::json!({ + "jsonrpc": "2.0", + "id": idv, + "error": { + "code": -32602, + "message": "waitForDiagnostics requires { uri, version }" + } + }) + }; + write_frame(&mut stdout, &resp); + } (_, Some(idv)) => { // Generic echo response. let resp = serde_json::json!({ diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index 13cfcd0..6fe5ed4 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -347,12 +347,85 @@ fn acc26_did_open_carries_the_lean4_language_id() { } // --------------------------------------------------------------------------- -// Acceptance 28 (probe) — the version predicate. +// Acceptance 27 / 28 / 35 / 36 — the probe and the fallback latch. // -// The parse is unit-tested directly because the spawn path is timing- -// bound; the latch's *effect* is pinned separately below. +// **Driven through the production path**, not by calling internals. +// Round 1's versions poked `_fire_latch` directly and asserted on config +// mutation, which proved nothing about whether a server ever starts — +// and acceptance 36 went further and asserted every server was terminal, +// pinning the ABSENCE of the fallback it claimed to test. These go +// `buffer.after-load` -> ticks -> probe drain -> latch -> re-attach, and +// assert the originally opened buffer ends up on a LIVE server. +// +// The stubs are real executables the fixture writes. `M.fallback` is a +// table precisely so it can point at `pmacs_fake_lsp` here. // --------------------------------------------------------------------------- +impl Fixture { + /// An executable shell stub. `serve` sleeps (so the "server" does not + /// die and only the named failure mode is under test); `--version` + /// prints `version_line`. + fn lake_stub(&self, rel: &str, version_line: &str) -> PathBuf { + use std::os::unix::fs::PermissionsExt as _; + let path = self.root.join(rel); + std::fs::create_dir_all(path.parent().unwrap()).unwrap(); + std::fs::write( + &path, + format!( + "#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n echo '{version_line}'\n exit 0\nfi\nexec sleep 300\n" + ), + ) + .unwrap(); + std::fs::set_permissions(&path, std::fs::Permissions::from_mode(0o755)).unwrap(); + path + } +} + +/// Point `command` at `lake_cmd` and the latch's fallback at the fake +/// LSP server, so a fallback that fires produces a server that works. +fn with_fallback(state: &EditorState, lake_cmd: &Path) { + exec( + state, + &format!( + r#" + pmacs.lsp.config.lean4.command = "{}" + pmacs.lsp.config.lean4.args = {{ "serve" }} + pmacs.lean.fallback = {{ command = "{}", args = {{}} }} + "#, + lua_str(lake_cmd), + fake_lsp_path() + ), + ); +} + +/// The active buffer's attached server id, or "none". +fn attached_sid(state: &EditorState) -> String { + eval( + state, + r#" + local rec = pmacs.lsp.active_attachment() + return rec and tostring(rec.server) or "none" + "#, + ) +} + +/// State kind of the active buffer's attached server, or "none". +fn attached_state(state: &EditorState) -> 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" + "#, + ) +} + #[test] fn acc28_version_predicate_triggers_only_below_3_1() { let fx = Fixture::new(); @@ -374,36 +447,156 @@ fn acc28_version_predicate_triggers_only_below_3_1() { ); } -// --------------------------------------------------------------------------- -// Acceptance 27 / 35 / 36 — the fallback latch. -// --------------------------------------------------------------------------- +#[test] +fn acc28_an_old_lake_falls_back_and_the_buffer_lands_on_a_live_server() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let old_lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &old_lake); + + open(&state, &file); + settle(&mut state); + // The stub's `serve` sleeps rather than dying, so ONLY the probe can + // have caused a fallback here. That isolation is the point. + for _ in 0..40 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } + + assert_eq!( + attached_state(&state), + "initialized", + "an old lake must leave the buffer on a LIVE fallback server, not \ + merely rewrite the config" + ); + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!(cmd, fake_lsp_path(), "the fallback command is in effect"); +} + +#[test] +fn acc28_a_current_lake_does_not_trigger_the_fallback() { + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let new_lake = fx.lake_stub("bin/lake", "Lake version 3.1.0"); + let mut state = editor(&fx); + with_fallback(&state, &new_lake); + + open(&state, &file); + for _ in 0..20 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + } + + // Non-vacuity against the test above: same harness, same stub shape, + // only the version differs — so a latch that fired unconditionally + // would be caught here. + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!( + cmd, + new_lake.display().to_string(), + "a current lake keeps its command; the probe must not fall back" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!(!latched, "the latch did not arm"); +} + +#[test] +fn acc27_a_missing_lake_falls_back_and_the_buffer_lands_on_a_live_server() { + // The case round 1 could not see at all: `ensure_server` swallows a + // synchronous ENOENT and returns nil, so there is no attachment to + // key off. This is also the most likely real-world failure — a user + // with `lean` but no `lake`. + 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); + + open(&state, &file); + for _ in 0..40 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } + + assert_eq!( + attached_state(&state), + "initialized", + "a missing `lake` must fall back to a live server and re-attach \ + the buffer that was already open" + ); + let status = state.core.borrow().status.clone(); + assert!( + status.contains("lean4"), + "and it says so on the status line; saw {status:?}" + ); +} + +#[test] +fn acc27_the_latch_is_one_shot_and_does_not_re_arm() { + 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); + + open(&state, &file); + settle(&mut state); + let after_first: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!(after_first, fake_lsp_path(), "the fallback fired once"); + + // A user who deliberately sets something else after the fallback must + // not have it silently replaced by a second firing. + exec(&state, "pmacs.lsp.config.lean4.command = \"user-choice\""); + exec(&state, "pmacs.lean._fire_latch(nil, \"a second failure\")"); + assert_eq!( + eval::(&state, "return pmacs.lsp.config.lean4.command"), + "user-choice", + "the latch never re-arms within a session" + ); +} #[test] fn acc35_latch_preserves_user_config_and_swaps_only_command_and_args() { let fx = Fixture::new(); - let state = editor(&fx); - // A user's init.lua settings, on the shipped shape. + 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, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lsp.config.lean4.env = { MYVAR = "1" } + r" pmacs.lsp.config.lean4.settings = { lean = { verbose = true } } pmacs.lsp.config.lean4.init_options = { hasWidgets = false } _G.root_before = pmacs.lsp.config.lean4.root - pmacs.lean._fire_latch(nil, "test") - "#, + ", ); + open(&state, &file); + settle(&mut state); + let after: String = eval( &state, r#" local c = pmacs.lsp.config.lean4 return table.concat({ - tostring(c.command), - tostring(c.args and c.args[1]), - tostring(c.env and c.env.MYVAR), tostring(c.settings and c.settings.lean and c.settings.lean.verbose), tostring(c.init_options and c.init_options.hasWidgets), tostring(c.root == _G.root_before), @@ -411,78 +604,70 @@ fn acc35_latch_preserves_user_config_and_swaps_only_command_and_args() { "#, ); assert_eq!( - after, "lean|--server|1|true|false|true", - "only command/args change; env, settings, init_options and root \ - survive the swap" - ); -} - -#[test] -fn acc27_the_latch_is_one_shot_and_does_not_re_arm() { - let fx = Fixture::new(); - let state = editor(&fx); - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(nil, "first failure") - _G.after_first = pmacs.lsp.config.lean4.command - -- A second failure must not rewrite the command again; if it did, - -- a user who deliberately set something else after the fallback - -- would have it silently replaced. - pmacs.lsp.config.lean4.command = "user-choice" - pmacs.lean._fire_latch(nil, "second failure") - _G.after_second = pmacs.lsp.config.lean4.command - "#, - ); - assert_eq!(eval::(&state, "return _G.after_first"), "lean"); - assert_eq!( - eval::(&state, "return _G.after_second"), - "user-choice", - "the latch never re-arms within a session" + after, "true|false|true", + "settings, init_options and root survive the swap; only \ + command/args change" ); } #[test] fn acc36_latch_stops_the_failing_server_before_spawning_the_fallback() { + // A stub whose `serve` exits immediately: the server dies before + // `initialize` completes, which is the failure the latch polls for. + // `RestartPolicy::OnCrash` would otherwise respawn it forever + // underneath the latch, with no attempt ceiling. + 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\nif [ \"$1\" = \"--version\" ]; then echo 'Lake version 9.9.9'; exit 0; fi\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); - settle(&mut state); - assert_eq!(rows(&state).len(), 1, "precondition: one server is up"); + for _ in 0..60 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + if attached_state(&state) == "initialized" { + break; + } + } - // Fire the latch against the live server, exactly as `poll_latch` - // would. `pmacs.lsp.stop` sets `restart = Never` on the way out — - // which is what prevents `RestartPolicy::OnCrash` from respawning the - // broken command underneath the latch, forever, with no attempt cap. - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(pmacs.lsp.list()[1].id, "failed to start") - "#, + // The load-bearing assertion: the buffer ends up on a LIVE server. + assert_eq!( + attached_state(&state), + "initialized", + "the failing server is stopped and the buffer re-attached to the \ + fallback — not left terminal" ); - settle(&mut state); - - let terminal: bool = eval( + // And the dead one really is stopped, so nothing is respawning it. + let dying_still_running: bool = eval( &state, r#" + local live = tostring(pmacs.lsp.active_attachment().server) for _, s in ipairs(pmacs.lsp.list()) do - local k = s.state and s.state.kind - if k ~= "stopped" and k ~= "crashed" then return false end + if tostring(s.id) ~= live then + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then return true end + end end - return true + return false "#, ); assert!( - terminal, - "the failing server is stopped, not left to be respawned under \ - the latch" + !dying_still_running, + "the failing server is not respawning underneath the latch" ); + assert_ne!(attached_sid(&state), "none"); } // --------------------------------------------------------------------------- @@ -492,23 +677,24 @@ fn acc36_latch_stops_the_failing_server_before_spawning_the_fallback() { #[test] fn acc36a_latch_leaves_a_status_line_trace() { let fx = Fixture::new(); - let state = editor(&fx); - exec( - &state, - r#" - pmacs.lsp.config.lean4.command = "lake" - pmacs.lsp.config.lean4.args = { "serve" } - pmacs.lean._fire_latch(nil, "`lake serve` failed to start") - "#, - ); + 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); + + open(&state, &file); + settle(&mut state); + let status = state.core.borrow().status.clone(); assert!( - status.contains("lean4") && status.contains("lean --server"), - "the fallback names itself and what it fell back to; saw {status:?}" + status.contains("lean4") && status.contains("falling back"), + "the fallback names the language and says it fell back; saw {status:?}" ); // The channel assertion is the point (COHERENCE §1.2): a report made // only through `pmacs.error` — undefined in production — would leave - // this empty while every other assertion here still passed. + // this empty while the fallback itself still worked, so the user + // would silently be on a different server than they configured. assert!(!status.is_empty()); } @@ -550,7 +736,7 @@ fn acc37_wait_for_diagnostics_resolves_through_the_response_seam() { r#" _G.settled = "never" local rec = pmacs.lsp.active_attachment() - pmacs.lean.wait_for_diagnostics(rec.server, rec.uri, function(err) + pmacs.lean.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err) _G.settled = tostring(err) end) "#, From 3377db070ae59232c3caca706d550629b11daaac Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 18:35:11 -0400 Subject: [PATCH 4/9] fix(lean): correct the server lifecycle; round 2 review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- builtin/runtime/lean.lua | 216 ++++++++++++++++++--------- docs/active-work.md | 12 +- docs/lean4-mode-framing.md | 12 +- tests/lean4_server_acceptance.rs | 247 ++++++++++++++++++++++++++++++- 4 files changed, 406 insertions(+), 81 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index dd98892..5f74792 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -125,7 +125,8 @@ local probe = { started = false, -- the `lake --version` probe has been spawned latched = false, -- the fallback has fired (or been ruled out) proc = nil, -- process id of the running probe - buf = "", -- accumulated probe stdout + out = "", -- accumulated probe stdout + buf_key = nil, -- tostring() of the buffer that started this watching = nil, -- sid we are waiting to see fail before initialize saw_initialized = false, } @@ -142,9 +143,9 @@ end -- `lake serve` below 3.1.0 starts a server that cannot answer, which is -- worse than failing: `lean4-mode` probes for exactly this and falls -- back to `lean --server`. Parses the leading `x.y` of a version line. --- State kind for `sid`, or nil if the manager has forgotten it. -local function server_state_kind(sid) - local skey = tostring(sid) +-- State kind for the server whose `tostring(id)` is `skey`, or nil if +-- the manager has forgotten it (which is itself a terminal answer). +local function server_state_kind_for_key(skey) local ok, rows = pcall(pmacs.lsp.list) if not ok or not rows then return nil end for _, info in ipairs(rows) do @@ -155,6 +156,10 @@ local function server_state_kind(sid) return nil end +local function server_state_kind(sid) + return server_state_kind_for_key(tostring(sid)) +end + local function version_below_3_1(text) local major, minor = text:match("(%d+)%.(%d+)") if not major then return false end @@ -163,11 +168,25 @@ local function version_below_3_1(text) return major == 3 and minor < 1 end --- What the latch falls back TO. A table rather than a literal so the --- acceptance suite can point it at a stand-in server and drive the real --- latch path end to end, instead of asserting on a config mutation that --- proves nothing about whether a server ever starts. -M.fallback = { command = "lean", args = { "--server" } } +-- What the latch falls back TO. +-- +-- **Underscored: a test seam, not supported user configuration.** It is +-- a table only so the acceptance suite can point it at a stand-in server +-- and drive the real latch path end to end, instead of asserting on a +-- config mutation that proves nothing about whether a server ever +-- starts. Presenting it as public config would owe framing, +-- documentation, validation and mutation semantics that nothing here +-- provides; users configure Lean through `pmacs.lsp.config.lean4`. +M._fallback = { command = "lean", args = { "--server" } } + +local function same_args(a, b) + a, b = a or {}, b or {} + if #a ~= #b then return false end + for i = 1, #a do + if a[i] ~= b[i] then return false end + end + return true +end -- Swap `command`/`args` ONLY. A wholesale table replacement would -- silently discard a user's `env` / `settings` / `init_options` / `root` @@ -181,81 +200,111 @@ M.fallback = { command = "lean", args = { "--server" } } local function swap_to_fallback() local cfg = pmacs.lsp.config.lean4 if not cfg then return false end - if cfg.command == M.fallback.command then return false end - cfg.command = M.fallback.command - cfg.args = M.fallback.args + -- Idempotence compares command AND args: the same command with + -- different arguments is not "already applied", and treating it as + -- such would silently skip a swap that still needed to happen. + if cfg.command == M._fallback.command + and same_args(cfg.args, M._fallback.args) then + return false + end + cfg.command = M._fallback.command + cfg.args = M._fallback.args return true end --- Fire the fallback: stop the failing server FIRST, then swap, then let --- the next attach spawn afresh. --- --- Stopping first is load-bearing, not defensive. The spec default is --- `LspRestartPolicy::OnCrash`, the termination handler never consults --- the exit code, and `maybe_restart` has no attempt ceiling — so a --- broken `lake` respawns forever on a backoff, underneath the latch, --- producing a loop the latch cannot see the end of. `pmacs.lsp.stop` --- sets `restart = Never` on the way out, which is what disarms it. The --- fallback is therefore a FRESH server, not a restart of the old one. +-- Retire the failed server, swap the command, then rebuild the +-- attachment on the buffer that started this. local try_reattach +-- Retire `sid` so it cannot come back. **Which call to use depends on +-- the state, and using the wrong one is worse than doing nothing:** +-- +-- * TERMINAL (`crashed` / `stopped`) -> `forget`. It requires a +-- terminal state and removes the client outright, which also drops +-- the `next_restart_at` the crash scheduled. `stop` here would take +-- its not-initialized branch and set `ShuttingDown { .. None }` on +-- the premise that "the next exit observation cleans up" — but the +-- exit already happened, which is what made it `Crashed`. No +-- further event arrives, so it sits in `ShuttingDown` forever: +-- `server_is_live` reads that as LIVE so `attach_buffer` never +-- rebuilds, and `forget` then refuses it for not being terminal. +-- * NON-TERMINAL -> `stop`. `forget` rejects it, and `stop` disables +-- restart and drives the polite shutdown. +-- +-- Round 1 skipped the call entirely for terminal servers. That avoided +-- the corruption but left `next_restart_at` armed, so the crashed +-- primary respawned 500ms later and kept respawning underneath the +-- live fallback — invisible to a test that stopped ticking first. +local function retire_server(sid) + local kind = server_state_kind(sid) + if kind == nil then return end + if kind == "crashed" or kind == "stopped" then + pcall(pmacs.lsp.forget, sid) + else + pcall(pmacs.lsp.stop, sid) + end +end + local function fire_latch(sid, why) if probe.latched then return end probe.latched = true probe.watching = nil - -- **Only stop a server that is not ALREADY terminal**, and this is - -- load-bearing rather than tidy. `LspManager::stop` on a crashed - -- client takes its not-initialized branch: it terminates the - -- (already-dead) process and sets `ShuttingDown { .. None }`, with the - -- comment "the next exit observation cleans up" — but the exit was - -- already observed, which is what made it `Crashed`. No further event - -- arrives, so the client stays in `ShuttingDown` forever: - -- `server_is_live` counts it as LIVE (neither crashed nor stopped) so - -- `attach_buffer` never rebuilds, and `LspManager::forget` refuses it - -- for not being terminal. Stopping a dead server is what makes it - -- un-replaceable. Recorded as a substrate deferral in the framing §6. - if sid then - local kind = server_state_kind(sid) - if kind and kind ~= "crashed" and kind ~= "stopped" then - pcall(pmacs.lsp.stop, sid) - end - end + if sid then retire_server(sid) end if not swap_to_fallback() then report("LSP: lean4 " .. why) return end report("LSP: lean4 " .. why .. "; falling back to `" - .. tostring(M.fallback.command) .. "`") - -- **Spawn the replacement and re-point the buffer at it.** Stopping - -- and rewriting the config is not a fallback on its own: nothing - -- re-fires an attach on a config change, and `attach_buffer` - -- early-returns for a live attachment, so without this the buffer - -- stays bound to the server we just stopped and the user is left with - -- a config edit and no language server. Round 1 shipped exactly that, - -- with an acceptance test that asserted every server was terminal — - -- i.e. that pinned the absence of the fallback it claimed to check. + .. tostring(M._fallback.command) .. "`") + -- **Spawn the replacement and re-point the buffer at it.** Swapping + -- the config is not a fallback on its own: nothing re-fires an attach + -- on a config change and `attach_buffer` early-returns for a live + -- attachment, so without this the buffer stays bound to the server we + -- just retired and the user has a config edit and no language server. -- - -- **Retried on the tick, not done inline**, and that is not caution: - -- `pmacs.lsp.stop` sends shutdown+exit and the state becomes - -- `shutting-down`, which `server_is_live` counts as LIVE. So an - -- immediate `_attach_buffer` early-returns the stale record and the - -- swap has no effect — the exact silent no-op this whole path exists - -- to avoid. Retrying until the old server actually reaches a terminal - -- state is what makes the rebuild happen. + -- The rebuild waits for two things, and conflating them is what made + -- round 2 wrong in two ways at once: + -- 1. the retired server actually reaching a terminal state (or + -- being gone) — `stop` leaves `shutting-down`, which + -- `server_is_live` counts as LIVE, so attaching before then + -- early-returns the stale record and the swap silently no-ops; + -- 2. the buffer that started this being the ACTIVE one, because + -- `_attach_buffer` is an active-buffer-only seam. The verdict + -- arrives asynchronously, so the user may well be somewhere else + -- by then — and "some attachment now names a different server" + -- is satisfied by an unrelated Rust buffer, which would clear the + -- retry while leaving the Lean buffer stale forever. probe.reattach_from = sid and tostring(sid) or false try_reattach() end --- Returns true once the active Lean buffer is attached to a server that --- is not the one the latch stopped. +-- Returns true when there is nothing left to do: either the initiating +-- buffer is attached to the replacement, or the replacement itself +-- failed and that has been reported. function try_reattach() if probe.reattach_from == nil then return true end - local ok, rec = pcall(pmacs.lsp._attach_buffer) - if not ok or not rec then return false end - if probe.reattach_from and tostring(rec.server) == probe.reattach_from then + -- (2) Wait for the initiating buffer to be the active one. + local buf = pmacs.window.buffer() + if not buf or not probe.buf_key or tostring(buf) ~= probe.buf_key then return false end + -- (1) Wait for the retired server to stop counting as live. + if probe.reattach_from then + local kind = server_state_kind_for_key(probe.reattach_from) + if kind ~= nil and kind ~= "crashed" and kind ~= "stopped" then + return false + end + end + -- Both conditions met: attempt the replacement EXACTLY ONCE. Cleared + -- first so a failing fallback cannot retry every tick forever — + -- acceptance 27 promises a second failure surfaces rather than loops. probe.reattach_from = nil + local ok, rec = pcall(pmacs.lsp._attach_buffer) + if not ok or not rec then + report("LSP: lean4 fallback `" .. tostring(M._fallback.command) + .. "` did not start either") + return false + end return true end @@ -265,7 +314,7 @@ local function drain_probe() if not ok or not evs then return end for _, ev in ipairs(evs) do if ev.kind == "stdout" or ev.kind == "stderr" then - probe.buf = probe.buf .. tostring(ev.bytes) + probe.out = probe.out .. tostring(ev.bytes) elseif ev.kind == "exited" or ev.kind == "signaled" or ev.kind == "crashed" then local proc = probe.proc @@ -279,7 +328,7 @@ local function drain_probe() -- question failure detection would otherwise answer slowly: an -- old-but-working lake that starts a useless server. if ev.kind == "exited" and ev.code == 0 - and version_below_3_1(probe.buf) then + and version_below_3_1(probe.out) then fire_latch(probe.watching, "lake is older than 3.1.0") end end @@ -296,10 +345,20 @@ local function start_probe(root) probe.started = true local cfg = pmacs.lsp.config.lean4 if not cfg or not cfg.command then return end + -- **Only probe something actually named `lake`.** `version_below_3_1` + -- parses the first `x.y` it finds anywhere in the output, which is a + -- rule about LAKE's output contract and nothing else. Run against a + -- user's wrapper it is a category error: a working `my-lean-wrapper` + -- reporting "wrapper 1.0" would be replaced despite its server having + -- initialized fine. The FAILURE latch stays command-agnostic — that + -- one keys on the server actually not starting, which is true of any + -- command — but the version rule only applies where its contract + -- holds. + local base = cfg.command:match("([^/]+)$") or cfg.command + if base ~= "lake" then return end -- Probe the binary we would actually run, not the literal string - -- "lake": a user pointing `command` at a wrapper or an absolute path - -- should have THAT probed, and a hardcoded name would silently probe - -- something else (or nothing). + -- "lake": a user pointing `command` at an absolute path to lake should + -- have THAT probed, not whatever `lake` resolves to on PATH. local spec = { -- COHERENCE §9: `ProcessSpec.label` is the only identity a process -- carries, and it is what `pmacs.process.list` renders. A user @@ -429,6 +488,11 @@ pmacs.hook.add("buffer.after-load", function() local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf) if not ok_lang or lang ~= "lean4" then return end + -- The buffer that started this, remembered for the asynchronous + -- rebuild: `_attach_buffer` acts on whatever is active when the + -- verdict lands, which may be a different buffer entirely. + probe.buf_key = tostring(buf) + if not probe.started then local path = pmacs.editor.file_path() start_probe(path and M.root_for(path) or nil) @@ -444,14 +508,21 @@ pmacs.hook.add("buffer.after-load", function() return end - -- No attachment for a Lean buffer means `ensure_server` could not - -- spawn at all — a synchronous ENOENT, already swallowed upstream. - -- That is not something to wait for; it is the failure itself, and - -- the only place it is still observable. + -- **Unconfigured is DISABLED, not failed.** A user who sets + -- `pmacs.lsp.config.lean4 = nil`, or clears its `command`, has turned + -- the Lean server off; reporting that "nil could not be started" is a + -- false alarm, and latching would poison the session so a later + -- configuration could never take effect. Only a CONFIGURED command + -- that produced no attachment is a failure. + local cfg = pmacs.lsp.config.lean4 + if not cfg or not cfg.command then return end + + -- No attachment for a Lean buffer with a configured command means + -- `ensure_server` could not spawn at all — a synchronous ENOENT, + -- already swallowed upstream. That is not something to wait for; it + -- is the failure itself, and the only place it is still observable. if not probe.latched then - fire_latch(nil, "`" .. tostring( - pmacs.lsp.config.lean4 and pmacs.lsp.config.lean4.command) - .. "` could not be started") + fire_latch(nil, "`" .. tostring(cfg.command) .. "` could not be started") end end) @@ -467,6 +538,7 @@ end) -- waiting on real process timing. Not part of the public surface. M._probe = probe M._fire_latch = fire_latch +M._try_reattach = try_reattach M._version_below_3_1 = version_below_3_1 pmacs.lean = M diff --git a/docs/active-work.md b/docs/active-work.md index 1a1e7ae..4a650da 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,7 +265,7 @@ If it does not, stop and repair the remote/fetch configuration. - Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`, a `leanprogress` mode plus `waitForDiagnostics` validation on - `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (20 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (25 tests). No protocol change. - **Stage 1's acceptance 12 is half superseded and was rewritten, not deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a @@ -308,10 +308,14 @@ If it does not, stop and repair the remote/fetch configuration. server-failure latch covers the rest. - Verification on this branch: `cargo fmt --check` clean; strict workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; - lean4 server 17/17; lean4 stage 1 9/9; dispatch seams 15/15; + lean4 server 25/25; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,206 across 94 suites, zero failures**; - `git diff --check` clean. + workspace sweep 3,214 across 94 suites, zero failures**; + `git diff --check` clean. (Round 1 of + this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the + fixes were pushed. The ledger's protocol is that verification + describes the pushed tree; recording it late is the #161 fmt-blocker + error in a slower form.) ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index fac090b..ec62980 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1553,10 +1553,14 @@ What remains deferred: stopped), so `attach_buffer` never rebuilds against it, and `LspManager::forget` refuses it for not being terminal. **Stopping a dead server is what makes it un-replaceable.** Found implementing - Stage 3b's latch, which works around it by checking the state before - stopping. The fix belongs in `stop` (treat an already-terminal client - as a no-op, or drive it straight to `Stopped`) and changes behavior - for every language, so it does not ride a Lean PR. + Stage 3b's latch, which works around it by dispatching on state: + `forget` for a terminal server (it requires terminal state, and + removing the client also drops the `next_restart_at` the crash armed), + `stop` for a live one. Merely *skipping* the call is not enough — that + leaves the restart timer running and the broken command respawns + underneath the fallback. The fix belongs in `stop` (treat an + already-terminal client as a no-op, or drive it straight to `Stopped`) + and changes behavior for every language, so it does not ride a Lean PR. - **Forwarding `cfg.restart` through `ensure_server`** — read by `lua_to_lsp_spec`, never set by the spawn table, so silently dropped on every auto-attach (found landing #161). Fixing it changes behavior for diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index 6fe5ed4..cba8792 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -390,7 +390,7 @@ fn with_fallback(state: &EditorState, lake_cmd: &Path) { r#" pmacs.lsp.config.lean4.command = "{}" pmacs.lsp.config.lean4.args = {{ "serve" }} - pmacs.lean.fallback = {{ command = "{}", args = {{}} }} + pmacs.lean._fallback = {{ command = "{}", args = {{}} }} "#, lua_str(lake_cmd), fake_lsp_path() @@ -824,3 +824,248 @@ fn lean_root_is_canonical_so_a_symlinked_open_reuses_one_server() { both spellings produce the same affinity key" ); } + +// --------------------------------------------------------------------------- +// Round-2 review findings. Each of these fails against the code as it +// stood at cdaea66, where the focused suite was already 20/20 — the +// lifecycle defects were invisible to it. +// --------------------------------------------------------------------------- + +/// Tick for at least `ms`, so a 500ms restart backoff actually elapses. +/// The round-2 defect was invisible precisely because the suite stopped +/// ticking as soon as the fallback initialized, ~300ms in. +fn tick_for(state: &mut EditorState, ms: u64) { + let deadline = std::time::Instant::now() + Duration::from_millis(ms); + while std::time::Instant::now() < deadline { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(5)); + } +} + +#[test] +fn r2_crashed_primary_does_not_respawn_underneath_the_fallback() { + // The crash schedules `next_restart_at`; `maybe_restart` fires after + // the 500ms backoff with no attempt ceiling. Skipping the retire + // call (round 2) left that armed, so the broken command kept + // respawning under the live fallback — forever, unobserved. + use std::os::unix::fs::PermissionsExt as _; + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let dying = fx.root.join("bin/dying-lake"); + std::fs::create_dir_all(dying.parent().unwrap()).unwrap(); + std::fs::write(&dying, "#!/bin/sh\nexit 3\n").unwrap(); + std::fs::set_permissions(&dying, std::fs::Permissions::from_mode(0o755)).unwrap(); + + let mut state = editor(&fx); + with_fallback(&state, &dying); + open(&state, &file); + // Well past one backoff. + tick_for(&mut state, 1400); + + // **`attempt`, not liveness.** A respawning server spends most of + // its life in `crashed` waiting out the backoff, so "no live + // non-fallback server" is satisfied while it loops forever — that + // weaker assertion passed against the round-2 code and caught + // nothing. `attempt` increments on every spawn, so it counts the + // respawns directly. A retired server is absent from the list + // entirely (`forget` removes the client); one left with + // `next_restart_at` armed climbs past 1. + let worst_attempt: i64 = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + local live = rec and tostring(rec.server) or "" + local worst = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) ~= live then + local a = s.attempt or 0 + if a > worst then worst = a end + end + end + return worst + "#, + ); + assert_eq!( + worst_attempt, 0, + "the retired primary is gone from the manager, not respawning after the backoff (attempt > 0 means it is still there; > 1 means it respawned)" + ); + assert_eq!( + attached_state(&state), + "initialized", + "and the buffer is on the live fallback" + ); +} + +#[test] +fn r2_reattach_targets_the_originating_buffer_not_whatever_is_active() { + // `_attach_buffer` is an active-buffer-only seam and the latch's + // verdict arrives asynchronously. Round 2 accepted "some attachment + // now names a different server", which an unrelated Rust buffer + // satisfies — clearing the retry and stranding the Lean buffer. + // + // **Driven through the PROBE**, not through a missing executable: a + // missing command fails synchronously inside `buffer.after-load`, + // where the Lean buffer is still active and the rebuild happens + // inline, so the race cannot occur and the test proves nothing. The + // probe's verdict lands on a later tick, which is the whole point. + // The stub's `serve` sleeps, so only the probe can trigger anything. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + fx.write("pkg/Cargo.toml", "[package]\nname = \"p\"\n"); + let lean_file = fx.write("pkg/A.lean", "def a := 1\n"); + let rust_file = fx.write("pkg/src/main.rs", "fn main() {}\n"); + let old_lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + + let mut state = editor(&fx); + with_fallback(&state, &old_lake); + // A working Rust server, so switching away lands on a real + // attachment with a different server id — the decoy. + exec( + &state, + &format!( + "pmacs.lsp.config.rust = {{ command = \"{}\" }}", + fake_lsp_path() + ), + ); + + open(&state, &lean_file); + exec(&state, "_G.lean_buf = pmacs.window.buffer()"); + // Switch away before the probe's verdict can land. + open(&state, &rust_file); + tick_for(&mut state, 500); + + // Come back with a buffer SWITCH, not `find_or_open`. Re-opening + // fires `buffer.after-load`, which re-runs lsp.lua's own attach and + // would repair the record no matter what the latch did. + exec(&state, "pmacs.window.switch_buffer(_G.lean_buf)"); + tick_for(&mut state, 400); + + let lang: String = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + return rec and tostring(rec.language) or "none" + "#, + ); + assert_eq!(lang, "lean4", "we are back on the Lean buffer"); + + // The observable that discriminates: WHICH command the Lean buffer's + // server is running. A retry cleared by the decoy leaves it on the + // original `lake` stub. + let cmd: String = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + if not rec then return "none" end + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) == tostring(rec.server) then + return tostring(s.command) + end + end + return "gone" + "#, + ); + assert_eq!( + cmd, + fake_lsp_path(), + "the ORIGINATING Lean buffer ends up on the fallback — a decoy \ + Rust attachment must not satisfy the retry" + ); +} + +#[test] +fn r2_a_failing_fallback_is_reported_once_and_does_not_retry_forever() { + // Acceptance 27 promises a second failure surfaces rather than + // loops. Round 2 retried `_attach_buffer` every tick with nothing + // reported. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let absent_primary = fx.dir("bin/no-such-lake"); + let absent_fallback = fx.dir("bin/no-such-lean"); + + let mut state = editor(&fx); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.lean4.command = "{}" + pmacs.lsp.config.lean4.args = {{ "serve" }} + pmacs.lean._fallback = {{ command = "{}", args = {{}} }} + "#, + lua_str(&absent_primary), + lua_str(&absent_fallback) + ), + ); + + open(&state, &file); + tick_for(&mut state, 300); + + let status = state.core.borrow().status.clone(); + assert!( + status.contains("did not start either"), + "a failing fallback surfaces rather than retrying silently; saw \ + {status:?}" + ); + // And the retry state is cleared, so it is not looping. + let pending: String = eval(&state, "return tostring(pmacs.lean._probe.reattach_from)"); + assert_eq!(pending, "nil", "the retry is retired, not spinning"); +} + +#[test] +fn r2_a_working_wrapper_is_not_version_probed_as_lake() { + // `version_below_3_1` encodes LAKE's output contract. Applying it to + // an arbitrary wrapper is a category error: a working wrapper + // reporting its own "wrapper 1.0" would be replaced despite its + // server initializing fine. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + // Named something other than `lake`, reporting a sub-3.1 version, + // but which serves fine. + let wrapper = fx.lake_stub("bin/my-lean-wrapper", "wrapper 1.0"); + let mut state = editor(&fx); + with_fallback(&state, &wrapper); + + open(&state, &file); + tick_for(&mut state, 400); + + let cmd: String = eval(&state, "return pmacs.lsp.config.lean4.command"); + assert_eq!( + cmd, + wrapper.display().to_string(), + "a wrapper's own version string is not Lake's; the version probe \ + must not run against it" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!(!latched, "and the latch stayed disarmed"); +} + +#[test] +fn r2_an_unconfigured_lean_server_is_disabled_not_failed() { + // Setting `pmacs.lsp.config.lean4 = nil` means "off". Reporting that + // `nil` could not start is a false alarm, and latching poisons the + // session so a later configuration can never take effect. + let fx = Fixture::new(); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let mut state = editor(&fx); + exec(&state, "pmacs.lsp.config.lean4 = nil"); + exec(&state, "pmacs.editor.set_status(\"\")"); + + open(&state, &file); + settle(&mut state); + + assert_eq!( + state.core.borrow().status.clone(), + "", + "an unconfigured Lean server reports nothing — it is disabled" + ); + let latched: bool = eval(&state, "return pmacs.lean._probe.latched"); + assert!( + !latched, + "and the session is not poisoned: a later config must still work" + ); +} From 73587b0e371f49c26c87926941fe7518cce54004 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 19:23:50 -0400 Subject: [PATCH 5/9] fix(lean): correlate the probe verdict with its own server and buffer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 3 review: two P1 asynchronous-correlation defects, with the focused suite at 25/25 while both were live. **1. A late version verdict retired nothing and claimed success.** `probe.watching` is cleared the moment the server initializes — it is failure-polling state. A slow `lake --version` landing after a successful initialize therefore reached `fire_latch(nil)`, which retires nothing: `_attach_buffer` found the still-live primary attachment, early-returned it, and the retry counted that as done. Status said "falling back", the config named the fallback, and the buffer stayed on the old server. **That is the round-1 silent no-op arriving through a third event ordering** — first as "no re-attach at all", then as "re-attach cleared by an unrelated buffer", now as "re-attach satisfied by the server we were supposed to replace". The fix separates the two facts that were being carried by one field: `probe.primary` is the server the verdict applies to and survives initialization; `probe.watching` is the failure poll and is cleared by it. The existing fixture could not reach this ordering at all — its `serve` sleeps, so the primary can never initialize before `--version` returns. The new one execs the fake LSP for `serve` and delays 0.6s before reporting 3.0.0. **2. `buf_key` was the most recently loaded Lean buffer.** Written on every Lean `buffer.after-load`, so a second Lean file opened before the verdict became the rebuild target while the latch still watched the FIRST buffer's server. Target buffer and primary server are one fact and are now armed together, exactly once. Both files in the new test share a package, so mis-targeting shows up as a stranded buffer rather than as two unrelated servers. **3. The failure message hardcoded `lake serve`** after the latch became command-agnostic, telling a user whose `my-lean-wrapper` failed to go debug lake. `configured_command()` names what is actually configured, arguments included. **4. The ledger** now records all fifteen bites across the three rounds, both prior review rounds' findings (the round-2 block was lost when an earlier edit script aborted before writing), and the durable lesson. That lesson, recorded for the handoff: **six tests across three rounds were written, ran green, and pinned nothing** — caught only by biting. The shapes are enumerated in the ledger; the rule is that a test is not evidence until the mutation it targets has been shown to fail it. Two of the six are subtle enough to be worth naming here: a bite that RAISES is swallowed by the hook's pcall and "passes" for the wrong reason, and a fixture whose `serve` sleeps cannot reach any ordering where the primary comes up first. --- builtin/runtime/lean.lua | 66 +++++++++--- docs/active-work.md | 80 +++++++++++++-- tests/lean4_server_acceptance.rs | 171 +++++++++++++++++++++++++++++++ 3 files changed, 294 insertions(+), 23 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 5f74792..8f3b339 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -127,10 +127,28 @@ local probe = { proc = nil, -- process id of the running probe 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 + watching = nil, -- sid still being polled for die-before-initialize + primary = nil, -- sid the probe's verdict applies to; NOT cleared + -- when the server initializes, because a late + -- version verdict still has to retire it + armed = false, -- the target buffer + primary have been captured saw_initialized = false, } +-- The command as configured, for status text. Hardcoding "lake serve" +-- was untruthful the moment the failure latch became command-agnostic: +-- a user whose `my-lean-wrapper` failed was told `lake serve` did. +local function configured_command() + local cfg = pmacs.lsp.config.lean4 + local cmd = cfg and cfg.command + if not cmd then return "the Lean server" end + local args = cfg.args or {} + if #args > 0 then + return "`" .. tostring(cmd) .. " " .. table.concat(args, " ") .. "`" + end + return "`" .. tostring(cmd) .. "`" +end + local function report(msg) -- COHERENCE §1.2: background work must leave an attributed trace. -- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error` @@ -327,9 +345,19 @@ local function drain_probe() -- case, and covers it better. The probe answers only the ONE -- question failure detection would otherwise answer slowly: an -- old-but-working lake that starts a useless server. + -- **`probe.primary`, NOT `probe.watching`.** `watching` is + -- failure-polling state and is cleared the moment the server + -- initializes. A slow `--version` that lands after a successful + -- initialize would then arrive with nil, and `fire_latch(nil)` + -- retires nothing: `_attach_buffer` finds the still-live primary + -- attachment, early-returns it, and the retry calls that success. + -- Status and config would say "fell back" while the buffer stayed + -- on the old server — the same silent no-op as round 1, reached + -- through a different event ordering. Initializing must stop the + -- failure poll, not erase the server the verdict has to retire. if ev.kind == "exited" and ev.code == 0 and version_below_3_1(probe.out) then - fire_latch(probe.watching, "lake is older than 3.1.0") + fire_latch(probe.primary, "lake is older than 3.1.0") end end end @@ -393,18 +421,20 @@ local function poll_latch() if tostring(info.id) == skey then local kind = info.state and info.state.kind if kind == "initialized" then + -- Stop polling for failure; `probe.primary` deliberately + -- survives, because a later version verdict still needs it. probe.saw_initialized = true probe.watching = nil return end if kind == "crashed" or kind == "stopped" then - fire_latch(sid, "`lake serve` failed to start") + fire_latch(sid, configured_command() .. " failed to start") end return end end -- Gone from the manager entirely without ever initializing. - fire_latch(nil, "`lake serve` failed to start") + fire_latch(nil, configured_command() .. " failed to start") end -- Q#LN16 — `textDocument/waitForDiagnostics` -------------------------- @@ -488,11 +518,6 @@ 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) @@ -500,9 +525,18 @@ pmacs.hook.add("buffer.after-load", function() local rec = pmacs.lsp.active_attachment() if rec and rec.language == "lean4" then - -- Watch only the FIRST Lean server: the latch is per session. - if not probe.latched and not probe.saw_initialized - and probe.watching == nil then + -- **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 + -- latch still watched the FIRST buffer's server — so the rebuild + -- either repaired the wrong buffer or accepted the second buffer's + -- unrelated live server as success, stranding the first. The pair + -- (target buffer, primary server) is one fact and is captured as + -- one. + if not probe.armed and not probe.latched and not probe.saw_initialized then + probe.armed = true + probe.buf_key = tostring(buf) + probe.primary = rec.server probe.watching = rec.server end return @@ -522,7 +556,13 @@ pmacs.hook.add("buffer.after-load", function() -- 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(cfg.command) .. "` could not be started") + -- No server was ever created, so there is no primary to retire — + -- but the rebuild still needs a target buffer. + if not probe.armed then + probe.armed = true + probe.buf_key = tostring(buf) + end + fire_latch(nil, configured_command() .. " could not be started") end end) diff --git a/docs/active-work.md b/docs/active-work.md index 4a650da..6cdac4f 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` (25 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (28 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 @@ -279,12 +279,70 @@ If it does not, stop and repair the remote/fetch configuration. an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, not content). Discriminator is `read`'s SECOND return; decline only on a non-nil err. Probed on LuaJIT 2.1. -- Seven bites recorded, each against the committed tree: bare `io.open` - → 24a fails / 24b passes; require-non-nil → 24b fails / 24a passes; - no canonicalization → symlinked open spawns two servers; no re-attach - after the swap → three latch tests fail; hook keyed on the attachment - → the missing-`lake` case fails; `waitForDiagnostics` without - `version` → acc37 fails with the server's InvalidParams. +- **Fifteen bites recorded, each against the committed tree.** R1: bare + `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a + passes; no canonicalization → symlinked open spawns two servers; no + re-attach after the swap → three latch tests fail; hook keyed on the + attachment → the missing-`lake` case fails; `waitForDiagnostics` + without `version` → acc37 fails with InvalidParams. R2: skip retiring + a terminal server → `attempt` reaches 3; no originating-buffer gate → + the Lean buffer is left on the `lake` stub; retry-forever → the + failing-fallback test fails; version-probe any command → the + working-wrapper test fails; no disabled guard → the unconfigured test + sees "`nil` could not be started". R3: verdict keyed on `watching` → + the late-verdict test finds the buffer still on `lake`; `buf_key` + rewritten per load → the second-buffer test fails; hardcoded + `lake serve` → the wrapper-naming test fails. +- **Round-2 review: three more P1 lifecycle defects, suite 20/20 with + all of them live.** (1) The crashed primary respawned forever — + skipping the retire call avoided corrupting terminal servers but left + `next_restart_at` armed. **`forget` is the call for a TERMINAL server** + (it requires terminal state and removes the client, dropping the + restart timer); `stop` is for a live one and corrupts a terminal one. + (2) Re-attachment targeted whatever buffer was active when the async + verdict landed; an unrelated Rust attachment satisfied "a different + server id". (3) A failing fallback retried every tick forever, silent. + Plus two P2s: the Lake version parser was applied to arbitrary wrapper + output, and an UNCONFIGURED `config.lean4` was reported as failure and + latched, poisoning the session. +- **Round-3 review: two more P1s, both asynchronous correlation, suite + 25/25.** (a) `probe.watching` is cleared when the server initializes, + so a SLOW version verdict arrived with nil and retired nothing — + `_attach_buffer` returned the still-live primary and the retry called + it success, so status and config said "fell back" while the buffer + stayed put. **That is the round-1 silent no-op reached through a third + event ordering.** `probe.primary` is now separate from + `probe.watching` and survives initialization. (b) `buf_key` was + rewritten on every Lean `after-load`, so a second Lean buffer opened + before the verdict became the rebuild target while the latch still + watched the first buffer's server. Target buffer and primary server + are one fact and are now armed together, once. Plus a P2: the failure + message hardcoded `lake serve` after the latch became + command-agnostic, sending wrapper users to debug the wrong binary. +- **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 + 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 + ABSENCE of the fallback it claimed to test. + 2. "No live non-fallback server" misses a respawn loop: a respawning + server sits in `crashed` most of the time. `attempt` counts + respawns; liveness does not. + 3. Returning to a buffer via `find_or_open` re-fires + `buffer.after-load`, which repairs the attachment regardless of the + code under test. Use `switch_buffer`. + 4. A MISSING executable fails synchronously inside `after-load`, where + the rebuild happens inline — no async race can occur. Only the + probe path exercises asynchronous ordering. + 5. A mutation that RAISES (indexing a nil config) is swallowed by the + hook's pcall, so the bite "passes" for the wrong reason. A bite must + reproduce the original shape, not merely break the code. + 6. A fixture whose `serve` sleeps can never let the primary initialize + first, so it cannot reach the ordering where a late verdict must + retire a LIVE server. + Rule: **a test is not evidence until the mutation it targets has been + shown to fail it.** - **SUBSTRATE BUG FOUND, not fixed here (framing §6).** `LspManager::stop` on an ALREADY-terminal server takes its not-initialized branch, terminates the dead process and sets @@ -294,7 +352,9 @@ If it does not, stop and repair the remote/fetch configuration. `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so `attach_buffer` never rebuilds, and `forget` refuses it for not being terminal. **Stopping a dead server is what makes it un-replaceable.** - Lean works around it by checking the state before stopping. + Lean works around it by dispatching on state: `forget` when + terminal, `stop` when live. Merely SKIPPING the call is not + enough — that leaves `next_restart_at` armed. - Round-1 review found four P1s, all real: the latch swapped the config but never spawned or re-attached (and acc36 *asserted every server was terminal*, pinning the absence of the fallback); a missing `lake` @@ -308,9 +368,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 25/25; lean4 stage 1 9/9; dispatch seams 15/15; + lean4 server 28/28; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,214 across 94 suites, zero failures**; + workspace sweep 3,217 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 cba8792..db708f1 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -1069,3 +1069,174 @@ fn r2_an_unconfigured_lean_server_is_disabled_not_failed() { "and the session is not poisoned: a later config must still work" ); } + +// --------------------------------------------------------------------------- +// Round-3 review findings — asynchronous correlation. +// +// Both fail against 3377db0, where the suite was 25/25. +// --------------------------------------------------------------------------- + +impl Fixture { + /// A `lake` whose `serve` really works (it execs the fake LSP) but + /// whose `--version` answers slowly with an old version. This is the + /// ordering the previous fixtures could not produce: the primary + /// INITIALIZES before the version verdict arrives. + fn slow_version_lake(&self, rel: &str, server: &str, version_line: &str) -> PathBuf { + use std::os::unix::fs::PermissionsExt as _; + let path = self.root.join(rel); + std::fs::create_dir_all(path.parent().unwrap()).unwrap(); + std::fs::write( + &path, + format!( + "#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n sleep 0.6\n echo '{version_line}'\n exit 0\nfi\nexec '{server}'\n" + ), + ) + .unwrap(); + std::fs::set_permissions(&path, std::fs::Permissions::from_mode(0o755)).unwrap(); + path + } +} + +/// The command backing the active buffer's attached server. +fn attached_command(state: &EditorState) -> 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" + "#, + ) +} + +#[test] +fn r3_a_late_version_verdict_still_retires_an_initialized_primary() { + // `probe.watching` is cleared the moment the server initializes. A + // verdict arriving after that used to call `fire_latch(nil)`, which + // retires nothing — `_attach_buffer` then returns the still-live + // primary and the retry calls it success. Status and config would + // say "fell back" while the buffer stayed put. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let lake = fx.slow_version_lake("bin/lake", &fake_lsp_path(), "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &file); + // Let the primary initialize first — the ordering that matters. + tick_for(&mut state, 300); + assert_eq!( + attached_state(&state), + "initialized", + "precondition: the primary really did come up before the verdict" + ); + assert_eq!( + attached_command(&state), + lake.display().to_string(), + "precondition: and the buffer is on it" + ); + + // Now let the slow `--version` land and the fallback complete. + tick_for(&mut state, 1200); + + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "a late version verdict must actually move the buffer to the \ + fallback, not just rewrite the config and claim it did" + ); + // And the retired primary is not left running or respawning. + let stale: i64 = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + local live = rec and tostring(rec.server) or "" + local n = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) ~= live then + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then n = n + 1 end + end + end + return n + "#, + ); + assert_eq!(stale, 0, "the initialized primary was retired, not left up"); +} + +#[test] +fn r3_a_second_lean_buffer_does_not_steal_the_rebuild_target() { + // `buf_key` was written on every Lean `buffer.after-load`, so a + // second Lean file opened before the verdict became the rebuild + // target while the latch still watched the FIRST buffer's server. + // + // Both files live in the SAME Lake package, so they share one server + // and one root — which is what makes the mis-targeting observable as + // a stranded buffer rather than as two independent servers. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let first = fx.write("pkg/A.lean", "def a := 1\n"); + let second = fx.write("pkg/B.lean", "def b := 2\n"); + let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &first); + exec(&state, "_G.first_buf = pmacs.window.buffer()"); + // A second Lean buffer, opened before the probe's verdict lands. + open(&state, &second); + tick_for(&mut state, 500); + + // The armed target must still be the FIRST buffer. + let target_is_first: bool = eval( + &state, + "return pmacs.lean._probe.buf_key == tostring(_G.first_buf)", + ); + assert!( + target_is_first, + "the rebuild target is captured once, when the latch arms — a \ + later Lean buffer must not silently become the target" + ); + + // And the first buffer really does end up on the fallback. + exec(&state, "pmacs.window.switch_buffer(_G.first_buf)"); + tick_for(&mut state, 600); + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "the originating buffer is the one repaired" + ); +} + +#[test] +fn r3_a_failing_wrapper_is_named_truthfully_not_as_lake_serve() { + // The failure latch is command-agnostic, so its message must be too. + // Telling a user that `lake serve` failed when they configured + // `my-lean-wrapper` sends them to debug the wrong thing. + 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/my-lean-wrapper"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + + open(&state, &file); + settle(&mut state); + + let status = state.core.borrow().status.clone(); + assert!( + status.contains("my-lean-wrapper"), + "the status names the command the user actually configured; saw \ + {status:?}" + ); + assert!( + !status.contains("lake serve"), + "and does not attribute the failure to `lake serve`; saw {status:?}" + ); +} From 7c37bdc51455ba974a879340eabae700f1f1eb76 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 19:46:29 -0400 Subject: [PATCH 6/9] fix(lean): repair every buffer and retire every server on fallback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 4 review: one P1, and it is the same defect for the FOURTH time. `pmacs.lsp.config.lean4` is a single global entry, so swapping its command invalidates **every** Lean buffer and **every** Lean server — Q#LN15 gives one server per project root, so there can be several. Rounds 1-3 each repaired one buffer and retired one server, and round 3 shipped "repair the armed target, strand the rest": status and config said fallback while a second open Lean buffer stayed on the retired command, and a second project root's server stayed live. The shape that actually holds: * **Retire ALL `lean4` servers on latch**, not the one the probe happened to name. `probe.primary` identifies the server the VERDICT is about; it was never the set of servers the swap invalidates. * **Repair each buffer lazily and at most once**, when it becomes active — on `buffer.after-switch` and on the tick. `_attach_buffer` is an active-buffer-only seam, so a global swap cannot be applied to every open buffer at once; it has to be applied as they surface. lsp.lua's own `after-switch` re-pushes views but does not rebuild a stale attachment, so nothing else covered this. * The **once-per-buffer bound** is load-bearing: without it a fallback that also fails to spawn would retry every tick forever — the round-2 defect, which a naive global repair loop would reintroduce for every buffer instead of just one. * `shutting-down` is deliberately not treated as stale. It is still live by `server_is_live`'s reckoning, so attaching would early-return the stale record and burn that buffer's single attempt on a no-op. P2: argument-inclusive attribution was implemented in round 3 but pinned only by "contains the command name", so a mutation dropping every argument passed. Now asserted against the exact ` ` string. Also fixed a vacuous assertion this refactor created: a test checked `_probe.reattach_from == nil` for a field that no longer exists, which reads as nil and passes for nothing. It now asserts a positive count of recorded repair attempts. Three bites, each against 73587b0: repair only the armed buffer -> the second buffer stays on `lake`; retire only the named server -> one live stale server remains; drop arguments from attribution -> the exact-string assertion fails. The ledger records a second durable lesson beside the vacuity one: **a scope error repeats until the scope is named.** Four rounds of locally correct fixes, none of which asked what the config swap invalidates. When a change edits shared state, enumerate everything derived from it before repairing anything. --- builtin/runtime/lean.lua | 152 +++++++++++++++++++------------ docs/active-work.md | 33 ++++++- tests/lean4_server_acceptance.rs | 137 +++++++++++++++++++++++++++- 3 files changed, 257 insertions(+), 65 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 8f3b339..546e123 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -132,6 +132,7 @@ local probe = { -- when the server initializes, because a late -- version verdict still has to retire it armed = false, -- the target buffer + primary have been captured + repaired = {}, -- buffer key -> repair attempted (at most once) saw_initialized = false, } @@ -149,6 +150,16 @@ local function configured_command() return "`" .. tostring(cmd) .. "`" end +-- The fallback command, for status text. +local function fallback_name() + local args = M._fallback.args or {} + if #args > 0 then + return "`" .. tostring(M._fallback.command) .. " " + .. table.concat(args, " ") .. "`" + end + return "`" .. tostring(M._fallback.command) .. "`" +end + local function report(msg) -- COHERENCE §1.2: background work must leave an attributed trace. -- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error` @@ -232,8 +243,6 @@ end -- 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:** -- @@ -263,67 +272,85 @@ local function retire_server(sid) end end +-- Retire EVERY Lean server, not just the one that failed. +-- +-- `pmacs.lsp.config.lean4` is a single global entry, so swapping its +-- command invalidates every server spawned from the old one — and +-- Q#LN15 gives one server per project root, so there can be several. +-- 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() + 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 + end + for _, id in ipairs(ids) do retire_server(id) end +end + +-- Rebuild the ACTIVE buffer's attachment if it is Lean and stale. +-- +-- `_attach_buffer` is an active-buffer-only seam, so a global config +-- swap cannot be applied to every open buffer at once. It is applied +-- lazily instead: whenever a Lean buffer becomes the active one, if its +-- record points at a server that is gone or terminal, it is rebuilt. +-- +-- **At most one attempt per buffer.** Without that bound a fallback +-- that also fails to spawn would retry every tick forever with nothing +-- reported — the round-2 defect, which a general repair loop would +-- otherwise reintroduce for every buffer instead of just one. +-- +-- A `shutting-down` server is deliberately NOT treated as stale: it is +-- still live by `server_is_live`'s reckoning, so `attach_buffer` would +-- early-return the stale record and burn this buffer's single attempt +-- 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 + local buf = pmacs.window.buffer() + if not buf then return end + local key = tostring(buf) + if probe.repaired[key] then return end + local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf) + if not ok_lang or lang ~= "lean4" then return end + + local rec = pmacs.lsp.active_attachment() + local stale + if not rec then + stale = true + else + local kind = server_state_kind(rec.server) + stale = (kind == nil or kind == "crashed" or kind == "stopped") + end + if not stale then return end + + probe.repaired[key] = true + 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") + end +end + local function fire_latch(sid, why) if probe.latched then return end probe.latched = true probe.watching = nil - if sid then retire_server(sid) end 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_all_lean_servers() return end - report("LSP: lean4 " .. why .. "; falling back to `" - .. 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. - -- - -- 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 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 - -- (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 + retire_all_lean_servers() + 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`). + repair_active_if_stale() end local function drain_probe() @@ -566,19 +593,26 @@ pmacs.hook.add("buffer.after-load", function() end end) +-- A buffer switch is the moment a stale Lean buffer becomes visible, so +-- repair immediately rather than waiting for the next tick. lsp.lua's +-- own `after-switch` subscription re-pushes views but does NOT rebuild a +-- stale attachment, so nothing else covers this. +pmacs.hook.add("buffer.after-switch", function() + repair_active_if_stale() +end) + pmacs.hook.add("process.after-tick", function() drain_probe() poll_latch() - -- Keep trying until the stopped server is really gone; see the note in - -- `fire_latch`. - if probe.reattach_from ~= nil then try_reattach() end + -- 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() end) -- Test seam: acceptance drives the latch deterministically rather than -- waiting on real process timing. Not part of the public surface. M._probe = probe M._fire_latch = fire_latch -M._try_reattach = try_reattach M._version_below_3_1 = version_below_3_1 pmacs.lean = M diff --git a/docs/active-work.md b/docs/active-work.md index 6cdac4f..e4e1064 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` (28 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (31 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 @@ -319,6 +319,21 @@ If it does not, stop and repair the remote/fetch configuration. are one fact and are now armed together, once. Plus a P2: the failure message hardcoded `lake serve` after the latch became command-agnostic, sending wrapper users to debug the wrong binary. +- **Round-4 review: one P1, and it is the same defect a FOURTH time.** + `pmacs.lsp.config.lean4` is a single global entry, so swapping its + command invalidates **every** Lean buffer and **every** Lean server — + Q#LN15 gives one per project root. Rounds 1–3 each fixed the repair + for one buffer and one server; round 4 is "repair the armed target, + strand the rest". The shape that finally holds: retire ALL `lean4` + servers on latch, and repair each buffer **lazily and at most once** + when it becomes active (`buffer.after-switch` + the tick), because + `_attach_buffer` is active-buffer-only and cannot reach the others. + The per-buffer once-only bound is what stops a failing fallback + retrying forever — the round-2 defect a naive global repair loop would + have reintroduced for every buffer instead of one. Plus a P2: the + argument-inclusive attribution was implemented but pinned only by + "contains the command name", so a mutation dropping every argument + still passed. - **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 @@ -341,8 +356,20 @@ If it does not, stop and repair the remote/fetch configuration. 6. A fixture whose `serve` sleeps can never let the primary initialize first, so it cannot reach the ordering where a late verdict must retire a LIVE server. + 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. 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 + named.** The "fallback silently does not happen" defect came back four + times: no re-attach; re-attach cleared by an unrelated buffer; + re-attach satisfied by the server being replaced; re-attach of one + buffer while the others stay stale. Every fix was locally correct and + none asked *what does this config swap invalidate?* — the answer being + every Lean buffer and every Lean server, because the config entry is + global and servers are per-root. **When a change edits shared state, + enumerate everything derived from it before repairing anything.** - **SUBSTRATE BUG FOUND, not fixed here (framing §6).** `LspManager::stop` on an ALREADY-terminal server takes its not-initialized branch, terminates the dead process and sets @@ -368,9 +395,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 28/28; lean4 stage 1 9/9; dispatch seams 15/15; + lean4 server 31/31; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,217 across 94 suites, zero failures**; + workspace sweep 3,220 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 db708f1..32cdf3e 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -1010,9 +1010,19 @@ fn r2_a_failing_fallback_is_reported_once_and_does_not_retry_forever() { "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"); + // And the repair was ATTEMPTED and recorded, so it is bounded rather + // than spinning. Asserting on a field that no longer exists would + // read as nil and pass for nothing — the vacuity shape this branch + // keeps producing, so the assertion is on a positive count. + let attempted: i64 = eval( + &state, + "local n = 0 for _ in pairs(pmacs.lean._probe.repaired) do n = n + 1 end return n", + ); + assert_eq!( + attempted, 1, + "exactly one repair attempt was made and recorded, so a failing \ + fallback cannot retry every tick forever" + ); } #[test] @@ -1240,3 +1250,124 @@ fn r3_a_failing_wrapper_is_named_truthfully_not_as_lake_serve() { "and does not attribute the failure to `lake serve`; saw {status:?}" ); } + +// --------------------------------------------------------------------------- +// Round-4 review — the config swap is GLOBAL, so one repaired buffer is +// not a fallback. Both fail against 73587b0. +// --------------------------------------------------------------------------- + +#[test] +fn r4_every_open_lean_buffer_is_repaired_not_just_the_armed_one() { + // `pmacs.lsp.config.lean4` is a single entry; swapping its command + // invalidates every buffer attached to the old one. Round 3 repaired + // exactly `probe.buf_key` and cleared the retry, leaving every other + // open Lean buffer on the retired server while status and config + // both said "fell back". + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let first = fx.write("pkg/A.lean", "def a := 1\n"); + let second = fx.write("pkg/B.lean", "def b := 2\n"); + let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &first); + exec(&state, "_G.first_buf = pmacs.window.buffer()"); + open(&state, &second); + exec(&state, "_G.second_buf = pmacs.window.buffer()"); + tick_for(&mut state, 700); + + // The armed (first) buffer. + exec(&state, "pmacs.window.switch_buffer(_G.first_buf)"); + tick_for(&mut state, 500); + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "the armed buffer is repaired" + ); + + // And the OTHER one, which round 3 stranded. + exec(&state, "pmacs.window.switch_buffer(_G.second_buf)"); + tick_for(&mut state, 500); + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "every open Lean buffer ends up on the fallback — repairing only \ + the armed target leaves this one on the retired server" + ); +} + +#[test] +fn r4_a_second_project_roots_server_is_also_retired() { + // Q#LN15 gives one server per project root, so a swap can invalidate + // several. `probe.primary` names only the first; retiring only that + // leaves the second root's server live on a command the config no + // longer names. + let fx = Fixture::new(); + fx.toolchain("one", "v4.9.0\n"); + fx.toolchain("two", "v4.9.0\n"); + let a = fx.write("one/A.lean", "def a := 1\n"); + let b = fx.write("two/B.lean", "def b := 2\n"); + let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &a); + open(&state, &b); + // Two roots, two servers, before any verdict lands. + let before: i64 = eval(&state, "return #pmacs.lsp.list()"); + assert_eq!(before, 2, "precondition: one server per root"); + + tick_for(&mut state, 900); + + // No server may still be running the retired command. + let stale_live: i64 = eval( + &state, + &format!( + r#" + local n = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.command) == "{}" then + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then n = n + 1 end + end + end + return n + "#, + lua_str(&lake) + ), + ); + assert_eq!( + stale_live, 0, + "every Lean server spawned from the old command is retired, not \ + just the one the probe happened to name" + ); +} + +#[test] +fn r4_attribution_names_the_exact_command_and_its_arguments() { + // Round 3 implemented argument-inclusive attribution but pinned only + // "contains my-lean-wrapper" and "does not contain lake serve" — a + // mutation dropping every argument still passed. + 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/my-lean-wrapper"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + exec( + &state, + "pmacs.lsp.config.lean4.args = { \"serve\", \"--quiet\" }", + ); + + open(&state, &file); + settle(&mut state); + + let status = state.core.borrow().status.clone(); + let expected = format!("`{} serve --quiet`", absent.display()); + assert!( + status.contains(&expected), + "the status names the exact configured command AND its arguments;\n \ + want substring: {expected}\n saw: {status:?}" + ); +} From 19f48d46c0eed0ef1ddf17de1bc180b22420372e Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 21:28:11 -0400 Subject: [PATCH 7/9] fix(lsp,lean): bound the fallback's own failure; heal at point of use MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- builtin/runtime/lean.lua | 66 +++++++- builtin/runtime/lsp.lua | 26 +++ docs/active-work.md | 36 +++- tests/lean4_server_acceptance.rs | 271 +++++++++++++++++++++++++++++++ 4 files changed, 391 insertions(+), 8 deletions(-) diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 546e123..6490296 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -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-`, 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 diff --git a/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua index 0749cfa..6081a3d 100644 --- a/builtin/runtime/lsp.lua +++ b/builtin/runtime/lsp.lua @@ -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 diff --git a/docs/active-work.md b/docs/active-work.md index e4e1064..6b99985 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` (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 diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index 32cdf3e..e28ac8f 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -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:?}" + ); +} From 786de69d3827d37a648b5d378b388837161f662c Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 22:32:48 -0400 Subject: [PATCH 8/9] 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. --- builtin/runtime/lean.lua | 180 +++++++++++++++------- builtin/runtime/lsp.lua | 64 ++++++-- docs/active-work.md | 37 ++++- tests/lean4_server_acceptance.rs | 248 ++++++++++++++++++++++++++++++- 4 files changed, 455 insertions(+), 74 deletions(-) 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" + ); +} From dec51960da5967c4da9477cbe8a5e10059487481 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 22:36:02 -0400 Subject: [PATCH 9/9] docs: record round-six bite evidence Capture the concrete counterfactual outcomes for all five review fixes against 19f48d4. --- docs/active-work.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/active-work.md b/docs/active-work.md index b96cc42..2efce61 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -378,7 +378,10 @@ If it does not, stop and repair the remote/fetch configuration. 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`. + `default-lean4`. All five bites against `19f48d4` discriminate: the + old files produce 2 same-root servers, a fallback attempt of 4, a + shipped command still targeting `stopped`, retirement of the healthy + root, and retirement of the colliding user server, respectively. - **DURABLE LESSON — "the test that passes" vs "the test that discriminates."** Green tests across six rounds repeatedly pinned only a nearby helper or an absence, and only biting exposed it. **Carry this