From 914bf3f02f472774e79792347a23ff190d631e34 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 17:40:31 -0400 Subject: [PATCH] docs: record the Stage 3b lane and its stacking constraint --- docs/active-work.md | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/docs/active-work.md b/docs/active-work.md index aef6edc..99b54ea 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -54,7 +54,7 @@ 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) — Stages 1+2 MERGED; Stage 3a IN REVIEW +## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review round, all twelve checks green). Branch `githubsucks/lean4-stage1` @@ -252,6 +252,43 @@ If it does not, stop and repair the remote/fetch configuration. `#[cfg(unix)]` is NOT sufficient for such a fixture — `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. +### Stage 3b — the Lean language server (branch `lean4-stage3b-server`) + +- Same worktree `../pmacs-lean-stage3`, **branched off + `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response + seam and `pmacs.fs.canonicalize`, so it is strictly sequential and its + PR must be retargeted to `main` only after #167 merges. (Kill-ring + lesson: retarget stacked child PRs BEFORE merging the parent.) +- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in + `src/editor.rs`, a `leanprogress` mode on `pmacs_fake_lsp`, and + `tests/lean4_server_acceptance.rs` (17 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 + Stage-3 front-run; 3b is that stage. What survives is the restraint + half — constructing an editor spawns nothing though the config now + names `lake`, and opening a Lean buffer with no server configured + spawns nothing — which is what holds Q#LN7's "not at init" promise. +- **The marker test is wrong in two opposite directions if done naively** + and both are pinned: `io.open` SUCCEEDS on a directory (so truthiness + accepts a `lean-toolchain` dir), but requiring a non-nil read rejects + 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. +- Four 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 stop + before fallback → acc36 fails. +- The probe's non-zero exit is deliberately NOT a fallback trigger — + §2.9's elan shim makes `lake --version` fail where `lake serve` still + works. Only a parseable version below 3.1.0 triggers it; the + 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 17/17; lean4 stage 1 9/9; dispatch seams 15/15; + multi-root 13/13; M4 121; required GPU 155; **isolated-config + workspace sweep 3,206 across 94 suites, zero failures**; + `git diff --check` clean. + ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next - Approved framing: `docs/dired-framing.md` (revision 5), landing as its