Two review findings, both revision edits.
**Q#LN8's marker test was wrong in the other direction.** Rev 5 fixed
the directory case by reading a byte and requiring a non-nil read — but
an **empty** `lean-toolchain` reads nil at EOF too, so that rule
declines a marker that exists, silently, falling through to
`pmacs.project.detect`. 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)`, declining only on a non-nil `err`. The
rule needs no per-platform re-probe: both directory behaviors are
declines, since a platform whose `fopen` refuses a directory 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 gains **24b** (an empty `lean-toolchain` marks a root) beside
24a, with the obligation that each be shown to fail against the
implementation satisfying only the other. A suite carrying just one is
satisfied by a resolver silently wrong for the other case — which is
precisely how rev 5's first answer got written.
**Citation sweep.** Round 4 stated the `project_root_for` correction in
§0.1 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` at :1448), which
prompted a sweep of every `file:line` from §2.4 onward. Four more were
stale. All six: `project_root_for` 513 → 592, `ensure_server` 527 → 610,
`handle_server_requests` 1448 → 1549, `take_typed_edit` 12798 → 12827,
`pair.lua` 213 → 229, `compile.lua` 264 → 266. Six others were verified
good and left alone, listed in §0.1 so the next sweep knows what has
already been checked.
Q#LN15's present-tense "the change is small and spans two files" now
reads as past tense with its PR number, since that stage landed. Its
pre-#161 line numbers stay as written — historical record, not
navigation.
Stages 1 and 2 landed (#160, #161). Re-scouting Stage 3 against `main`
@ `46a1b8f` — six merged PRs past the rev-4 snapshot — produced three
findings that change the plan and four that confirm it. Two were
established by running Lua in a fresh `EditorState` rather than by grep,
and are marked *probed* in §0.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 generalization shipped as Stage 2; the other is
Q#LN9's dispatch seams, which modify `handle_server_requests` —
confirmed the only production drain of LSP events, since
`LspManager::take_all_events` has no non-test caller. By the test that
justified splitting Stage 2 out, that is cross-cutting substrate. Stage
3 is now 3a (seams + canonicalizer, no Lean) and 3b (the Lean server),
strictly sequential.
**The Lean resolver could not satisfy the contract Stage 2 documented.**
#161 established that a configured root reaches `file_uri_for` verbatim
and that the resulting URI is the affinity key. Probed:
`pmacs.editor.file_path()` is not canonical — opening
`<tmp>/linkpkg/sub/./../sub/a.lean` through a symlink yields
`<tmp>/linkpkg/sub/a.lean`, lexical collapse only. No canonicalize
binding is exposed to Lua, and `pmacs.project.detect` canonicalizes but
returns nil without a marker. So one Lake package opened by two
spellings would spawn two `lake serve` processes — the bug Stage 2 was
built to prevent, re-entered through Stage 3's door. New Q#LN20 adds a
synchronous `pmacs.fs.canonicalize`; it rides 3a, and it serves every
future function-valued root rather than only Lean's. Two alternatives
are recorded with why they were rejected — the `detect`-anchored walk in
particular is incorrect, not merely inelegant.
**`pmacs.fs.stat` is unusable in the resolver.** It is async and the
resolver runs synchronously inside `ensure_server` ← `attach_buffer` ←
`buffer.after-load`, with no coroutine to await on. Probed: `io` and
`os` are exposed in the sandbox, so the marker walk uses `io.open` — the
opposite of what a reader would assume, hence Q#LN8 now says so. One
edge, also probed: `io.open` succeeds on a directory, so the walk reads
a byte rather than testing for a handle, and acceptance 24a bites the
version that does not.
Confirmed rather than changed: Q#LN7's stop-before-respawn is necessary
(default policy is OnCrash, the termination handler never consults the
exit code, and `maybe_restart` has no attempt ceiling — a broken `lake`
respawns forever; `stop()` setting `restart = Never` is what disarms
it); the response seam works as specified, since `Response` events are
pushed unconditionally and `send_request` returns the keying id.
One confirmation narrowed the design. `handle_server_requests` builds
its sid list from `attachments` and `push_event` is uncapped, so
subscribers fire only for servers with a live attachment. That turns
acceptance 34 into a reachable leak: killing the buffer with a request
outstanding strands the registration behind a drain that no longer runs.
The purge is now driven from both edges and 34 exercises the buffer-kill
path, which is the one a user can reach.
Also: §9 states the lane's coherence impact per COHERENCE §20 (journey
steps, interaction islands, config registry, background attribution),
including the honest note that 3b makes §2's step-3 grade marginally
worse by adding one more instance of the silent-spawn-failure class.
Three items are named in §6 rather than paid: the uncapped event queue,
the dropped `cfg.restart`, and surfacing the spawn failure itself.
Acceptance keeps every rev-4 number. The two split sections are
bulleted with literal labels because a markdown ordered list renumbers
from its first item, and 3b's criteria are non-contiguous; round 3's
finding 4 was stale references surviving a renumber, and not renumbering
is the cheaper way to not repeat it. Stale cross-references from the
split were reconciled in the same pass, and `project_root_for`'s
citation was corrected from 513 to 592 per COHERENCE §25.
The approved framing for Arc 8, revision 4, after three review rounds.
Seven stages: grammar/mode, multi-root LSP affinity, the Lean language
server, the Unicode input method, the goal view, the #eval output
channel, and module hierarchy. 19 decisions, 64 acceptance criteria.
Committed as this branch first commit per the house workflow; the
implementation of Stage 1 follows.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Levi Neuwirth