Merge remote-tracking branch 'githubsucks/main' into terminal-copy-mode
This commit is contained in:
commit
b9fbb42dc0
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
`<tmp>/linkpkg/sub/./../sub/a.lean`, where `linkpkg` symlinks to
|
||||
`pkg`, yields `<tmp>/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 = <number>, 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
|
||||
`<pkg>/.lake/packages/dep/…` whose ancestor chain contains two
|
||||
`lean-toolchain` files resolves to `<pkg>`, 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
|
||||
`<pkg>/.lake/packages/dep/…` whose ancestor chain contains two
|
||||
`lean-toolchain` files resolves to `<pkg>`, 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.
|
||||
|
|
|
|||
|
|
@ -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!({
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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()?;
|
||||
|
||||
{
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -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"
|
||||
);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<T: mlua::FromLuaMulti>(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::<i64>(&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::<i64>(&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::<i64>(&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::<i64>(&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::<i64>(&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::<i64>(&state, "return _G.echoed or -1"),
|
||||
42,
|
||||
"the handler receives the server's result payload"
|
||||
);
|
||||
assert_eq!(
|
||||
eval::<String>(&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"
|
||||
);
|
||||
}
|
||||
Loading…
Reference in New Issue