docs(active-work): remove the landed Lean 4 lane
The ledger preamble already says Lean 4's merged lane was removed, and the durable Stage 4b facts already live in the handoff. Remove the stale section that still called Stage 4b in review so PR #182's post-merge state is internally consistent.
This commit is contained in:
parent
d0817314f9
commit
7a3a55de40
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue