Merge pull request #170 from levineuwirth/lean4-stage3b-server

feat(lean): the Lean 4 language server (Arc 8 Stage 3b)

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 `<pkg>/.lake/packages/dep/Foo.lean`
+-- belongs to `<pkg>`'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

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
+  local kind = server_state_kind(sid)
-  for _, info in ipairs(pmacs.lsp.list()) do
+  return kind ~= nil and kind ~= "crashed" and kind ~= "stopped"
-    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
 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

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) — Stages 1+2 MERGED; Stage 3a IN REVIEW
+## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED
 
 - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
   round, all twelve checks green). Branch `githubsucks/lean4-stage1`
@@ -253,6 +253,216 @@ If it does not, stop and repair the remote/fetch configuration.
      `#[cfg(unix)]` is NOT sufficient for such a fixture —
      `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn.
 
+### Stage 3b — the Lean language server (branch `lean4-stage3b-server`)
+
+- Same worktree `../pmacs-lean-stage3`, **branched off
+  `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response
+  seam and `pmacs.fs.canonicalize`, so it is strictly sequential.
+  **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

docs/lean4-mode-framing.md

@@ -1543,6 +1543,24 @@ What remains deferred:
   which events may be dropped, which is a policy question with
   user-visible consequences for diagnostics and progress; Stage 3a states
   the seam's contract around the behavior rather than changing it.
+- **`LspManager::stop` on an already-terminal server strands it.** The
+  not-initialized branch terminates the (already-dead) process and sets
+  `ShuttingDown { shutdown_request_id: None }` on the premise that "the
+  next exit observation cleans up" — but for a `Crashed` client the exit
+  has already been observed, which is what produced that state. No
+  further event arrives, so the client sits in `ShuttingDown`
+  permanently: `server_is_live` counts it as live (neither crashed nor
+  stopped), so `attach_buffer` never rebuilds against it, and
+  `LspManager::forget` refuses it for not being terminal. **Stopping a
+  dead server is what makes it un-replaceable.** Found implementing
+  Stage 3b's latch, which works around it by 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
@@ -1722,9 +1740,13 @@ the blast radius.
   channel a user can actually observe; a report added through
   `pmacs.error` alone must fail this.
 - **37.** `textDocument/waitForDiagnostics` resolves through the response seam
-  (Q#LN16). **PATH-and-success-gated live smoke:** if `lake serve`
+  (Q#LN16), **carrying both `uri` and `version`** — Lean's
-  starts successfully a real elaboration completes and diagnostics
+  `WaitForDiagnosticsParams` requires the document version, and a fake
-  arrive; skipped otherwise, never failed.
+  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

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!({

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

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() {
+fn acc12_opening_lean_spawns_no_process_without_a_server_config() {
-    // Stage 1 is grammar + Lua tables only. Opening a Lean file must not
+    // **Superseded in half by Stage 3b.** This criterion originally also
-    // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and
+    // asserted `pmacs.lsp.config.lean4 == nil`, guarding against a Stage-3
-    // even then it is fallible by design (Q#LN7).
+    // 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.
+    // Constructing an editor touches no process, even though the Lean
-    // The shared `editor()` helper wipes `pmacs.lsp.config` before any
+    // config now exists and names `lake`.
-    // 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.
     let pristine = EditorState::new();
-    let no_lean_config: bool = eval(&pristine, "return pmacs.lsp.config.lean4 == nil");
+    let at_init: i64 = eval(&pristine, "return #pmacs.process.list()");
-    assert!(
+    assert_eq!(
-        no_lean_config,
+        at_init, 0,
-        "Stage 1 defines no `pmacs.lsp.config.lean4`; the LSP is Stage 3"
+        "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,
+        names_lake,
-        "the config table is populated, so the lean4 absence above is meaningful"
+        "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
+    // And opening a Lean buffer with no server configured spawns nothing —
-    // value under the wiped config: a direct probe spawn from `lean.lua`
+    // the `editor()` helper wipes `pmacs.lsp.config`, so this catches a
-    // would show up here whatever `pmacs.lsp.config` contains.
+    // 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"
+    );
 }