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.
Levi Neuwirth
a516a46359