diff --git a/docs/active-work.md b/docs/active-work.md index 6ee50fe..83c3a51 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -178,146 +178,6 @@ If it does not, stop and repair the remote/fetch configuration. to recur; the next occurrence carries its own evidence under whoever's PR, and a Stage B framing follows then. -## Lean 4 lane (Arc 8) — Stages 1–4a MERGED; Stage 4b IN REVIEW - -- **Stages 1, 2, 3a, 3b and 4a are MERGED** — #160 (`main` @ `0827dd1`), - #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`), #179 - (`a27f646`). Their full - histories were pruned from this ledger in round 6, per this file's own - instruction to remove entries when their PR merges; the durable facts - now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where - a fresh machine should read them. `docs/lean4-mode-framing.md` rev 9 - carries the decisions. - -### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`) - -- Framing `docs/lean4-mode-framing.md` **revision 12** (rounds 10, 11 - and 12 = review of the implementation). Stage - 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, - the Lean content that registers on it. -- Footprint: `scripts/regen-lean-abbrev` (new, the generator), - `builtin/runtime/lean_abbrev.lua` (new, VENDORED DATA — 1,855 entries - from `leanprover/vscode-lean4@17d1d08`, Apache-2.0), - `builtin/runtime/lean_input.lua` (new, the consumer at priority 50), - `src/editor.rs` (two `include_str!` blocks), - `tests/lean_input_acceptance.rs` (new, 31 tests), and one - `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` - (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart - from the load sites and that one test. -- **Round 9 corrected three acceptance criteria that the real table - contradicts** — found by simulating the state machine over all 1,855 - entries and re-reading upstream at the pinned commit, not by reading - the prose again. `\to` is NOT eager (`top`, `to0`, `toa` extend it); - `\zzzz` expands to `ζzzz ` because `ze`/`zeta`/`zsqrtd` exist, and - only `$ % , ; @ W` open no key at all; and `\alpha`'s undo does not - restore `\alpha ` because `alpha` IS eager, so the terminator is a - separate edit. Criteria 38, 41 and 42 now state both paths. -- **Two generator bugs, both caught by its own round-trip check - failing closed:** `str.splitlines()` also splits on U+2028/U+2029, - and 53 symbols contain one literally, so the check reported a count - mismatch that was its own bug; then escaping via `chr(byte)` produced - a latin-1-shaped string that `write_text(encoding="utf-8")` - re-encoded, and every non-ASCII symbol landed double-encoded. The - first version of the check compared IN-MEMORY strings and agreed with - itself. **It now stages the file, re-reads the bytes from disk, and - renames into place only on a match.** -- **The point must be placed explicitly after the replace.** The - expansion SHRINKS the buffer (`\alpha` 6 bytes → `α` 2), so a point - left at the pre-edit offset is past the new end and every later - self-insert is silently rejected — the editor looks dead after the - first expansion. Pairing's "no cursor motion on the clean path" does - not generalize: that holds only for an insert AT the cursor. -- **Three tests were vacuous when first written and were found by - biting, not by review:** the abandonment test asserted text that a - wrongly-surviving record would also produce (claiming makes no edit — - it needed the follow-up keystroke that completes an eager key); the - re-arm test used the framing's own `\alpha\to`, which never reaches - the re-arm branch because `alpha` is eager and closes the record - first (`\al\to` does); and both buffer-switch tests passed through - `find_or_open`'s fresh-load path, which fires `buffer.after-load` and - a record-less edit rather than `buffer.after-switch` — deleting the - subscriber left them green. All three now bite. -- **Bite table** (each mutation, and the tests it fails): - - | Mutation | Tests it fails | - |---|---| - | register at priority 150 (after pairing) | 2 | - | claim only completed expansions | 2 | - | longest match instead of shortest | 9 | - | equal-length tie keeps the LATER key | 3 | - | remove the eager branch | 8 | - | expand without the terminator in the span | 2 | - | remove the re-arm branch | 1 | - | remove the point-still-at-span-end check | 1 | - | remove the exact-revision check | 1 | - | leave the point where the replace found it | 5 | - | remove the `lean4` language gate | 1 | - | remove the `lean.abbrev` gate | 2 | - | `buffer.after-switch` clears every frontend | 1 | - | delete the `buffer.after-switch` subscriber | 1 | - | `frontend.detached` purges every frontend | 1 | - | claim the terminator | 1 | - | expand inside the chain, then decline | 2 | - | drop the `cursor() == post_cursor` check | 1 | - | place the point without the context guard | 1 | - | load lean_input.lua after lsp.lua | 1 | - | let a nested fan-out consume the deferred slot | 1 | - | stop counting chain invocations | 1 | - | count fan-outs in the expander instead of the sentinel | 1 | - - Acceptance 45f bit by construction: without a registered window for - the source frontend it ran six fan-outs with a nil record and proved - nothing, because `handle_remote_crdt_op` arms nothing unless the - source's active window displays the buffer. -- **Round 10 (review) found three defects, all about what happens - AROUND the expansion rather than about resolving an abbreviation.** A - pair character that TERMINATES an abbreviation never reached pairing - (`\alp(` gave `α(`): the first revision claimed the terminator, and - merely declining is not enough either, because the chain hands each - consumer a copy of the record made before any consumer ran — so - expanding inside the chain invalidates pairing's copy and the closer - is lost anyway (verified by mutation, not assumed). The expansion now - runs on **its own `buffer.after-edit` subscriber** after the chain, - with a span that stops before the terminator. That is a new instance - of Q#AP7, so it is now pinned with the sighelp fake server. - Post-insert point motion was also mistaken for a valid span (the - relevance check needs `cursor() == post_cursor`, as pairing's has - since #110), and cursor placement could move a buffer an intercept - had switched to. -- **Round 11 found the round-10 fix incomplete in one place: - `buffer.after-edit` fan-outs NEST.** A consumer between the expander - (50) and pairing (100) that calls `pmacs.hook.run("buffer.after-edit")` - re-enters the expander's subscriber while the OUTER chain is still - mid-list; the nested pass expanded and outer pairing then resumed with - an invalidated record — `α(` again, through the chain's documented - re-entrancy seam instead of through claiming. **Deferring work past a - fan-out means owning which fan-out it belongs to.** The chain's - subscriber and the expander's each run exactly once per fan-out, so - counting the first and matching it off in the second identifies the - nesting level with no new seam in merged Stage 4a substrate. -- **Round 12 found round 11's counter in the wrong place.** It counted - invocations of the EXPANDER, which is optional: a lower-priority - consumer can claim and stop the chain before the expander runs, while - that fan-out's deferred subscriber still runs — so the nested pass - went uncounted, looked outermost, expanded early, and outer pairing - resumed with an invalidated record. The count now comes from a no-op - consumer at the MINIMUM priority, which runs first in every chain - invocation that reaches any consumer, and degrades safely: the only - thing that can skip it is a claim ahead of it, which skips the - expander too. A subscriber registered beside `run_deferred` cannot - serve — the whole nested fan-out completes inside the outer chain's - subscriber, before it would run. -- **Rounds 10–12 share a shape worth naming.** Each fix was correct - about the failure it was shown and wrong about the boundary of the - mechanism it leaned on — first the chain's copy semantics, then its - re-entrancy, then its short-circuit. **A queue that outlives the - thing that filled it has to name that thing, not approximate it.** -- Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, - named in the module header (Q#LN21): six source-peer optimistic - inserts replaced by one daemon-peer op. `set_round_trip_input` would - fix it and also disables `dispatch_idle`, so RET would stop inserting - a newline. - ## Journey Stage 1a — PR #182 OPEN, review round 1 closed - Framing `docs/journey-stage1a-framing.md` **rev 8** (four review