neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge pull request #167 from levineuwirth/lean4-stage3a-seams 

feat(lsp): notification/response dispatch seams and fs.canonicalize (Arc 8 Stage 3a)
This commit is contained in:
Levi Neuwirth 2026-07-26 13:47:46 +00:00 committed by GitHub
parent cf54270173 7243714b3f
commit 6f348c9285
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
6 changed files with 1591 additions and 102 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
builtin/runtime/fs.lua
View File

@ -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

188
builtin/runtime/lsp.lua
View File

@ -1546,6 +1546,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 +1778,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 +1804,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

66
docs/active-work.md
View File

@ -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; Stage 3a IN REVIEW
- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
round, all twelve checks green). Branch `githubsucks/lean4-stage1`
@ -189,6 +189,70 @@ 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.
## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165)
- Approved framing: `docs/dired-framing.md` **revision 6** — rev 5 is the

643
docs/lean4-mode-framing.md
View File

@ -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,18 @@ 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.
- **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 +1632,109 @@ 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). **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 +1821,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 +1839,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.

48
src/lua_bindings/mod.rs
View File

@ -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()?;
{

724
tests/lsp_dispatch_seams_acceptance.rs Normal file
View File

@ -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"
);
}