diff --git a/builtin/runtime/lean.lua b/builtin/runtime/lean.lua index 5f74792..8f3b339 100644 --- a/builtin/runtime/lean.lua +++ b/builtin/runtime/lean.lua @@ -127,10 +127,28 @@ local probe = { proc = nil, -- process id of the running probe out = "", -- accumulated probe stdout buf_key = nil, -- tostring() of the buffer that started this - watching = nil, -- sid we are waiting to see fail before initialize + watching = nil, -- sid still being polled for die-before-initialize + primary = nil, -- sid the probe's verdict applies to; NOT cleared + -- when the server initializes, because a late + -- version verdict still has to retire it + armed = false, -- the target buffer + primary have been captured saw_initialized = false, } +-- The command as configured, for status text. Hardcoding "lake serve" +-- was untruthful the moment the failure latch became command-agnostic: +-- a user whose `my-lean-wrapper` failed was told `lake serve` did. +local function configured_command() + local cfg = pmacs.lsp.config.lean4 + local cmd = cfg and cfg.command + if not cmd then return "the Lean server" end + local args = cfg.args or {} + if #args > 0 then + return "`" .. tostring(cmd) .. " " .. table.concat(args, " ") .. "`" + end + return "`" .. tostring(cmd) .. "`" +end + local function report(msg) -- COHERENCE §1.2: background work must leave an attributed trace. -- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error` @@ -327,9 +345,19 @@ local function drain_probe() -- case, and covers it better. The probe answers only the ONE -- question failure detection would otherwise answer slowly: an -- old-but-working lake that starts a useless server. + -- **`probe.primary`, NOT `probe.watching`.** `watching` is + -- failure-polling state and is cleared the moment the server + -- initializes. A slow `--version` that lands after a successful + -- initialize would then arrive with nil, and `fire_latch(nil)` + -- retires nothing: `_attach_buffer` finds the still-live primary + -- attachment, early-returns it, and the retry calls that success. + -- Status and config would say "fell back" while the buffer stayed + -- on the old server — the same silent no-op as round 1, reached + -- through a different event ordering. Initializing must stop the + -- failure poll, not erase the server the verdict has to retire. if ev.kind == "exited" and ev.code == 0 and version_below_3_1(probe.out) then - fire_latch(probe.watching, "lake is older than 3.1.0") + fire_latch(probe.primary, "lake is older than 3.1.0") end end end @@ -393,18 +421,20 @@ local function poll_latch() if tostring(info.id) == skey then local kind = info.state and info.state.kind if kind == "initialized" then + -- Stop polling for failure; `probe.primary` deliberately + -- survives, because a later version verdict still needs it. probe.saw_initialized = true probe.watching = nil return end if kind == "crashed" or kind == "stopped" then - fire_latch(sid, "`lake serve` failed to start") + fire_latch(sid, configured_command() .. " failed to start") end return end end -- Gone from the manager entirely without ever initializing. - fire_latch(nil, "`lake serve` failed to start") + fire_latch(nil, configured_command() .. " failed to start") end -- Q#LN16 — `textDocument/waitForDiagnostics` -------------------------- @@ -488,11 +518,6 @@ pmacs.hook.add("buffer.after-load", function() local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf) if not ok_lang or lang ~= "lean4" then return end - -- The buffer that started this, remembered for the asynchronous - -- rebuild: `_attach_buffer` acts on whatever is active when the - -- verdict lands, which may be a different buffer entirely. - probe.buf_key = tostring(buf) - if not probe.started then local path = pmacs.editor.file_path() start_probe(path and M.root_for(path) or nil) @@ -500,9 +525,18 @@ pmacs.hook.add("buffer.after-load", function() local rec = pmacs.lsp.active_attachment() if rec and rec.language == "lean4" then - -- Watch only the FIRST Lean server: the latch is per session. - if not probe.latched and not probe.saw_initialized - and probe.watching == nil then + -- **Arm ONCE, capturing buffer and server together.** Setting + -- `buf_key` on every Lean load meant a second Lean buffer opened + -- before the verdict silently became the rebuild target while the + -- latch still watched the FIRST buffer's server — so the rebuild + -- either repaired the wrong buffer or accepted the second buffer's + -- unrelated live server as success, stranding the first. The pair + -- (target buffer, primary server) is one fact and is captured as + -- one. + if not probe.armed and not probe.latched and not probe.saw_initialized then + probe.armed = true + probe.buf_key = tostring(buf) + probe.primary = rec.server probe.watching = rec.server end return @@ -522,7 +556,13 @@ pmacs.hook.add("buffer.after-load", function() -- already swallowed upstream. That is not something to wait for; it -- is the failure itself, and the only place it is still observable. if not probe.latched then - fire_latch(nil, "`" .. tostring(cfg.command) .. "` could not be started") + -- No server was ever created, so there is no primary to retire — + -- but the rebuild still needs a target buffer. + if not probe.armed then + probe.armed = true + probe.buf_key = tostring(buf) + end + fire_latch(nil, configured_command() .. " could not be started") end end) diff --git a/docs/active-work.md b/docs/active-work.md index 4a650da..6cdac4f 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -265,7 +265,7 @@ If it does not, stop and repair the remote/fetch configuration. - Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`, a `leanprogress` mode plus `waitForDiagnostics` validation on - `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (25 tests). + `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (28 tests). No protocol change. - **Stage 1's acceptance 12 is half superseded and was rewritten, not deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a @@ -279,12 +279,70 @@ If it does not, stop and repair the remote/fetch configuration. an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, not content). Discriminator is `read`'s SECOND return; decline only on a non-nil err. Probed on LuaJIT 2.1. -- Seven bites recorded, each against the committed tree: bare `io.open` - → 24a fails / 24b passes; require-non-nil → 24b fails / 24a passes; - no canonicalization → symlinked open spawns two servers; no re-attach - after the swap → three latch tests fail; hook keyed on the attachment - → the missing-`lake` case fails; `waitForDiagnostics` without - `version` → acc37 fails with the server's InvalidParams. +- **Fifteen bites recorded, each against the committed tree.** R1: bare + `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a + passes; no canonicalization → symlinked open spawns two servers; no + re-attach after the swap → three latch tests fail; hook keyed on the + attachment → the missing-`lake` case fails; `waitForDiagnostics` + without `version` → acc37 fails with InvalidParams. R2: skip retiring + a terminal server → `attempt` reaches 3; no originating-buffer gate → + the Lean buffer is left on the `lake` stub; retry-forever → the + failing-fallback test fails; version-probe any command → the + working-wrapper test fails; no disabled guard → the unconfigured test + sees "`nil` could not be started". R3: verdict keyed on `watching` → + the late-verdict test finds the buffer still on `lake`; `buf_key` + rewritten per load → the second-buffer test fails; hardcoded + `lake serve` → the wrapper-naming test fails. +- **Round-2 review: three more P1 lifecycle defects, suite 20/20 with + all of them live.** (1) The crashed primary respawned forever — + skipping the retire call avoided corrupting terminal servers but left + `next_restart_at` armed. **`forget` is the call for a TERMINAL server** + (it requires terminal state and removes the client, dropping the + restart timer); `stop` is for a live one and corrupts a terminal one. + (2) Re-attachment targeted whatever buffer was active when the async + verdict landed; an unrelated Rust attachment satisfied "a different + server id". (3) A failing fallback retried every tick forever, silent. + Plus two P2s: the Lake version parser was applied to arbitrary wrapper + output, and an UNCONFIGURED `config.lean4` was reported as failure and + latched, poisoning the session. +- **Round-3 review: two more P1s, both asynchronous correlation, suite + 25/25.** (a) `probe.watching` is cleared when the server initializes, + so a SLOW version verdict arrived with nil and retired nothing — + `_attach_buffer` returned the still-live primary and the retry called + it success, so status and config said "fell back" while the buffer + stayed put. **That is the round-1 silent no-op reached through a third + event ordering.** `probe.primary` is now separate from + `probe.watching` and survives initialization. (b) `buf_key` was + rewritten on every Lean `after-load`, so a second Lean buffer opened + before the verdict became the rebuild target while the latch still + watched the first buffer's server. Target buffer and primary server + are one fact and are now armed together, once. Plus a P2: the failure + message hardcoded `lake serve` after the latch became + command-agnostic, sending wrapper users to debug the wrong binary. +- **DURABLE LESSON — "the test that passes" vs "the test that + discriminates."** Six tests across three rounds were written, run + green, and only bite-testing showed they pinned nothing. **Carry this + to `docs/agent-handoff.md` when the lane lands.** The concrete shapes, + all from this branch: + 1. R1 acceptance 36 asserted "every server is terminal" — pinning the + ABSENCE of the fallback it claimed to test. + 2. "No live non-fallback server" misses a respawn loop: a respawning + server sits in `crashed` most of the time. `attempt` counts + respawns; liveness does not. + 3. Returning to a buffer via `find_or_open` re-fires + `buffer.after-load`, which repairs the attachment regardless of the + code under test. Use `switch_buffer`. + 4. A MISSING executable fails synchronously inside `after-load`, where + the rebuild happens inline — no async race can occur. Only the + probe path exercises asynchronous ordering. + 5. A mutation that RAISES (indexing a nil config) is swallowed by the + hook's pcall, so the bite "passes" for the wrong reason. A bite must + reproduce the original shape, not merely break the code. + 6. A fixture whose `serve` sleeps can never let the primary initialize + first, so it cannot reach the ordering where a late verdict must + retire a LIVE server. + Rule: **a test is not evidence until the mutation it targets has been + shown to fail it.** - **SUBSTRATE BUG FOUND, not fixed here (framing §6).** `LspManager::stop` on an ALREADY-terminal server takes its not-initialized branch, terminates the dead process and sets @@ -294,7 +352,9 @@ If it does not, stop and repair the remote/fetch configuration. `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so `attach_buffer` never rebuilds, and `forget` refuses it for not being terminal. **Stopping a dead server is what makes it un-replaceable.** - Lean works around it by checking the state before stopping. + Lean works around it by dispatching on state: `forget` when + terminal, `stop` when live. Merely SKIPPING the call is not + enough — that leaves `next_restart_at` armed. - Round-1 review found four P1s, all real: the latch swapped the config but never spawned or re-attached (and acc36 *asserted every server was terminal*, pinning the absence of the fallback); a missing `lake` @@ -308,9 +368,9 @@ If it does not, stop and repair the remote/fetch configuration. server-failure latch covers the rest. - Verification on this branch: `cargo fmt --check` clean; strict workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; - lean4 server 25/25; lean4 stage 1 9/9; dispatch seams 15/15; + lean4 server 28/28; lean4 stage 1 9/9; dispatch seams 15/15; multi-root 13/13; M4 121; required GPU 155; **isolated-config - workspace sweep 3,214 across 94 suites, zero failures**; + workspace sweep 3,217 across 94 suites, zero failures**; `git diff --check` clean. (Round 1 of this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the fixes were pushed. The ledger's protocol is that verification diff --git a/tests/lean4_server_acceptance.rs b/tests/lean4_server_acceptance.rs index cba8792..db708f1 100644 --- a/tests/lean4_server_acceptance.rs +++ b/tests/lean4_server_acceptance.rs @@ -1069,3 +1069,174 @@ fn r2_an_unconfigured_lean_server_is_disabled_not_failed() { "and the session is not poisoned: a later config must still work" ); } + +// --------------------------------------------------------------------------- +// Round-3 review findings — asynchronous correlation. +// +// Both fail against 3377db0, where the suite was 25/25. +// --------------------------------------------------------------------------- + +impl Fixture { + /// A `lake` whose `serve` really works (it execs the fake LSP) but + /// whose `--version` answers slowly with an old version. This is the + /// ordering the previous fixtures could not produce: the primary + /// INITIALIZES before the version verdict arrives. + fn slow_version_lake(&self, rel: &str, server: &str, version_line: &str) -> PathBuf { + use std::os::unix::fs::PermissionsExt as _; + let path = self.root.join(rel); + std::fs::create_dir_all(path.parent().unwrap()).unwrap(); + std::fs::write( + &path, + format!( + "#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n sleep 0.6\n echo '{version_line}'\n exit 0\nfi\nexec '{server}'\n" + ), + ) + .unwrap(); + std::fs::set_permissions(&path, std::fs::Permissions::from_mode(0o755)).unwrap(); + path + } +} + +/// The command backing the active buffer's attached server. +fn attached_command(state: &EditorState) -> String { + eval( + state, + r#" + local rec = pmacs.lsp.active_attachment() + if not rec then return "none" end + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) == tostring(rec.server) then + return tostring(s.command) + end + end + return "gone" + "#, + ) +} + +#[test] +fn r3_a_late_version_verdict_still_retires_an_initialized_primary() { + // `probe.watching` is cleared the moment the server initializes. A + // verdict arriving after that used to call `fire_latch(nil)`, which + // retires nothing — `_attach_buffer` then returns the still-live + // primary and the retry calls it success. Status and config would + // say "fell back" while the buffer stayed put. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let lake = fx.slow_version_lake("bin/lake", &fake_lsp_path(), "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &file); + // Let the primary initialize first — the ordering that matters. + tick_for(&mut state, 300); + assert_eq!( + attached_state(&state), + "initialized", + "precondition: the primary really did come up before the verdict" + ); + assert_eq!( + attached_command(&state), + lake.display().to_string(), + "precondition: and the buffer is on it" + ); + + // Now let the slow `--version` land and the fallback complete. + tick_for(&mut state, 1200); + + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "a late version verdict must actually move the buffer to the \ + fallback, not just rewrite the config and claim it did" + ); + // And the retired primary is not left running or respawning. + let stale: i64 = eval( + &state, + r#" + local rec = pmacs.lsp.active_attachment() + local live = rec and tostring(rec.server) or "" + local n = 0 + for _, s in ipairs(pmacs.lsp.list()) do + if tostring(s.id) ~= live then + local k = s.state and s.state.kind + if k ~= "stopped" and k ~= "crashed" then n = n + 1 end + end + end + return n + "#, + ); + assert_eq!(stale, 0, "the initialized primary was retired, not left up"); +} + +#[test] +fn r3_a_second_lean_buffer_does_not_steal_the_rebuild_target() { + // `buf_key` was written on every Lean `buffer.after-load`, so a + // second Lean file opened before the verdict became the rebuild + // target while the latch still watched the FIRST buffer's server. + // + // Both files live in the SAME Lake package, so they share one server + // and one root — which is what makes the mis-targeting observable as + // a stranded buffer rather than as two independent servers. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let first = fx.write("pkg/A.lean", "def a := 1\n"); + let second = fx.write("pkg/B.lean", "def b := 2\n"); + let lake = fx.lake_stub("bin/lake", "Lake version 3.0.0"); + let mut state = editor(&fx); + with_fallback(&state, &lake); + + open(&state, &first); + exec(&state, "_G.first_buf = pmacs.window.buffer()"); + // A second Lean buffer, opened before the probe's verdict lands. + open(&state, &second); + tick_for(&mut state, 500); + + // The armed target must still be the FIRST buffer. + let target_is_first: bool = eval( + &state, + "return pmacs.lean._probe.buf_key == tostring(_G.first_buf)", + ); + assert!( + target_is_first, + "the rebuild target is captured once, when the latch arms — a \ + later Lean buffer must not silently become the target" + ); + + // And the first buffer really does end up on the fallback. + exec(&state, "pmacs.window.switch_buffer(_G.first_buf)"); + tick_for(&mut state, 600); + assert_eq!( + attached_command(&state), + fake_lsp_path(), + "the originating buffer is the one repaired" + ); +} + +#[test] +fn r3_a_failing_wrapper_is_named_truthfully_not_as_lake_serve() { + // The failure latch is command-agnostic, so its message must be too. + // Telling a user that `lake serve` failed when they configured + // `my-lean-wrapper` sends them to debug the wrong thing. + let fx = Fixture::new(); + fx.toolchain("pkg", "v4.9.0\n"); + let file = fx.write("pkg/A.lean", "def a := 1\n"); + let absent = fx.dir("bin/my-lean-wrapper"); + let mut state = editor(&fx); + with_fallback(&state, &absent); + + open(&state, &file); + settle(&mut state); + + let status = state.core.borrow().status.clone(); + assert!( + status.contains("my-lean-wrapper"), + "the status names the command the user actually configured; saw \ + {status:?}" + ); + assert!( + !status.contains("lake serve"), + "and does not attribute the failure to `lake serve`; saw {status:?}" + ); +}