diff --git a/docs/active-work.md b/docs/active-work.md index f55627e..5bacaa1 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -54,10 +54,11 @@ git status --short --branch The `git log` command must expose `0dd16a5` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stage 1 IN REVIEW (PR #160) +## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #TBD) -- Portable branch: `githubsucks/lean4-stage1`, worked in the shared - checkout (no sibling worktree), based on `githubsucks/main` @ `e745068`. +- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review + round, all twelve checks green). Branch `githubsucks/lean4-stage1` + retained; it was worked in the shared checkout (no sibling worktree). - Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as the branch's first commit (`a382965`) after three review rounds. **Seven stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star: @@ -113,16 +114,59 @@ If it does not, stop and repair the remote/fetch configuration. 152; **isolated-config workspace sweep 3,150 across 90 suites**; `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` for the reason recorded in the bottom-panel lane below. -- **Stage 2 is multi-root LSP server affinity** — pure substrate, no Lean - content, and it changes `ensure_server`, which every LSP language - shares. It is sequenced next because Lean is the language that makes its - absence a correctness failure rather than an inconvenience. Two - corrections the framing already carries for it: `root` is computed at - `lsp.lua:537`, **after** the reuse loop, so the fix must hoist it; and - `project_root_for` never returns nil for a file with a path, so the - affinity key must be the root only when a root was actually *detected*, - or markerless scratch files fragment into one server per directory for - every language. +### Stage 2 — multi-root LSP server affinity (Q#LN15) + +- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout, + based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not + for Lean: **the diff contains no Lean content**, because `ensure_server` + is the one server-affinity function every LSP language shares and a + cross-cutting change to it must not be reviewable only as a Lean + feature. +- Three files, no protocol change: `src/lua_bindings/mod.rs` (the + `lsp.list()` row builder gains `root_uri` + `cwd`), + `builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`; + `ensure_server` hoists it above the reuse loop and matches on it), + `tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21). +- **The rule that keeps this from regressing every other language: the + affinity key is the root only when a root was actually FOUND.** + `project_root_for` never returns nil for a file with a path — its last + resort is the file's own directory — so a naive `(language_id, root)` + key gives every directory of loose scratch files its own server, for + every language. `source` is `"config" | "detected" | "fallback"` and + only the first two become a key. +- **Wire-identical for the fallback case, and that is provable rather + than hoped.** Matching is on the spawned spec's `root_uri` (nil matching + nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries + the directory and `build_initialize` derives the identical `rootUri` + from `cwd` when the field is None, using a percent-encoder with the same + allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`) + is the **only** reader of `spec.root_uri` in the tree. +- Deliberate behavior change, asserted not discovered: a server + hand-spawned from `init.lua` with only `cwd` set also reads back nil, so + a root-bearing attach will not adopt it. +- `config[language].root` may now be a `function(path) -> string|nil`, + memoized per directory — needed because the hoist puts root resolution + on every attach rather than every spawn. The memo is keyed **weakly by + the resolver function itself**, so replacing `config[lang].root` cannot + serve a root the previous resolver computed. This is Q#LN8's + generalization landing early; the Lean resolver that uses it is Stage 3. +- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`, + 8/9 against the pre-change `mod.rs`, and — the one that matters most — + installing the naive always-key-on-root variant fails acceptance 20 and + 21 exactly as Q#LN15 part 2 predicts. The four that survive the first + bite (13, 15, 16, 19) are the regression pins; passing on both sides is + their job. +- Every fixture sets `pmacs.project.set_search_boundary` at its own + tempdir root. Without it the marker walk climbs to the filesystem root + and a stray `.git` above the temp directory turns the markerless cases + into detected ones — the assertions would still pass while testing + nothing. +- **Found but not fixed here (pre-existing, own lane):** `ensure_server` + never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a + `restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on + the auto-attach path. At least one existing test sets it believing it + takes effect. Out of scope for a PR whose acceptance 16 pins existing + attach behavior as unchanged. ## Bottom-panel lane (window placement + side windows) — Stage 1 IN REVIEW