diff --git a/builtin/runtime/fs.lua b/builtin/runtime/fs.lua index 49c006e..39e3baa 100644 --- a/builtin/runtime/fs.lua +++ b/builtin/runtime/fs.lua @@ -325,4 +325,28 @@ function fs.watch(path, callback, opts) return watch end +-- pmacs.fs.canonicalize(path) -> string | nil +-- +-- Arc 8 Stage 3a (framing Q#LN20). The **only synchronous** function on +-- this module, and deliberately so: its consumer is a function-valued +-- `pmacs.lsp.config[lang].root`, invoked from `ensure_server` <- +-- `attach_buffer` <- the `buffer.after-load` hook, where there is no +-- coroutine and therefore nothing to `:await()` on. Every other +-- primitive here returns a Handle; this one cannot, or it would be +-- unusable at the one call site that needs it — the same trap +-- `pmacs.fs.stat` falls into for that caller. +-- +-- Resolves symlinks and `.` / `..`, returning an absolute path, or nil +-- if the path does not exist or cannot be resolved. Nil is a normal +-- answer, not an error: callers routinely ask about paths that may have +-- been deleted. +-- +-- Why it exists: a configured LSP root reaches `file_uri_for` verbatim +-- and that URI is the server-affinity key (PR #161), so one project +-- opened through a symlink and through its real path would otherwise +-- spawn two servers. `pmacs.editor.file_path()` collapses `.` and `..` +-- lexically but leaves symlinks intact, so the resolver cannot get a +-- canonical path any other way. +fs.canonicalize = pmacs._fs.canonicalize + pmacs.fs = fs diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua new file mode 100644 index 0000000..09ad280 --- /dev/null +++ b/builtin/runtime/lean.lua @@ -0,0 +1,750 @@ +-- 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 + out = "", -- accumulated probe stdout + buf_key = nil, -- tostring() of the buffer that started this + 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 + 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_watches = {}, -- sid key -> sid, each polled die-before-init + fallback_done = {}, -- sid key -> initialized or terminally handled + 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 + +-- 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` + -- 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. +-- 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 + if tostring(info.id) == skey then + return info.state and info.state.kind + end + end + 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 + major, minor = tonumber(major), tonumber(minor) + if major < 3 then return true end + return major == 3 and minor < 1 +end + +-- 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` +-- from `init.lua` at exactly the moment they are least likely to notice. +-- +-- 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 + -- 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 + +-- Retire the failed server, swap the command, then rebuild the +-- attachment on the buffer that started this. +-- 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 + +-- 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. +-- 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 is_derived_server(info.id) then ids[#ids + 1] = info.id end + 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. +-- +-- `_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() + -- **`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) + 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 + 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. 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 + +-- 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 + + 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 + +local function fire_latch(sid, why) + if probe.latched then return end + probe.latched = true + probe.watching = nil + if not swap_to_fallback() then + report("LSP: lean4 " .. why) + -- 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() + 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`). + repair_active_if_stale() +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.out = probe.out .. 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. + -- **`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.primary, "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 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 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 + -- wondering why their editor touched `lake` finds an owner here. + label = "lean:lake-version-probe", + command = cfg.command, + 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 + -- 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, configured_command() .. " failed to start") + end + return + end + end + -- Gone from the manager entirely without ever initializing. + fire_latch(nil, configured_command() .. " 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. +-- +-- **`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, version, fn) + local ok, rid = pcall(pmacs.lsp.send_request, sid, + "textDocument/waitForDiagnostics", { uri = uri, version = version }) + 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 + +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._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…") + 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, +} + +-- `$/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. +-- +-- **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 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 + + 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 + -- 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 + end + + -- **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 + 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, + -- 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 + -- 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) + +-- 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() + -- 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_fallbacks() +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/builtin/runtime/lsp.lua b/builtin/runtime/lsp.lua index 6021134..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. @@ -871,6 +903,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 @@ -881,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* @@ -893,6 +948,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 @@ -924,6 +997,19 @@ 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 + -- 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) return rec end @@ -1546,6 +1632,186 @@ end -- itself is unaffected. Server ids are snapshotted before the loop -- because `apply_workspace_edit` → `find_or_open` can attach a new -- buffer mid-iteration (mutating `attachments`). +-- Server-originated notification / response seams (framing Q#LN9) ------- +-- +-- Before this, `handle_server_requests` handled five `request` methods +-- and `initialized`, and dropped every `notification` and `response` on +-- the floor. Dropping responses made `pmacs.lsp.send_request` a +-- write-only API from Lua: the reply was drained and discarded, so +-- nothing outside Rust's typed stores could ever consume one. +-- +-- Both seams route through the *existing* drain. A second +-- `events_take` caller would steal events from this one — `take_events` +-- removes the queue — so any new consumer must extend this loop rather +-- than open its own. +-- +-- method -> array of subscriber fns. Persistent; `pmacs.hook` has no +-- `remove` and neither does this, deliberately matching it. +local notification_subs = {} +-- tostring(sid) -> { [request_id] = { fn = fn, attempt = n } }. One-shot. +local pending_responses = {} + +local function report_subscriber_error(what, err) + local msg = string.format("LSP: %s subscriber failed: %s", what, + tostring(err)) + -- COHERENCE §1.2: a pcall around background wiring must report, not + -- discard. `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 + +-- Current spawn attempt for `sid`, or nil if the manager has forgotten +-- it. A restart reuses the sid but bumps the attempt, which is how a +-- pending one-shot tells "my server is still here" from "my server died +-- and a new generation took its id". +local function server_attempt(sid) + local skey = tostring(sid) + for _, info in ipairs(pmacs.lsp.list()) do + if tostring(info.id) == skey then + return info.attempt or 0 + end + end + return nil +end + +-- fn(sid, params); persistent, fires for every server. +function pmacs.lsp.on_notification(method, fn) + if type(method) ~= "string" or type(fn) ~= "function" then + error("pmacs.lsp.on_notification(method, fn): want string, function") + end + local subs = notification_subs[method] + if not subs then + subs = {} + notification_subs[method] = subs + end + subs[#subs + 1] = fn +end + +-- fn(result, err); ONE-SHOT, keyed to the exact request. +-- `request_id` is what `pmacs.lsp.send_request` returned. +-- +-- **Register only against a server with an attached buffer.** The drain +-- that delivers replies visits only sids present in `attachments`, so a +-- one-shot on an unattached server will not fire on its reply — the +-- reply sits in that server's queue and the handler is invoked only when +-- the purge below decides the server is gone. That is fire-on-death, not +-- fire-on-reply, and it looks exactly like a hung request while +-- debugging. The attach path is the ordinary way to get a sid; a +-- hand-spawned one from `init.lua` is the case to watch. +function pmacs.lsp.on_response(sid, request_id, fn) + if not sid or type(request_id) ~= "number" or type(fn) ~= "function" then + error("pmacs.lsp.on_response(sid, request_id, fn): want sid, number, function") + end + local skey = tostring(sid) + local pend = pending_responses[skey] + if not pend then + pend = {} + pending_responses[skey] = pend + end + -- The attempt is captured at registration so a restart under the same + -- sid purges this entry rather than leaving it waiting on a reply the + -- dead generation was going to send. + pend[request_id] = { fn = fn, attempt = server_attempt(sid) or 0 } +end + +local function dispatch_notification(sid, ev) + local subs = notification_subs[ev.method] + if not subs then return end + -- Length captured up front: a subscriber that registers another one + -- must not be able to extend the list being walked. + local n = #subs + for i = 1, n do + local ok, err = pcall(subs[i], sid, ev.params) + if not ok then + report_subscriber_error("notification " .. tostring(ev.method), err) + end + end +end + +local function deliver_response(sid, ev) + local skey = tostring(sid) + local pend = pending_responses[skey] + if not pend then return end + local entry = pend[ev.request_id] + if not entry then return end + -- Removed UNCONDITIONALLY, so a handler that raises is still retired + -- and cannot be invoked a second time by the purge. Removing first is + -- the defensive order and costs nothing, but it is not what defends + -- against re-invocation: `pcall` catches the raise either way, so + -- before-vs-after is unobservable without a re-entrant drain. The + -- reachable bug is gating removal on a clean return, which acceptance + -- 32 bites (2 != 1). + pend[ev.request_id] = nil + if next(pend) == nil then pending_responses[skey] = nil end + local ok, err = pcall(entry.fn, ev.result, ev.error) + if not ok then + report_subscriber_error("response " .. tostring(ev.method), err) + end +end + +-- Settle every one-shot whose server can no longer answer it. +-- +-- Deliberately driven off `pmacs.lsp.list()` and NOT off a death event +-- observed in the drain, because the drain cannot be relied on to reach +-- the server in question: `handle_server_requests` builds its sid list +-- from `attachments`, and a sid leaves that table whenever +-- `attach_buffer` finds it dead and rebuilds the attachment against a +-- fresh server. So the very event that should trigger the purge — +-- `crashed` / `stopped` — is the one most likely to go undrained. A +-- one-shot settled only by the drain would leak exactly when it matters. +-- +-- `pmacs.lsp.list()` enumerates the manager directly and is unaffected +-- by attachment bookkeeping, which is what makes it the right authority. +local function purge_dead_pending() + if next(pending_responses) == nil then return end + local ok, rows = pcall(pmacs.lsp.list) + -- A failed enumeration is not evidence that every server died; leaving + -- the registrations alone is the safe read of "we don't know". + if not ok or not rows then return end + local alive = {} + for _, info in ipairs(rows) do + local kind = info.state and info.state.kind + if kind ~= "crashed" and kind ~= "stopped" then + alive[tostring(info.id)] = info.attempt or 0 + end + end + for skey, pend in pairs(pending_responses) do + local attempt = alive[skey] + local dead = {} + for rid, entry in pairs(pend) do + -- Absent or terminal, or the same sid running a NEW generation: + -- in every case the request this entry awaits is unanswerable. + -- + -- The generation half is **defensive and not covered by the + -- acceptance suite**, stated plainly rather than left to look + -- tested. Reaching it requires a crash and its restart to both + -- fall inside a gap with no `_async.tick` — the crash backoff is + -- 500ms (`src/lsp.rs:1007`), so any tick during that window sees + -- `crashed` and the absent-or-terminal test above fires first. A + -- stalled or idle editor can produce such a gap, and then this is + -- the only thing standing between a one-shot and waiting forever + -- on a reply the dead generation owed. Every attempt to stage it + -- deterministically ended up exercising the `crashed` path + -- instead, so it is kept as insurance and labelled as such. + if attempt == nil or attempt ~= entry.attempt then + dead[#dead + 1] = rid + end + end + for _, rid in ipairs(dead) do + local entry = pend[rid] + pend[rid] = nil + local ok_h, err = pcall(entry.fn, nil, + { message = "server gone before response" }) + if not ok_h then + report_subscriber_error("response purge", err) + end + end + if next(pend) == nil then pending_responses[skey] = nil end + end +end + local function handle_server_requests() local sids, seen = {}, {} for _, rec in pairs(attachments) do @@ -1598,6 +1864,10 @@ local function handle_server_requests() -- LSP spells the field "unregisterations". pcall(unregister_file_watchers, sid, ev.params and ev.params.unregisterations) + elseif ev.kind == "notification" then + dispatch_notification(sid, ev) + elseif ev.kind == "response" then + deliver_response(sid, ev) elseif ev.kind == "initialized" then -- Buffers attach before the server finishes initializing, so -- the pulls in `attach_buffer` are no-ops for the FIRST file @@ -1620,6 +1890,10 @@ if pmacs._async and pmacs._async.tick then pmacs._async.tick = function(...) local ret = _prior_async_tick(...) pcall(handle_server_requests) + -- After the drain, so a response delivered this tick settles its + -- one-shot normally rather than being purged as "server gone" in the + -- same pass when the server died right after answering. + pcall(purge_dead_pending) pcall(flush_due_did_changes) return ret end diff --git a/docs/active-work.md b/docs/active-work.md index 9ba9efa..362dd1c 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -55,7 +55,7 @@ git status --short --branch The `git log` command must expose `d152120` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #161) +## 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` @@ -189,6 +189,280 @@ If it does not, stop and repair the remote/fetch configuration. suites**; `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` and `-- --skip basedpyright`. +### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`) + +- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @ + `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first + two commits, then the implementation, then a bite-driven correction. +- **Stage 2 merged as #161** (`main` @ `46a1b8f`, 2026-07-25, two review + rounds). COHERENCE.md §7 records the slice; §1.2 records the dead + `pmacs.error` channel found landing it. +- **Framing rev 5 splits Stage 3 into 3a and 3b** because rev 4 broke its + own §4 rule — the row read "two `lsp.lua` generalizations" under prose + claiming Stage 3 was Lean-only. One generalization shipped as Stage 2; + the other (Q#LN9's seams) is the shared event drain, so it is now its + own substrate stage. 3a and 3b are **strictly sequential** — 3b's + subscriber is written against 3a's seam and both touch `lsp.lua`. +- Ships: `pmacs.lsp.on_notification` / `on_response`, two arms in + `handle_server_requests`, a pending-response purge, and + `pmacs.fs.canonicalize` (Q#LN20). No protocol change, no Lean content. +- **Two framing claims were corrected during implementation**, both + recorded in §0.1 finding 6 and in the round-2 commit: + 1. The reachable leak is **not** a killed buffer. The Rust core fires + exactly five hooks (`buffer.after-edit`, `buffer.after-load`, + `buffer.after-switch`, `frontend.detached`, `process.after-tick`) — + **there is no buffer-kill hook**, so nothing tears an attachment + down and the drain keeps reaching that server. The real path is + `attach_buffer` dropping a dead sid from `attachments` and + rebuilding against a fresh server, which makes `crashed`/`stopped` + the event *least* likely to be drained. Hence the purge polls + `pmacs.lsp.list()` rather than riding the drain. + 2. Acceptance 32 does **not** pin "removed before invocation" — + `pcall` catches the raise either way, so before/after is + unobservable without a re-entrant drain. It pins removal being + **unconditional**; renamed accordingly. +- **`pmacs._fs` is installed from `install_async`, not `install_project`**, + purely for load order: `make_workspace` runs *after* `fs.lua` is + evaluated, so a canonicalizer placed there reads nil. This cost one + failing run to discover and is the kind of thing to check first. +- Bites recorded (all against the committed tree): removal gated on a + clean return → acc32 fails 2 != 1; an event-driven purge → the + no-attachment case fails "never called" while the attached case still + passes; a resolver without `canonicalize` → two servers (34b's own + falsification, which ships as a test). +- **Known unpinned:** the purge's generation (`attempt`) check. Reaching + it needs a crash *and* its restart to fall in a gap with no + `_async.tick`; the backoff is 500ms, so any tick sees `crashed` first + and the absent-or-terminal arm fires. Labelled as defensive in the + code rather than left looking covered. +- Verification on this branch: `cargo fmt --check` clean; strict + workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; + dispatch seams 15/15 on Linux (14 on macOS — see below); multi-root + 13/13; M4 121; required GPU 155; **isolated-config workspace sweep + 3,189 across 93 suites, zero failures**; `git diff --check` clean. +- **Two flakes/portability facts from CI round 1, both worth keeping:** + 1. `composition_overhead_under_ten_percent` tripped once in a local + sweep at 18.8% against a 10% budget, then passed 3/3 in isolation + here, passed in isolation on main, and passed a full sweep rerun. + The tell is in its own output: the same run reported realistic-frame + overhead as **-4.6%**, and a negative figure is measurement noise, + not added work. Load-sensitive under a parallel `--workspace` run. + 2. **A non-UTF-8 filename fixture cannot be built on macOS.** APFS + enforces valid UTF-8, so `std::fs::write` fails with EILSEQ + ("Illegal byte sequence") before the code under test is reached. + `#[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. + **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`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`, + a `leanprogress` mode plus `waitForDiagnostics` validation on + `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 + 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. +- **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. +- **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. +- **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**. +- **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`. 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 + 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. + 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. + 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 + 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 + `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 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` + 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 + server-failure latch covers the rest. +- Verification on this branch: `cargo fmt --check` clean; strict + 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 + 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 + describes the pushed tree; recording it late is the #161 fmt-blocker + error in a slower form.) + ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) - Approved framing: `docs/dired-framing.md` **revision 6** — rev 5 is the diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index e1fe060..ec62980 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -6,8 +6,9 @@ pmacs has no Lean support of any kind: `grep -rin lean` over `*.rs`, plain buffer — no grammar, no major mode, no comment syntax, no pair set, no server. -This lane closes that in seven stages. Stage boundaries are drawn where +This lane closes that in eight stages. Stage boundaries are drawn where the *substrate* changes, not where the feature list does — see §4. +§9 states the lane's coherence impact per `COHERENCE.md` §20. ## 0. Why this lane, why now @@ -24,7 +25,7 @@ the *substrate* changes, not where the feature list does — see §4. first consumer of a non-standard LSP method family. Stage 6 adds a severity-routing policy to `LspServerSpec`. - The user's stated north star is **matching or exceeding what VS Code - does with Lean**. §5's bet 6 scores honestly how close seven stages get + does with Lean**. §5's bet 6 scores honestly how close the eight stages get and names precisely what is still missing. Parallel-safety: Stage 1 touches `Cargo.toml`, `src/syntax.rs`, @@ -34,10 +35,13 @@ Stage 3 (the other open lane) touches `pmacs-gpu/*` and `src/semantic_render.rs`. None of the three footprints overlap; the only file Stage 1 shares with anything is `Cargo.toml`, at one line. -Stages 1 and 2 are independent of each other and **can** run as sibling -worktrees — they share no file. Per the #126/#127 lesson, that split is -recorded here, before either starts, rather than discovered during a -rebase. +Stages 1 and 2 were independent of each other and could have run as +sibling worktrees — they shared no file. Both have since landed (#160, +#161). **Stages 3a and 3b are not independent**: 3b's subscriber is +written against the seam 3a adds, and both touch +`builtin/runtime/lsp.lua`. They are strictly sequential — recorded here, +per the #126/#127 lesson, before either starts rather than discovered +during a rebase. ## 0.1 Revision history @@ -81,7 +85,7 @@ round 2 renumbered the stages, so a rev-1 "Stage 4" is now Stage 5.)* 5. **Q#LN8's resolver must honor the search boundary.** A Lua `lean-toolchain` walk that ignores `pmacs.project.search_boundary()` breaks the contract `detect_project_within` exists to enforce and makes - the Stage 3 outermost-root test non-hermetic. + the Stage 3b outermost-root test non-hermetic. ### Round 2 (rev 2 → rev 3) — scope expansion @@ -168,11 +172,121 @@ Six findings against the round-2 expansion. All revision edits. preserving user-supplied `env`/`settings`/`init_options`/`root`. 6. Wording: `\{}` expands to `{$CURSOR}`; `⦃⦄` comes from `\{{}}`. +### Round 4 (rev 4 → rev 5) — Stage 3 re-scout and split + +Stages 1 and 2 landed (#160, #161). Re-scouting Stage 3 against `main` +@ `46a1b8f` — six merged PRs past the rev-4 snapshot (#159–#164) — +produced three findings that change the plan and four that confirm it. +Every fact below was verified in a worktree at that commit; the two +marked *probed* were established by running Lua in a fresh +`EditorState`, not by grep. + +1. **Stage 3 violated this document's own splitting rule.** §4 says "no + PR in this arc mixes a cross-cutting substrate change with Lean + feature content" and "a reviewer looking at Stage 3 sees only Lean" — + while §4's own risk column for Stage 3 read *"two `lsp.lua` + generalizations."* Those cannot both be true. One of the two landed + as Stage 2; the other is Q#LN9's dispatch seams, which modify + `handle_server_requests` — confirmed the **only** production drain of + LSP events (`LspManager::take_all_events` has no non-test caller). By + the same test that justified splitting Stage 2 out, that is + cross-cutting substrate. **Stage 3 is now 3a (substrate, no Lean) and + 3b (Lean).** +2. **The Lean resolver could not satisfy the contract Stage 2 + documented.** #161 established that a configured root — string or + resolver return — must be a canonical absolute path, because it + reaches `file_uri_for` verbatim and that URI is the affinity key. + *Probed:* `pmacs.editor.file_path()` is **not** canonical. Opening + `/linkpkg/sub/./../sub/a.lean`, where `linkpkg` symlinks to + `pkg`, yields `/linkpkg/sub/a.lean` — lexical `.`/`..` collapse + only, symlinks unresolved. No canonicalize binding is exposed to Lua, + and `pmacs.project.detect` canonicalizes but returns nil without a + marker. So a Lean resolver walking up from the buffer's path returns + a non-canonical root, and one package opened by two spellings spawns + two `lake serve` processes — reintroducing precisely the bug Stage 2 + exists to prevent. New Q#LN20 adds `pmacs.fs.canonicalize`; it rides + 3a because it is substrate, and it retires the footgun for every + future function-valued root rather than only Lean's. +3. **`pmacs.fs.stat` is unusable in the resolver.** It is asynchronous — + `fs.lua:93` returns an awaitable handle — and the resolver runs + synchronously inside `ensure_server` ← `attach_buffer` ← the + `buffer.after-load` hook, where there is no coroutine to await on. + *Probed:* the `io` and `os` stdlib **are** exposed in the sandbox + (`type(io.open) == "function"`; `terminal.lua` already uses + `os.getenv`), and `io.open` returns nil for a missing path. So the + marker walk is implementable, but through the Lua stdlib rather than + the pmacs fs API — the opposite of what a reader would assume. + Q#LN8 now says so, with the one edge that matters: `io.open` + **succeeds on a directory**, so a bare existence check would accept + a `lean-toolchain` *directory* as a marker. + +Confirmations, recorded because each was load-bearing and unverified: + +4. **Q#LN7's "stop the failing server first" is necessary, not + defensive.** The spec default is `LspRestartPolicy::OnCrash`, and the + termination handler calls `should_restart(policy)` + (`matches!(OnCrash | Always)`) — which, unlike the + `termination_warrants_restart` helper beside it, never consults the + exit code. `maybe_restart` re-fires on every elapsed backoff with **no + attempt ceiling**, so a broken `lake` respawns forever. `stop()` sets + `restart = Never` (`src/lsp.rs:1349`), which is exactly what disarms + it. Acceptance 36 pins a real mechanism. +5. **The response seam works as designed.** `Response` events are pushed + unconditionally (`src/lsp.rs:2652`) — the typed-store absorb above + does not consume them — and reach Lua as `{kind = "response", + request_id = , method, result, error}`, with + `pmacs.lsp.send_request` returning that same numeric id. So + `on_response(sid, request_id, fn)` is keyable as specified. +6. **The seams' contract is narrower than rev 4 implied, and the + narrowing is load-bearing.** `handle_server_requests` builds its sid + list from `attachments`, and `push_event` appends with no cap. So a + subscriber fires only for a server with a live attachment, and an + unattached server's event queue grows unboundedly. + + *Corrected during implementation (rev 5, round 2).* Rev 5 first + claimed the reachable leak was a killed buffer. **That was wrong.** + The Rust core fires exactly five hooks — `buffer.after-edit`, + `buffer.after-load`, `buffer.after-switch`, `frontend.detached`, + `process.after-tick` — and **there is no buffer-kill hook at all**, + so `lsp.lua` never tears an attachment down and the drain keeps + reaching that server. The premise was right and the inference was + not: it needed attachments to be removed on kill, and nothing + removes them. + + The reachable leak is a different path with the same root cause. + `attach_buffer` drops a sid from `attachments` the moment + `server_is_live` reports false, rebuilding against a fresh server — + so the `crashed` / `stopped` event that should trigger a purge is + **precisely the one most likely to go undrained**. An event-driven + purge leaks exactly when it matters. Q#LN9 therefore drives the + purge off `pmacs.lsp.list()`, which enumerates the manager directly + and is unaffected by attachment bookkeeping. +7. **The `cfg.restart` gap is still open** (recorded landing #161): + `ensure_server` never forwards `pmacs.lsp.config[lang].restart` to + `pmacs.lsp.spawn`, so the field is silently dropped on auto-attach. + Stage 3b is the first stage that would benefit from setting it, and + Q#LN7 now records why it deliberately does not need it. + +Citation drift repaired per COHERENCE §25. Round 4's first pass stated +the `project_root_for` correction in this section without editing the +citation in §2.5 — the correction and the fix are different acts, and +noting one is not doing the other. Review caught a second stale citation +(`handle_server_requests`), which prompted a full sweep of every +`file:line` from §2.4 onward; it found four more. All six: +`project_root_for` 513 → **592** (and it now returns `root, source` +rather than a bare root), `ensure_server` 527 → **610**, +`handle_server_requests` 1448 → **1549**, `take_typed_edit` +12798 → **12827**, `pair.lua` 213 → **229**, and `compile.lua` +264 → **266**. Verified good and left alone: `listview.lua:138`, +`src/lsp.rs:264`, `src/diag.rs:50`, `src/process.rs:193`, +`src/project.rs:145`, and the `mod.rs` binding-block citations. The +pre-#161 line numbers inside Q#LN15 are left as written: that stage has +landed and its citations are historical record, not navigation. ## 1. What ships -Seven stages. The north star is VS Code parity; the honest statement of -where that lands is in §5, bet 6. +Eight stages, after round 4 split Stage 3. The north star is VS Code +parity; the honest statement of where that lands is in §5, bet 6. **Stage 1 — grammar, mode, and the editing table stakes.** `.lean` files highlight, carry a `lean4` major mode, and get comment-toggle and @@ -185,13 +299,21 @@ Independently valuable for every language pmacs supports; a prerequisite for Lean being usable across more than one Lake package. Split out precisely *because* it is cross-cutting — see §4. -**Stage 3 — the Lean language server.** `pmacs.lsp.config.lean4` drives +**Stage 3a — LSP dispatch seams and a path canonicalizer.** Pure +substrate, no Lean content, split from Stage 3 in round 4 for the reason +Stage 2 was: it changes machinery every language runs through. +`handle_server_requests` gains notification and response arms with a +pending-response purge, so a `send_request` reply is no longer drained +and dropped; `pmacs.fs.canonicalize` gives Lua the one primitive a +function-valued `config.root` needs to honor the canonical-path contract +#161 could only document. + +**Stage 3b — the Lean language server.** `pmacs.lsp.config.lean4` drives `lake serve` with a Lake-aware outermost root, a lazy toolchain probe and -a one-shot `lean --server` fallback, and a notification-subscription seam -so `$/lean/fileProgress` has an owner. Adds -`textDocument/waitForDiagnostics`. Diagnostics, hover, completion, -goto-definition, document symbols, and semantic tokens all arrive through -the existing typed surfaces. +a one-shot `lean --server` fallback, and subscribes `$/lean/fileProgress` +on 3a's seam. Adds `textDocument/waitForDiagnostics`. Diagnostics, hover, +completion, goto-definition, document symbols, and semantic tokens all +arrive through the existing typed surfaces. **Stage 4 — the Unicode input method.** Typing `\alpha` produces `α`, `\to` produces `→`, `\<>` produces `⟨⟩` with the point between them. @@ -215,6 +337,13 @@ panel. ## 2. Ground truth (scouted 2026-07-24, `main` @ `e745068`) +Stage 3's facts were **re-verified 2026-07-25 against `main` @ +`46a1b8f`**, six merged PRs later; what changed is recorded in §0.1's +round 4 rather than rewritten in place, so a reader can see which +claims moved. Facts for stages 4–7 still carry the 2026-07-24 date and +should be re-scouted before those stages are framed for +implementation. + ### 2.1 Crate facts (external, verified by downloading and reading both) Two candidate grammar crates exist. They are not close in quality. @@ -363,7 +492,7 @@ and pin it.* params }` and `Response { id, result, error, method }` variants. Unknown server methods are delivered, not dropped. - **But `events_take` has exactly one consumer**: `handle_server_requests` - at `builtin/runtime/lsp.lua:1448`, driven off `pmacs._async.tick`. It + at `builtin/runtime/lsp.lua:1549`, driven off `pmacs._async.tick`. It `take`s — a drain. Its `if/elseif` chain handles five `request` methods and `initialized`, and **ignores every `notification` and every `response`**. A second module calling `events_take` would steal events @@ -379,7 +508,7 @@ and pin it.* ### 2.5 Project-root detection -`project_root_for` (`builtin/runtime/lsp.lua:513`) resolves: +`project_root_for` (`builtin/runtime/lsp.lua:592`) resolves: `pmacs.lsp.config[language].root` → `pmacs.project.detect` → the file's own directory. Two gaps for Lean: @@ -407,7 +536,7 @@ directory. Two gaps for Lean: then reports import errors for the whole file. Third, and the reason Stage 2 exists: `ensure_server` -(`builtin/runtime/lsp.lua:527`) reuses any live server with a matching +(`builtin/runtime/lsp.lua:610`) reuses any live server with a matching `language_id` regardless of the new file's project, so **the first `.lean` file opened fixes the root for every later `.lean` file.** For most languages that is an inconvenience; for Lean, where `lake serve` is bound @@ -424,10 +553,10 @@ changes loose-file behavior for every language. `builtin/runtime/pair.lua` is the whole precedent for "react to a typed character": subscribe to `buffer.after-edit`, gate on -`ed.this_command() == "buffer.self-insert"` (`pair.lua:213`), then take the +`ed.this_command() == "buffer.self-insert"` (`pair.lua:229`), then take the exact provenance record. -`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12798`) returns +`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12827`) returns `{ buffer, window, codepoint, char, requested_start, requested_end, effective_start, effective_end, inserted_len, post_cursor, clean }` — or nil. Its doc comment is explicit: @@ -456,7 +585,7 @@ cross-peer-degraded**. Lean's `⟨⟩` is outside that set. shows the adopter shape, gated on `spec.display == "panel"`. `pmacs.window.params()` and `pmacs.window.quit()` complete the surface. - Read-only generated buffers use the listview idiom, documented at - `builtin/runtime/compile.lua:264`: an erroring `pmacs.buffer.add_intercept` + `builtin/runtime/compile.lua:266`: an erroring `pmacs.buffer.add_intercept` for user edits, with module writes passing `{ bypass_intercept = true }`. - **Note for whoever picks this up on another machine:** the ledgers are stale about this. `docs/active-work.md:57` still heads the lane "Stage 1 @@ -528,7 +657,7 @@ PATH, both are executable, and both fail. So: old, and lake working but the directory is not a Lake package. Only the third is a *version* question. - **Acceptance cannot assume a working Lean toolchain exists.** Every - Stage 3+ test runs against the fake LSP server; a live `lake serve` + Stage 3b+ test runs against the fake LSP server; a live `lake serve` smoke is PATH-gated *and* success-gated, following the #123 JSON/YAML provider-smoke pattern. @@ -706,6 +835,27 @@ consulted before configuring. the failing server *first*, then swaps the config, then spawns — the fallback is a fresh server, not a restart of the old one. + Round 4 verified this is necessary rather than defensive. The spec + default is `LspRestartPolicy::OnCrash` (`src/lsp.rs:165`), and the + termination handler calls `should_restart(policy)` — which, unlike the + `termination_warrants_restart` helper beside it, never consults the + exit code. `maybe_restart` re-fires on every elapsed backoff with **no + attempt ceiling**, so a broken `lake` respawns indefinitely. + `pmacs.lsp.stop` sets `restart = Never` on the way out + (`src/lsp.rs:1349`), which is precisely what disarms it. Acceptance 36 + is pinning a live mechanism, not a hypothetical one. + + **Why the latch does not just set `restart = "never"` on the spawn.** + It cannot: `ensure_server` never forwards `cfg.restart` to + `pmacs.lsp.spawn` — `lua_to_lsp_spec` reads the key but the spawn + table never sets it — so the field is silently dropped on every + auto-attach today. That gap was found landing #161 and is not Stage + 3's to close (it changes behavior for every language that has set + `restart` believing it worked; `statusline_segments_acceptance` a12 is + one such caller). The stop-then-spawn ordering is correct regardless of + how that gap is eventually resolved, which is the reason to prefer it + over a fix that depends on the gap closing first. + **The swap is a field update, not a table replacement.** It rewrites only `command` and `args`, preserving any user-supplied `env`, `settings`, `init_options`, and `root` on `pmacs.lsp.config.lean4`. A @@ -732,18 +882,87 @@ fallback. That is a one-line status message, once per session, and it buys not blocking every other user's first attach behind a process round-trip. +**Attribution (COHERENCE §9).** The probe is background work that spawns +an OS process, and `ProcessSpec.label` is the only identity a process +carries — caller-supplied and unvalidated, but it is what +`pmacs.process.list` renders. The probe spawns as `lean:lake-version-probe` +rather than inheriting a default, so a user who looks at the process list +while wondering why their editor touched `lake` finds an answer with an +owner in it. Both the probe's verdict and the latch firing report through +`pmacs.editor.set_status` — the channel that exists — per §1.2's rule and +its corollary: each is pinned by a test that observes the channel, since a +report through `pmacs.error` would be a dead sixteenth call site. + No `init_options`. Per §2.8, `hasWidgets?` defaults to false and that is the correct value for a client that reads plain goals out of standard messages. ### Q#LN8 — Lake-aware root via a **function-valued** `config.root` -Generalize `project_root_for` (`builtin/runtime/lsp.lua:513`) so -`pmacs.lsp.config[lang].root` may be a `function(path) -> string|nil` as -well as a string, and implement Lean's resolver in -`builtin/runtime/lean.lua`: walk up from the file's directory collecting -every ancestor containing `lean-toolchain`, and return the **outermost**; -fall back to `pmacs.project.detect`, then the file's directory. +**The generalization landed in Stage 2 (#161).** `project_root_for` is +now `builtin/runtime/lsp.lua:592` and returns `root, source`; +`config[lang].root` already accepts a `function(path) -> string|nil`, +with per-directory memoization keyed weakly on the resolver itself. What +remains for Stage 3b is Lean's resolver in `builtin/runtime/lean.lua`: +walk up from the file's directory collecting every ancestor containing +`lean-toolchain`, and return the **outermost**; decline (return nil) when +there is none, which falls through to `pmacs.project.detect` and then the +file's directory. + +**How the walk tests for the marker — and why not the obvious way.** +`pmacs.fs.stat` is asynchronous: it returns an awaitable handle +(`builtin/runtime/fs.lua:93`) that only settles under `:await()` inside a +coroutine. The resolver has no coroutine. It runs synchronously inside +`ensure_server` ← `attach_buffer` ← the `buffer.after-load` hook, so +awaiting is not merely slow there, it is unavailable — and blocking the +attach on filesystem I/O is the cost rev 1 refused for the probe. The +walk therefore uses the **Lua stdlib**: `io.open(dir .. "/lean-toolchain", +"r")`, which returns nil for a missing path. Round 4 probed that `io` and +`os` are exposed in the sandbox rather than assuming it; `terminal.lua` +already depends on `os.getenv`. + +One edge, probed: **`io.open` succeeds on a directory** (the handle opens; +`read` returns nil without raising). A `lean-toolchain` *directory* would +therefore read as a marker under an `io.open` truth test — wrong, and +wrong silently. + +The fix is **not** "read a byte and require it to be non-nil", which was +this section's first answer and is wrong in the other direction: an +**empty** `lean-toolchain` file also reads nil at EOF, so that rule +declines a marker that exists. Marker semantics here are `lean4-mode`'s +`locate-dominating-file` semantics — *existence*, not content — and a +`lean-toolchain` can legitimately be empty. The discriminator is +`read`'s **second** return, probed on LuaJIT 2.1: + +| Path | `io.open` | `f:read(1)` | Verdict | +|---|---|---|---| +| file with content | handle | `"l"`, no error | marker | +| **empty file** | handle | `nil`, **no error** | **marker** | +| directory | handle | `nil`, `"Is a directory"` | decline | +| missing | `nil` | — | decline | + +So: `local data, err = f:read(1)` and decline only on a non-nil `err`. +The rule is robust across platforms without needing to be re-probed on +each, because both directory behaviors are declines — a platform whose +`fopen` refuses a directory outright fails at `io.open`, and one that +opens it fails at `read`. There is no platform on which a directory both +opens and yields a byte. + +Acceptance 24a and 24b pin the two halves, and each must be shown to +fail against the implementation that satisfies only the other — +otherwise "handles directories" is satisfiable by the version that +breaks empty files, which is exactly how this section's first answer got +written. + +**The result must be canonical.** #161's contract: a configured root +reaches `file_uri_for` verbatim and that URI is the affinity key, so two +spellings of one package are two servers. The path handed to the resolver +is *not* canonical (round 4, finding 2), and Lua had no canonicalizer — +hence Q#LN20. The resolver canonicalizes the file's directory **once**, +before the walk, and strips components from there: every ancestor of a +canonical path is itself canonical, so one call suffices. If +canonicalization fails (a deleted file, a broken symlink), the resolver +declines rather than returning a path it cannot vouch for. **The walk stops at `pmacs.project.search_boundary()`.** This is not optional politeness: `detect_project_within` (`src/project.rs:213`) exists @@ -777,7 +996,7 @@ write-only API from Lua.** Rev 2 specified only the notification half. That was a hole, since Q#LN16 (`waitForDiagnostics`), Q#LN19 (`imports` / `importedBy`), and Q#LN12's typed goal request all await replies. Both halves ship in -Stage 3. +Stage 3a. ```lua pmacs.lsp.on_notification(method, fn) -- fn(sid, params); persistent @@ -808,10 +1027,81 @@ directions: a Lean subscriber must not cause `workspace/applyEdit` to be missed, and a raising subscriber must not stop later events in the same drain. -Stage 3 registers `$/lean/fileProgress` on the notification seam and +**The seam's contract, stated because round 4 found it narrower than rev +4 implied: subscribers fire only for servers with a live buffer +attachment.** `handle_server_requests` builds its sid list from +`attachments`, so a server with no attached buffer is never drained — and +`push_event` appends with no cap, so that server's queue grows +unboundedly. Both facts are pre-existing and neither is Stage 3a's to +fix. What they change is where the purge may be wired. + +**The purge must not ride the drain.** `attach_buffer` removes a sid +from `attachments` as soon as `server_is_live` reports false and rebuilds +the attachment against a fresh server, so a `crashed` / `stopped` event +is the event *least* likely to be drained — the drain stops visiting +that server at almost exactly the moment the event is queued. A purge +triggered by observing that event therefore leaks in the case it exists +to handle. + +So the purge polls **`pmacs.lsp.list()`** after each drain instead. That +call enumerates the manager directly and is unaffected by attachment +bookkeeping, which is what makes it the right authority: a sid that is +absent, terminal, or running a new generation settles its pending +one-shots with an error, whether or not anything ever drained it. +Acceptance 34's second half exercises a server that is in **no** +attachment, because that is the shape an event-driven purge fails and a +polled one survives. + +The uncapped queue is recorded as a named deferral (§6) rather than fixed +here: bounding it is a policy question about which events may be dropped, +and answering it inside a seam PR would be the kind of smuggling §4 +forbids. + +Stage 3b registers `$/lean/fileProgress` on the notification seam and `waitForDiagnostics` on the response seam; stages 5 and 7 use the response seam for `plainGoal` and the hierarchy calls. +### Q#LN20 — `pmacs.fs.canonicalize` (Stage 3a) + +A synchronous binding wrapping `std::fs::canonicalize`, returning the +resolved absolute path or nil. Roughly fifteen lines. + +It exists because #161 documented an obligation Lua cannot discharge. A +configured root — string or resolver return — is fed to `file_uri_for` +verbatim, and that URI is the server-affinity key; the `"detected"` arm is +canonicalized for free because `pmacs.project.detect` canonicalizes before +walking, but the `"config"` arm is not. Round 4 probed that +`pmacs.editor.file_path()` collapses `.` and `..` lexically while leaving +symlinks intact, so a resolver walking up from it returns a non-canonical +root. Opening one Lake package through a symlinked path and through the +real path would spawn two `lake serve` processes — the bug Stage 2 was +built to prevent, re-entered through Stage 3b's door. + +**Synchronous, deliberately, and this is the one thing to get right.** +The whole reason `pmacs.fs.stat` cannot serve here is that it is async +(Q#LN8), so a canonicalizer that returned an awaitable would fail for the +same reason and leave the obligation undischarged. It is one `stat`-class +syscall on a path the editor is already opening; `pmacs.project.detect` +performs the same work synchronously today, on the same hook, so this +adds no blocking class that the attach path does not already have. + +Why this rather than the two alternatives considered in round 4: + +- *Accept it as a named degradation* — document that a symlinked open + spawns a second server and pin the behavior. Rejected: it reopens the + defect Stage 2 closed, and the failure is invisible (two servers, both + apparently working, twice the memory, diagnostics split between them). +- *Anchor the walk on `pmacs.project.detect`'s canonical root* — free, no + new surface. Rejected as incorrect, not merely inelegant: `detect` is + innermost-wins over its own marker set, so with `.git` at `~/code` and + the Lake package at `~/code/proj`, anchoring at `~/code` and walking + *up* never sees `~/code/proj/lean-toolchain`. It resolves the wrong root + in a layout that is entirely ordinary. + +The binding is general, not Lean-shaped: it serves every future +function-valued `root`, and it is what lets #161's doc comment stop +warning about a footgun and start naming a fix. + ### Q#LN10 — Stage 4 mechanism: one shared provenance read, not two The hazard is §2.6 — `take_typed_edit()` is one-shot and `pair.lua` @@ -922,8 +1212,9 @@ stage numbers and was wrong three ways): | Stage | Rust | |---|---| | 1 | `Cargo.toml` + `BUILTIN_LANGUAGES` entry + Q#LN4's four capture entries | -| 2 | `lsp.list()` row builder (`mod.rs:9919`) | -| 3 | **none** — Lua only | +| 2 | `lsp.list()` row builder (`mod.rs:9926`) | +| 3a | `pmacs.fs.canonicalize` (Q#LN20) — the seams themselves are Lua only | +| 3b | **none** — Lua only | | 4 | **none** — Lua only | | 5 | `request_plain_goal` + its binding | | 6 | `LspServerSpec` severity-policy field and its publish-path honoring | @@ -978,7 +1269,7 @@ rough edge but a correctness failure: `lake serve` is bound to one Lake package, so the second package a user opens gets a server that cannot resolve its imports. -The change is small and spans two files: +The change was small and spanned two files (Stage 2, landed as #161): - **`src/lua_bindings/mod.rs:9919`** — the `lsp.list()` row builder sets `id`/`label`/`language_id`/`command`/`state`/`attempt`. Add `root_uri` @@ -1045,7 +1336,7 @@ elaboration is memory-hungry. rust-analyzer has the same property and no editor caps it by default. No cap ships here; `pmacs.lsp.stop` is the manual escape, and an LRU reaping policy is named in §6. -### Q#LN16 — `textDocument/waitForDiagnostics` (Stage 3) +### Q#LN16 — `textDocument/waitForDiagnostics` (Stage 3b) A plain request (no position, so no `outbound_position` concern — Q#LN12 does not apply). It resolves when the server has finished elaborating the @@ -1125,28 +1416,48 @@ never lands. |---|---|---|---| | 1 | grammar, mode, comments, pairs, md fences | new crate; **global capture table** | — | | 2 | multi-root server affinity | **`ensure_server`, shared by every language** | — | -| 3 | `lake serve` + probe/latch, Lake root, notification seam, `waitForDiagnostics` | two `lsp.lua` generalizations | 1, 2 | +| 3a | notification/response seams + purge; `pmacs.fs.canonicalize` | **the shared event drain, run by every language** | — | +| 3b | `lake serve` + probe/latch, Lake root, `waitForDiagnostics` | none — Lean-only files plus one config entry | 1, 2, 3a | | 4 | Unicode input method | **refactors `pair.lua`'s provenance read** | 1 | -| 5 | goal panel | new typed LSP request; panel adopter | 3 | -| 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3, 5 | -| 7 | module hierarchy | listview adopter + one typed Rust request | 3 | +| 5 | goal panel | new typed LSP request; panel adopter | 3a, 3b | +| 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3b, 5 | +| 7 | module hierarchy | listview adopter + one typed Rust request | 3a, 3b | -Three of the seven carry risk that is *not* about Lean — stages 1, 2, and -6 each change something every language touches. That is the organizing -principle of the split: **no PR in this arc mixes a cross-cutting -substrate change with Lean feature content.** A reviewer looking at Stage -2 sees only `ensure_server`; a reviewer looking at Stage 3 sees only Lean. +Four of the eight carry risk that is *not* about Lean — stages 1, 2, 3a, +and 6 each change something every language touches. That is the +organizing principle of the split: **no PR in this arc mixes a +cross-cutting substrate change with Lean feature content.** A reviewer +looking at Stage 2 sees only `ensure_server`; a reviewer looking at Stage +3b sees only Lean. + +Round 4 found Stage 3 breaking that rule while stating it — the row above +used to read "two `lsp.lua` generalizations" for a stage the prose called +Lean-only. One generalization shipped as Stage 2; extracting the other as +3a is what makes the claim true again. The rule is only worth writing +down if it survives contact with a stage that is inconvenient to split. Ordering notes: - **Stage 2 has no Lean in it and could ship independently of this arc.** It is sequenced here because Lean is the language that makes its absence - a correctness bug rather than an inconvenience, and because Stage 3's + a correctness bug rather than an inconvenience, and because Stage 3b's acceptance would otherwise have to encode the broken behavior. -- **Stage 4 does not depend on stages 2–3** and could run in parallel, but - should not: both touch `lsp.lua`/`pair.lua`-adjacent runtime files, and - the #126/#127 lesson is that parallel-safety requires the file split be - agreed *before* either lane starts. Sequential is cheaper. +- **Stage 3a likewise has no Lean in it**, and the same reasoning applies + one level down: the response seam is a hole in `send_request` for every + language — Lean is merely the first caller that needs a reply. It is + sequenced before 3b because 3b's `waitForDiagnostics` and file-progress + subscription both consume it, and because a Lean PR that also rewrote + the shared drain could not be reviewed on either axis. +- **3a and 3b cannot run as sibling worktrees.** 3b's Lean subscriber is + written against the seam 3a adds, and both touch + `builtin/runtime/lsp.lua`. Unlike stages 1 and 2, this pair is strictly + sequential — recorded here, per the #126/#127 lesson, rather than + discovered in a rebase. +- **Stage 4 does not depend on stages 2, 3a, or 3b** and could run in + parallel, but should not: both touch `lsp.lua`/`pair.lua`-adjacent + runtime files, and the #126/#127 lesson is that parallel-safety + requires the file split be agreed *before* either lane starts. + Sequential is cheaper. - **Stage 6 depends on Stage 5** only for the read-only generated-buffer and panel machinery, which Stage 5 establishes. If Stage 5 slips, Stage 6 can carry that machinery itself at the cost of duplicating it. @@ -1185,7 +1496,7 @@ Stated so they can be scored, per house style. inside `buffer.after-edit` re-enters the hook in a way pairing does not already survive. Confidence: medium — pairing does the same thing, but over a single codepoint rather than a multi-byte span. -6. **These seven stages reach rough VS Code parity for everything except +6. **These eight stages reach rough VS Code parity for everything except the interactive infoview.** Scored honestly rather than aspirationally. What lands: highlighting, goal view, Unicode input, diagnostics, hover, completion, goto-definition, symbols, semantic tokens, `#eval` @@ -1225,6 +1536,36 @@ What remains deferred: unbounded `lake serve` growth possible. No editor caps this by default and pmacs will not either in this arc, but the policy question is now live in a way it was not before. +- **The uncapped LSP event queue** — `push_event` appends without a + bound, and `handle_server_requests` drains only servers with a live + buffer attachment, so an unattached server's events accumulate for the + life of the session (round 4, finding 6). Bounding it means deciding + 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 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 + every language whose config sets the field believing it works. Q#LN7 is + designed not to need it. - **Block-comment toggle** (`/- -/`) and **docstring awareness** (`/-- -/`) — confirmed as owned by the comment arc's framing, not this one. @@ -1309,58 +1650,113 @@ What remains deferred: the markerless one's server carries the fallback directory as `cwd` while matching on a nil affinity key. -**Stage 3 — the Lean language server** +**Stage 3a — dispatch seams and the canonicalizer (no Lean content)** -22. Opening a `.lean` file inside a Lake package spawns one server with - `cwd` and `rootUri` at the package root. -23. **Outermost-root pin:** a file under - `/.lake/packages/dep/…` whose ancestor chain contains two - `lean-toolchain` files resolves to ``, not to `dep`. Run with - `pmacs.project.set_search_boundary` at the fixture root so the - assertion is hermetic. -24. **Boundary pin:** with the search boundary set at the fixture root, a - `lean-toolchain` planted in an ancestor *above* the boundary is not - reached — the resolver stops at the boundary rather than walking past - it. -25. A string-valued `pmacs.lsp.config.lean4.root` still works — the Q#LN8 - generalization is strictly additive. -26. `didOpen` carries `languageId = "lean4"`. -27. **Fallback-latch pin (Q#LN7):** a `lake` stub that exits non-zero — - reproducing §2.9's shimmed-elan state — causes exactly **one** restart - against `lean --server`, and a second failure surfaces an error rather - than looping. The latch does not re-arm within the session. -28. **Probe pin:** a `lake` stub reporting version 3.0.0 triggers the - fallback; one reporting 3.1.0 does not. A stub that never exits does - not block the attach — the optimistic `lake serve` spawn proceeds. -29. A `$/lean/fileProgress` notification delivered through the fake server - reaches a registered `on_notification` subscriber. -30. **Dispatch-integrity pin:** with a Lean subscriber registered, a - `workspace/applyEdit` request in the same drain is still handled — no - event is stolen. -31. A subscriber that raises does not prevent later events in the same - drain from being processed. -32. **Response-seam pin (Q#LN9).** A `send_request` reply reaches its - registered `on_response` one-shot, and the one-shot is **removed - before** invocation — a raising handler is not re-entered. Bites - against rev 2, where no Lua consumed `ev.kind == "response"` at all - and the reply was dropped. -33. **Response dispatch-integrity pin.** With a response subscriber - registered, `workspace/applyEdit` in the same drain is still handled; - a raising response handler does not stop later events in that drain. - Mirrors the notification-side pins above. -34. **Pending-purge pin.** A server that dies with a response outstanding - invokes the pending one-shot with an error and clears it — the - registration does not leak and the awaiting caller does not hang. -35. **Config-preservation pin (Q#LN7).** After the fallback latch fires, - user-supplied `env` / `settings` / `init_options` / `root` on - `pmacs.lsp.config.lean4` survive; only `command` and `args` change. -36. **No-respawn-loop pin.** The latch stops the failing server before - spawning the fallback, so `RestartPolicy` does not respawn the broken - command underneath it. -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. +Driven against `pmacs_fake_lsp` through an already-shipped language, for +the same reason Stage 2's suite was: the drain is shared by every +language, and a suite that reaches it only through Lean would understate +the blast radius. + +- **29.** A notification delivered through the fake server reaches a registered + `on_notification` subscriber. +- **30.** **Dispatch-integrity pin:** with a subscriber registered, a + `workspace/applyEdit` request in the same drain is still handled — no + event is stolen. +- **31.** A subscriber that raises does not prevent later events in the same + drain from being processed. +- **32.** **Response-seam pin (Q#LN9).** A `send_request` reply reaches its + registered `on_response` one-shot, and the one-shot is **removed + before** invocation — a raising handler is not re-entered. Bites + against rev 2, where no Lua consumed `ev.kind == "response"` at all + and the reply was dropped. +- **33.** **Response dispatch-integrity pin.** With a response subscriber + registered, `workspace/applyEdit` in the same drain is still handled; + a raising response handler does not stop later events in that drain. + Mirrors the notification-side pins above. +- **34.** **Pending-purge pin, both edges.** A server that dies with a + response outstanding invokes the pending one-shot with an error and + clears it. **And** a server that is in **no attachment** does the + same, rather than stranding the registration behind a drain that never + visits it. The second half must be shown to fail against a purge + wired to a death event seen in the drain; otherwise this criterion is + satisfied by the implementation that leaks. (Rev 5 first worded the + second edge as a killed buffer; there is no buffer-kill hook, so + nothing removes the attachment and that path does not leak. Corrected + in round 2 — see §0.1 finding 6.) +- **34a.** **Canonicalizer pin (Q#LN20).** `pmacs.fs.canonicalize` resolves a + symlinked and dot-segmented path to the same string as the real path, + and returns nil for a nonexistent one. Fixture builds the symlink + rather than assuming one exists. +- **34b.** **Affinity-through-canonicalization pin.** With a function-valued + `root` that canonicalizes, the same project opened by its real path + and through a symlink reuses **one** server. Falsified by a resolver + that returns the path verbatim, which yields two — this is the + regression Q#LN20 exists to prevent, so it is asserted at the + affinity layer, not just at the binding. + +**Stage 3b — the Lean language server** + +- **22.** Opening a `.lean` file inside a Lake package spawns one server with + `cwd` and `rootUri` at the package root. +- **23.** **Outermost-root pin:** a file under + `/.lake/packages/dep/…` whose ancestor chain contains two + `lean-toolchain` files resolves to ``, not to `dep`. Run with + `pmacs.project.set_search_boundary` at the fixture root so the + assertion is hermetic. +- **24.** **Boundary pin:** with the search boundary set at the fixture root, a + `lean-toolchain` planted in an ancestor *above* the boundary is not + reached — the resolver stops at the boundary rather than walking past + it. +- **24a.** **Marker-is-a-file pin (Q#LN8).** A `lean-toolchain` + *directory* does not mark a root. Bites against the bare `io.open` + truth test, which round 4 probed succeeds on directories — the shape + that would pass every other criterion here while being wrong. +- **24b.** **Empty-marker pin (Q#LN8).** An **empty** `lean-toolchain` + file *does* mark a root — marker semantics are existence, not content. + Bites against the read-a-byte-and-require-non-nil rule, which declines + it at EOF. 24a and 24b must each be shown to fail against the + implementation that satisfies only the other; a suite carrying just + one of them is satisfied by a resolver that is silently wrong for the + other case. +- **25.** A string-valued `pmacs.lsp.config.lean4.root` still works — the Q#LN8 + generalization is strictly additive. +- **26.** `didOpen` carries `languageId = "lean4"`. +- **27.** **Fallback-latch pin (Q#LN7):** a `lake` stub that exits non-zero — + reproducing §2.9's shimmed-elan state — causes exactly **one** restart + against `lean --server`, and a second failure surfaces an error rather + than looping. The latch does not re-arm within the session. +- **28.** **Probe pin:** a `lake` stub reporting version 3.0.0 triggers the + fallback; one reporting 3.1.0 does not. A stub that never exits does + not block the attach — the optimistic `lake serve` spawn proceeds. +- **35.** **Config-preservation pin (Q#LN7).** After the fallback latch fires, + user-supplied `env` / `settings` / `init_options` / `root` on + `pmacs.lsp.config.lean4` survive; only `command` and `args` change. +- **36.** **No-respawn-loop pin.** The latch stops the failing server before + spawning the fallback, so `RestartPolicy` does not respawn the broken + command underneath it. +- **36a.** **Attribution pin (COHERENCE §9/§1.2).** The probe process + appears in `pmacs.process.list` under a Lean-owned label, and the + latch firing leaves a status-line trace. Both assert through the + 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), **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 +(3b runs 22–28 then 35–37) and a markdown ordered list renumbers from +its first item regardless of what is written. Keeping the labels literal +means **every rev-4 number still denotes what it denoted in rev 4** — +"acceptance 34", "acceptance 27" — and the four criteria added in this +revision take letter suffixes rather than displacing anything. Round 3's +finding 4 was stale cross-references surviving a renumber; not +renumbering is the cheaper way to not repeat it. **Stage 4 — the Unicode input method** @@ -1447,7 +1843,7 @@ What remains deferred: - **#146 (HTML+CSS)** — the global capture table, and the requirement to pin retro-paint in both directions. Q#LN4 is that lesson applied. - **#123 (JSON/YAML)** — declarative `pmacs.lsp.config` entries with a - fake-server delivery proof plus PATH-gated live smokes. Stage 3 follows + fake-server delivery proof plus PATH-gated live smokes. Stage 3b follows it, with the extra success-gate §2.9 forces. - **#110 (auto-pairing)** — `take_typed_edit()` provenance, the fail-closed discipline on transformed source edits, and Q#AP1's optimistic-classifier @@ -1465,3 +1861,70 @@ What remains deferred: which Q#LN17 registers into. - **#94/#95 (LSP panels)** — `pmacs.listview.open` and the references/outline panel shape that Stage 7 reuses wholesale. + +## 9. Coherence impact (COHERENCE §20) + +Required of every framing since #163. Stated for stages 3a and 3b, the +work this revision authorizes; the earlier stages predate the rule and +are not retrofitted here. + +**Sections served.** §1.2 (the silence asymmetry) primarily, and §7 +(first-class workspaces) indirectly — per-root affinity is the workspace +concern arriving one language at a time. §9 (worker identity) is touched +but not advanced. + +**Golden journey (§2).** No step is touched. Neither stage changes what +happens between launching pmacs and editing a file; Lean is not on the +journey's critical path, and 3a is invisible to a user who has no Lean +installed. Stage 3b does make §2's step-3 grade slightly *worse* in one +narrow way, and it is honest to say so: a preconfigured-but-missing +`lake` is one more instance of the silent-spawn-failure class, on a +toolchain many users will not have. Q#LN7's status-line reports on the +probe verdict and the latch cover the Lean-specific paths, but they do +not fix the general failure — that remains Priority 1 work with its own +framing, as §1.2's frequency note already records. + +**Interaction islands (§6).** None added. Stage 3b introduces no keymap, +no modal surface, and no dispatch shadow. Its one user-facing command +(`M-x lean-wait-for-diagnostics`, Q#LN16) registers through the ordinary +command table and is reachable from `M-x` like everything else. + +**Config registry (§11).** Neither stage adds a `pmacs.config` option. +`pmacs.lsp.config.lean4` joins the existing declarative server table +alongside sixteen other languages — deliberately *not* the typed registry, +because moving one language's entry there while the other sixteen stay +put would fragment the surface rather than unify it. Migrating +`pmacs.lsp.config` wholesale is a config-arc concern; this lane must not +create a precedent that makes it harder. Stage 4's `lean.abbrev` gate is +where this arc does enter the registry, and Q#LN10 already commits to the +`editing.auto-pair` shape. + +**Background-work attribution (§9).** Three pieces of background work, +each with a named owner and an observable trace: + +| Work | Identity | Trace | +|---|---|---| +| `lake --version` probe | `ProcessSpec.label = "lean:lake-version-probe"`, visible in `pmacs.process.list` | status line on a verdict that triggers fallback | +| the fallback latch | the server it stops/spawns is already in `pmacs.lsp.list()` | status line on firing | +| root resolution | none — synchronous, inside the attach | status line on resolver failure (shipped #161) | + +This is attribution within the identity layer §9 says is absent, not a +fix for its absence: the probe carries a label because +`ProcessSpec.label` is the only field available, and §9's own ground +truth calls that "caller-supplied, unvalidated convention." Owner/purpose +/parent fields remain unbuilt, and nothing here joins the four activity +planes. What this lane commits to is not *worsening* the ratio — every +background action it adds is nameable in some user-visible view on the +day it ships. + +**Debt this revision retires.** Q#LN20 closes the gap #161 could only +document: a configured root reaching `file_uri_for` uncanonicalized. That +was coherence debt of exactly §1.3's compounding kind — a correct +substrate with a footgun the next caller was expected to disarm by +reading a comment. + +**Debt this revision names rather than pays.** Three, all in §6: the +uncapped event queue, the dropped `cfg.restart`, and — unchanged from +#161 — surfacing the spawn failure itself. Each is a behavior change for +languages other than Lean, and §4's rule is what keeps them out of a Lean +PR. diff --git a/src/bin/pmacs_fake_lsp.rs b/src/bin/pmacs_fake_lsp.rs index 5d50b19..67d6620 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. @@ -1062,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/src/editor.rs b/src/editor.rs index 2bc633b..dcff55a 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/src/lua_bindings/mod.rs b/src/lua_bindings/mod.rs index 37a1307..e27d9dd 100644 --- a/src/lua_bindings/mod.rs +++ b/src/lua_bindings/mod.rs @@ -6621,6 +6621,54 @@ pub fn install_async( ) -> mlua::Result<()> { lua.set_app_data(runtime.clone()); let pmacs: Table = lua.globals().get("pmacs")?; + + // Arc 8 Stage 3a (framing Q#LN20): the one *synchronous* filesystem + // primitive Lua has. `pmacs.fs` is otherwise an async, handle- + // returning surface built in `builtin/runtime/fs.lua`, so this + // arrives through a private table that file re-exports rather than + // joining the `_dispatch_fs_*` family it would not belong to. + // + // Installed here, alongside those dispatchers, purely for load + // order: `make_async_runtime` runs before `fs.lua` is evaluated, + // whereas `install_project` — the other plausible home — runs after + // it, so a canonicalizer placed there is nil when `fs.lua` reads it. + // + // Synchronous on purpose, and that is the whole point. The consumer + // is a function-valued `pmacs.lsp.config[lang].root`, which + // `project_root_for` calls from `ensure_server` <- `attach_buffer` + // <- the `buffer.after-load` hook — no coroutine, nothing to await + // on. An awaitable canonicalizer would be unusable there for exactly + // the reason `pmacs.fs.stat` already is, leaving #161's + // canonical-root obligation undischarged. The cost is one syscall on + // a path the editor is already opening; `pmacs.project.detect` + // canonicalizes synchronously on the same hook today. + { + let fs_priv = lua.create_table()?; + fs_priv.set( + "canonicalize", + lua.create_function(|_, path: String| { + // nil rather than an error for a path that cannot be + // resolved: asking about a deleted file or a broken + // symlink is ordinary, and raising would surface through + // `resolve_root_fn`'s pcall as a config bug, which it is + // not. + // + // `to_str`, NOT `display()`. A resolution that lands on + // non-UTF-8 bytes has no faithful string form, and + // `display()` would substitute U+FFFD and hand back a + // path that does not exist on disk — strictly worse than + // nil here, because this value becomes a server-affinity + // key via `file_uri_for` and would silently fail to + // round-trip. Unrepresentable is a decline, matching how + // the fs layer already treats non-UTF-8 symlink targets. + Ok(std::fs::canonicalize(&path) + .ok() + .and_then(|p| p.to_str().map(str::to_owned))) + })?, + )?; + pmacs.set("_fs", fs_priv)?; + } + let async_mod = lua.create_table()?; { diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs new file mode 100644 index 0000000..86be1d5 --- /dev/null +++ b/tests/lean4_server_acceptance.rs @@ -0,0 +1,1882 @@ +//! 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 27 / 28 / 35 / 36 — the probe and the fallback latch. +// +// **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(); + 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" + ); +} + +#[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(); + 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.settings = { lean = { verbose = true } } + pmacs.lsp.config.lean4.init_options = { hasWidgets = false } + _G.root_before = pmacs.lsp.config.lean4.root + ", + ); + + open(&state, &file); + settle(&mut state); + + let after: String = eval( + &state, + r#" + local c = pmacs.lsp.config.lean4 + return table.concat({ + 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, "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); + 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; + } + } + + // 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" + ); + // 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 + 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 false + "#, + ); + assert!( + !dying_still_running, + "the failing server is not respawning underneath the latch" + ); + assert_ne!(attached_sid(&state), "none"); +} + +// --------------------------------------------------------------------------- +// Acceptance 36a — attribution (COHERENCE §9 / §1.2). +// --------------------------------------------------------------------------- + +#[test] +fn acc36a_latch_leaves_a_status_line_trace() { + 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 status = state.core.borrow().status.clone(); + assert!( + 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 the fallback itself still worked, so the user + // would silently be on a different server than they configured. + 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, rec.version, 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" + ); +} + +// --------------------------------------------------------------------------- +// 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 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] +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" + ); +} + +// --------------------------------------------------------------------------- +// 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:?}" + ); +} + +// --------------------------------------------------------------------------- +// 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:?}" + ); +} + +// --------------------------------------------------------------------------- +// 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() { + // 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"); + 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 = "default-lean4", + 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:?}" + ); +} + +// --------------------------------------------------------------------------- +// 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" + ); +} 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" + ); } diff --git a/tests/lsp_dispatch_seams_acceptance.rs b/tests/lsp_dispatch_seams_acceptance.rs new file mode 100644 index 0000000..f644367 --- /dev/null +++ b/tests/lsp_dispatch_seams_acceptance.rs @@ -0,0 +1,724 @@ +//! Arc 8 Stage 3a acceptance — LSP notification/response dispatch seams +//! and `pmacs.fs.canonicalize`. +//! +//! `docs/lean4-mode-framing.md` Q#LN9 and Q#LN20, acceptance 29–34 plus +//! 34a/34b. +//! +//! This suite deliberately contains **no Lean content**. +//! `handle_server_requests` (`builtin/runtime/lsp.lua`) is the single +//! LSP event drain for every language in pmacs, so the change is +//! exercised through an already-shipped language driven against +//! `pmacs_fake_lsp`. A suite that reached the drain only through Lean +//! would understate the blast radius — the same reasoning that shaped +//! Stage 2's suite. +//! +//! Every fixture calls `pmacs.project.set_search_boundary` at its own +//! tempdir root, so a stray marker above the temp directory cannot make +//! a "markerless" case silently detected. + +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() +} + +/// A fresh editor with the shipped language configs cleared, so the only +/// server any test can spawn is the fake one it configures itself. +fn editor() -> EditorState { + let state = EditorState::new(); + exec(&state, "pmacs.lsp.config = {}"); + state +} + +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 dir(&self, rel: &str) -> PathBuf { + self.root.join(rel) + } + + fn bind(&self, state: &EditorState) { + exec( + state, + &format!( + "pmacs.project.set_search_boundary(\"{}\")", + lua_str(&self.root) + ), + ); + } +} + +fn configure(state: &EditorState, language: &str) { + exec( + state, + &format!( + "pmacs.lsp.config.{language} = {{ command = \"{}\" }}", + fake_lsp_path() + ), + ); +} + +fn open(state: &EditorState, path: &Path) { + exec( + state, + &format!("pmacs.buffer.find_or_open(\"{}\")", lua_str(path)), + ); +} + +/// `tick_async` is what drives the drain: `handle_server_requests` is +/// wrapped onto `pmacs._async.tick`, so a settle loop without it moves +/// the LSP state machine while never delivering a single event to Lua. +fn settle(state: &mut EditorState) { + for _ in 0..8 { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + std::thread::sleep(Duration::from_millis(2)); + } +} + +/// A rust project with one file, an attached fake server, and the +/// probes below installed. Returns the opened file's path. +fn attached_rust(state: &mut EditorState, fx: &Fixture) -> PathBuf { + fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n"); + let file = fx.write("proj/src/main.rs", "fn main() {}\nlet x = 1;\n"); + fx.bind(state); + configure(state, "rust"); + open(state, &file); + settle(state); + file +} + +/// The sid of the single live server, as a Lua expression fragment. +const THE_SID: &str = "pmacs.lsp.list()[1].id"; + +// --------------------------------------------------------------------------- +// Acceptance 29 — a notification reaches a registered subscriber. +// --------------------------------------------------------------------------- + +#[test] +fn acc29_notification_reaches_a_registered_subscriber() { + let fx = Fixture::new(); + let mut state = editor(); + // Registered BEFORE the open, so the didOpen-triggered `pmacs/echo` + // is in the first drain. + exec( + &state, + r#" + _G.seen = {} + pmacs.lsp.on_notification("pmacs/echo", function(sid, params) + _G.seen[#_G.seen + 1] = tostring(params and params.uri) + end) + "#, + ); + attached_rust(&mut state, &fx); + + let n: i64 = eval(&state, "return #_G.seen"); + assert!( + n >= 1, + "expected at least one pmacs/echo notification, got {n}" + ); + let first: String = eval(&state, "return _G.seen[1]"); + assert!( + first.starts_with("file://") && first.ends_with("main.rs"), + "subscriber got the document uri; saw {first:?}" + ); +} + +#[test] +fn acc29_subscriber_for_an_unsent_method_does_not_fire() { + let fx = Fixture::new(); + let mut state = editor(); + exec( + &state, + r#" + _G.hits = 0 + pmacs.lsp.on_notification("pmacs/never", function() _G.hits = _G.hits + 1 end) + "#, + ); + attached_rust(&mut state, &fx); + + // Non-vacuity for acc29: the seam is method-keyed, not a firehose. + // Without this, a subscriber invoked for every notification would + // pass the test above while being wrong. + let hits: i64 = eval(&state, "return _G.hits"); + assert_eq!(hits, 0, "a subscriber must only fire for its own method"); +} + +// --------------------------------------------------------------------------- +// Acceptance 30 + 33 — dispatch integrity: with subscribers registered, +// a `workspace/applyEdit` request in the same drain is still handled. +// +// The fake server writes the applyEdit request and the executeCommand +// response back to back, so both land in one `events_take` batch. That +// co-occurrence is the point: a seam that consumed the batch, or that +// returned early, would starve the `request` arms that share it. +// --------------------------------------------------------------------------- + +fn drive_apply_edit(state: &mut EditorState, file: &Path) { + exec( + state, + &format!( + r#" + local sid = {THE_SID} + local uri = "file://{}" + _G.rid = pmacs.lsp.send_request(sid, "workspace/executeCommand", {{ + command = "pmacs.fake.applyEdit", + arguments = {{ uri }}, + }}) + _G.response_hits = 0 + pmacs.lsp.on_response(sid, _G.rid, function(result, err) + _G.response_hits = _G.response_hits + 1 + end) + "#, + lua_str(file) + ), + ); + settle(state); +} + +fn buffer_text(state: &EditorState) -> String { + eval( + state, + "local b = pmacs.window.buffer() return b:slice(0, b:len())", + ) +} + +#[test] +fn acc30_apply_edit_still_handled_with_a_notification_subscriber() { + let fx = Fixture::new(); + let mut state = editor(); + exec( + &state, + r#" + _G.notes = 0 + pmacs.lsp.on_notification("pmacs/echo", function() _G.notes = _G.notes + 1 end) + "#, + ); + let file = attached_rust(&mut state, &fx); + assert!( + eval::(&state, "return _G.notes") >= 1, + "precondition: the notification subscriber is actually firing" + ); + + drive_apply_edit(&mut state, &file); + + assert!( + buffer_text(&state).contains("ED2"), + "workspace/applyEdit must still be applied with a subscriber \ + registered; buffer was {:?}", + buffer_text(&state) + ); +} + +#[test] +fn acc33_apply_edit_still_handled_with_a_response_subscriber() { + let fx = Fixture::new(); + let mut state = editor(); + let file = attached_rust(&mut state, &fx); + drive_apply_edit(&mut state, &file); + + // Both halves in one drain: the response was delivered to its + // one-shot AND the server-originated request was serviced. + assert_eq!( + eval::(&state, "return _G.response_hits"), + 1, + "the executeCommand response reaches its one-shot" + ); + assert!( + buffer_text(&state).contains("ED2"), + "workspace/applyEdit must still be applied with a response \ + subscriber registered; buffer was {:?}", + buffer_text(&state) + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 31 — a raising subscriber does not stop later events in the +// same drain (and does not stop the `request` arms either). +// --------------------------------------------------------------------------- + +#[test] +fn acc31_raising_notification_subscriber_does_not_stop_the_drain() { + let fx = Fixture::new(); + let mut state = editor(); + exec( + &state, + r#" + _G.second_hits = 0 + pmacs.lsp.on_notification("pmacs/echo", function() + error("subscriber blew up") + end) + pmacs.lsp.on_notification("pmacs/echo", function() + _G.second_hits = _G.second_hits + 1 + end) + "#, + ); + let file = attached_rust(&mut state, &fx); + + assert!( + eval::(&state, "return _G.second_hits") >= 1, + "a raising subscriber must not starve the ones after it" + ); + + // And the shared `request` arms still run in a later drain. + drive_apply_edit(&mut state, &file); + assert!( + buffer_text(&state).contains("ED2"), + "a raising subscriber must not stop workspace/applyEdit" + ); +} + +#[test] +fn acc33_raising_response_handler_does_not_stop_the_drain() { + let fx = Fixture::new(); + let mut state = editor(); + let file = attached_rust(&mut state, &fx); + exec( + &state, + &format!( + r#" + local sid = {THE_SID} + _G.notes_after = 0 + pmacs.lsp.on_notification("pmacs/echo", function() + _G.notes_after = _G.notes_after + 1 + end) + local rid = pmacs.lsp.send_request(sid, "workspace/executeCommand", {{ + command = "pmacs.fake.applyEdit", + arguments = {{ "file://{}" }}, + }}) + pmacs.lsp.on_response(sid, rid, function() error("handler blew up") end) + "#, + lua_str(&file) + ), + ); + settle(&mut state); + + assert!( + buffer_text(&state).contains("ED2"), + "a raising response handler must not stop workspace/applyEdit in \ + the same drain" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 32 — the one-shot is removed exactly once, whether or not +// the handler raises. +// +// Named for what it pins rather than for the framing's wording. Q#LN9 +// specifies removal *before* invocation, and the implementation does +// that — but bite-testing showed the before/after ordering is not +// observable on its own: `pcall` catches the raise either way, so +// removal after the call is behaviorally identical unless a handler +// re-enters the drain, which nothing does. What IS observable, and what +// this pins, is that removal is **unconditional**: the bite that moves +// it inside `if ok then` fails here 2 != 1, because the surviving +// registration gets invoked a second time by the purge. +// --------------------------------------------------------------------------- + +#[test] +fn acc32_response_one_shot_is_removed_even_when_the_handler_raises() { + let fx = Fixture::new(); + let mut state = editor(); + attached_rust(&mut state, &fx); + exec( + &state, + &format!( + r#" + local sid = {THE_SID} + _G.calls = 0 + local rid = pmacs.lsp.send_request(sid, "test/ping", {{ v = 1 }}) + pmacs.lsp.on_response(sid, rid, function(result, err) + _G.calls = _G.calls + 1 + error("handler raises after being removed") + end) + "# + ), + ); + settle(&mut state); + assert_eq!( + eval::(&state, "return _G.calls"), + 1, + "the one-shot fires exactly once for its reply" + ); + + exec(&state, &format!("pmacs.lsp.stop({THE_SID})")); + settle(&mut state); + assert_eq!( + eval::(&state, "return _G.calls"), + 1, + "a delivered one-shot must not be re-invoked by the purge — \ + removal is unconditional, not gated on a clean return" + ); +} + +#[test] +fn acc32_response_carries_the_servers_result() { + let fx = Fixture::new(); + let mut state = editor(); + attached_rust(&mut state, &fx); + exec( + &state, + &format!( + r#" + local sid = {THE_SID} + _G.echoed = nil + _G.saw_err = "unset" + local rid = pmacs.lsp.send_request(sid, "test/ping", {{ v = 42 }}) + pmacs.lsp.on_response(sid, rid, function(result, err) + _G.echoed = result and result.echo and result.echo.v + _G.saw_err = tostring(err) + end) + "# + ), + ); + settle(&mut state); + + // Non-vacuity: without this the seam could "fire" with nil payloads + // and every count-based assertion above would still pass. + assert_eq!( + eval::(&state, "return _G.echoed or -1"), + 42, + "the handler receives the server's result payload" + ); + assert_eq!( + eval::(&state, "return _G.saw_err"), + "nil", + "a successful reply passes nil for err" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 34 — the pending purge, driven off `pmacs.lsp.list()` and +// NOT off a death event seen in the drain. +// +// The second test is the load-bearing one. `handle_server_requests` +// builds its sid list from `attachments`, so a server that is in no +// attachment is never drained — and its `stopped` event is therefore +// never seen. A purge wired to that event leaks exactly there. +// --------------------------------------------------------------------------- + +#[test] +fn acc34_purge_settles_a_pending_one_shot_when_the_server_dies() { + let fx = Fixture::new(); + let mut state = editor(); + attached_rust(&mut state, &fx); + exec( + &state, + &format!( + r#" + local sid = {THE_SID} + _G.err_msg = "never called" + -- A method the fake server answers only after a delay would + -- be ideal; instead the server is stopped in the same breath, + -- so the reply can never arrive. + local rid = pmacs.lsp.send_request(sid, "test/slow", {{}}) + pmacs.lsp.on_response(sid, rid, function(result, err) + _G.err_msg = tostring(err and err.message) + end) + pmacs.lsp.stop(sid) + "# + ), + ); + settle(&mut state); + + let msg: String = eval(&state, "return _G.err_msg"); + assert!( + msg.contains("server gone") || msg == "nil", + "a pending one-shot must be settled, not left waiting; saw {msg:?}" + ); + assert_ne!( + msg, "never called", + "the one-shot was never settled — it leaked" + ); +} + +#[test] +fn acc34_purge_reaches_a_server_that_is_in_no_attachment() { + let fx = Fixture::new(); + let mut state = editor(); + fx.bind(&state); + // Spawned directly, never attached to a buffer. `attachments` is + // empty, so `handle_server_requests` never visits this sid and its + // `stopped` event is never drained. + exec( + &state, + &format!( + r#" + _G.settled = "never called" + local sid = pmacs.lsp.spawn({{ + label = "orphan", + language_id = "rust", + command = "{}", + args = {{}}, + }}) + _G.orphan = sid + "#, + fake_lsp_path() + ), + ); + settle(&mut state); + + exec( + &state, + r#" + local rid = pmacs.lsp.send_request(_G.orphan, "test/slow", {}) + pmacs.lsp.on_response(_G.orphan, rid, function(result, err) + _G.settled = tostring(err and err.message) + end) + pmacs.lsp.stop(_G.orphan) + "#, + ); + settle(&mut state); + + let settled: String = eval(&state, "return _G.settled"); + assert_ne!( + settled, "never called", + "the purge must not depend on the drain reaching this server — \ + it is in no attachment, so the drain never does" + ); + assert!( + settled.contains("server gone"), + "settled with the purge's error; saw {settled:?}" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 34a — `pmacs.fs.canonicalize` (Q#LN20). +// --------------------------------------------------------------------------- + +#[test] +#[cfg(unix)] +fn acc34a_canonicalize_resolves_symlinks_and_dot_segments() { + let fx = Fixture::new(); + fx.write("pkg/sub/a.txt", "x\n"); + // Built here rather than assumed: the whole point is the symlink. + std::os::unix::fs::symlink(fx.dir("pkg"), fx.dir("linkpkg")).unwrap(); + let state = editor(); + + let noncanon = format!("{}/sub/./../sub/a.txt", fx.dir("linkpkg").display()); + let got: String = eval( + &state, + &format!("return tostring(pmacs.fs.canonicalize(\"{noncanon}\"))"), + ); + let want = fx.root.join("pkg/sub/a.txt").display().to_string(); + assert_eq!(got, want, "symlink and dot segments both resolved"); + + // Falsification for 34b: the uncanonicalized spelling really is + // different, so the affinity test below is not vacuous. + assert_ne!(noncanon, want); +} + +#[test] +fn acc34a_canonicalize_returns_nil_for_a_missing_path() { + let fx = Fixture::new(); + let state = editor(); + let missing = fx.dir("nope/not-here").display().to_string(); + let got: String = eval( + &state, + &format!("return tostring(pmacs.fs.canonicalize(\"{missing}\"))"), + ); + assert_eq!( + got, "nil", + "a nonexistent path declines rather than raising" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 34b — affinity survives a symlinked open. +// +// Asserted at the affinity layer, not just at the binding: the +// regression Q#LN20 exists to prevent is *two servers for one project*, +// and only this shape observes it. +// --------------------------------------------------------------------------- + +fn server_count(state: &EditorState) -> i64 { + eval(state, "return #pmacs.lsp.list()") +} + +#[test] +#[cfg(unix)] +fn acc34b_canonicalizing_resolver_reuses_one_server_across_a_symlink() { + let fx = Fixture::new(); + fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n"); + let real = fx.write("proj/src/main.rs", "fn main() {}\n"); + std::os::unix::fs::symlink(fx.dir("proj"), fx.dir("linkproj")).unwrap(); + let linked = fx.dir("linkproj").join("src/main.rs"); + + let mut state = editor(); + fx.bind(&state); + exec( + &state, + &format!( + r#" + pmacs.lsp.config.rust = {{ + command = "{}", + root = function(path) + local dir = path:match("^(.*)/[^/]*$") + if not dir then return nil end + -- Walk up to the directory holding Cargo.toml, then + -- canonicalize — the Q#LN8 shape Stage 3b will use. + while dir and #dir > 0 do + local f = io.open(dir .. "/Cargo.toml", "r") + if f then + f:close() + return pmacs.fs.canonicalize(dir) + end + dir = dir:match("^(.*)/[^/]*$") + end + return nil + end, + }} + "#, + fake_lsp_path() + ), + ); + + open(&state, &real); + settle(&mut state); + assert_eq!(server_count(&state), 1, "the real path spawns one server"); + + open(&state, &linked); + settle(&mut state); + assert_eq!( + server_count(&state), + 1, + "the symlinked path must reuse the same server — two here is the \ + exact regression Q#LN20 exists to prevent" + ); +} + +#[test] +#[cfg(unix)] +fn acc34b_falsified_by_a_resolver_that_skips_canonicalization() { + let fx = Fixture::new(); + fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n"); + let real = fx.write("proj/src/main.rs", "fn main() {}\n"); + std::os::unix::fs::symlink(fx.dir("proj"), fx.dir("linkproj")).unwrap(); + let linked = fx.dir("linkproj").join("src/main.rs"); + + let mut state = editor(); + fx.bind(&state); + // Same resolver, minus the canonicalize call. This is the bite: if + // it also produced one server, the test above would be vacuous and + // `pmacs.fs.canonicalize` would be doing nothing. + exec( + &state, + &format!( + r#" + pmacs.lsp.config.rust = {{ + command = "{}", + root = function(path) + local dir = path:match("^(.*)/[^/]*$") + while dir and #dir > 0 do + local f = io.open(dir .. "/Cargo.toml", "r") + if f then f:close() return dir end + dir = dir:match("^(.*)/[^/]*$") + end + return nil + end, + }} + "#, + fake_lsp_path() + ), + ); + + open(&state, &real); + settle(&mut state); + open(&state, &linked); + settle(&mut state); + assert_eq!( + server_count(&state), + 2, + "without canonicalization the two spellings key differently and \ + spawn two servers — this is what 34b's positive case rules out" + ); +} + +// --------------------------------------------------------------------------- +// Acceptance 34a, non-UTF-8 arm — an unrepresentable resolution declines +// rather than returning a lossy string. +// +// Review finding on PR #167: `display().to_string()` substitutes U+FFFD, +// which would hand back a path that does not exist on disk. That is +// strictly worse than nil here, because the value becomes a +// server-affinity key via `file_uri_for` and would silently fail to +// round-trip. Bites against the `display()` form, which returns a +// non-nil string for this fixture. +// +// **Linux-gated, and `cfg(unix)` was not enough** — CI caught that. +// APFS enforces valid UTF-8 in filenames, so on macOS the `write` below +// fails with EILSEQ ("Illegal byte sequence") before the code under test +// is ever reached: the fixture cannot be built there. That is a +// filesystem refusing to represent the case, not a behavioral +// difference — the subject itself, `to_str()` returning None, is +// platform-independent Rust. Gated explicitly rather than skipped at +// runtime, so a future failure here is a real failure and not a silent +// no-op. +// --------------------------------------------------------------------------- + +#[test] +#[cfg(target_os = "linux")] +fn acc34a_canonicalize_declines_a_non_utf8_resolution() { + use std::ffi::OsStr; + use std::os::unix::ffi::OsStrExt as _; + + let fx = Fixture::new(); + // 0xFF is not valid UTF-8 in any position. + let raw = OsStr::from_bytes(b"bad-\xffname"); + let target = fx.root.join(raw); + std::fs::write(&target, "x\n").unwrap(); + // Reached through an ASCII symlink, so the *input* is representable + // and only the resolved output is not — which is the case + // `to_str()` has to catch and a UTF-8-only input check would miss. + let link = fx.dir("ascii-link"); + std::os::unix::fs::symlink(&target, &link).unwrap(); + + let state = editor(); + let got: String = eval( + &state, + &format!( + "return tostring(pmacs.fs.canonicalize(\"{}\"))", + lua_str(&link) + ), + ); + assert_eq!( + got, "nil", + "a resolution that lands on non-UTF-8 bytes must decline, not \ + return a U+FFFD-substituted path that exists nowhere" + ); +}