fix(typed-edit): close round-8 review on the consumer chain
Five defects in the chain itself, plus the stale handoff state. Each consumer now gets its own shallow copy of the typed-edit record. Handing everyone the same table let a DECLINING consumer rewrite provenance for the ones behind it, and pairing decides what to close from `rec.char` — so a forged `char` turned a typed `x` into `x)`. Every field is a scalar or an opaque id, so a shallow copy is complete. The fan-out iterates a snapshot of the consumer list. It was iterating the same array `add_consumer` mutates: a consumer that registered a lower-priority one shifted itself forward under `ipairs` and ran twice, and re-registering made that unbounded. Registrations and removals made during a fan-out now take effect on the next one, stated as a contract and pinned in both directions. `tostring` on the caught error moved inside the containment. A Lua error may be any value, including a table whose `__tostring` throws — rendering it outside the `pcall` reintroduced exactly the escape the containment exists to prevent. Priorities are validated as finite integers in i32 range, matching `pmacs.completion.register`. NaN is a number and every ordered comparison with it is false, so a NaN consumer landed wherever the insertion scan gave up and silently voided the lowest-first ordering that Q#LN22 depends on. `add_consumer` returns a handle and `remove_consumer` unregisters it, reporting whether it was live. Without teardown the chain inherited the `pmacs.hook.add` callback leak COHERENCE.md §13 already records, and spread it to every consumer. Also corrects the rationale the containment was documented with, in the module, the test, and the framing: an uncontained throw does NOT take the fan-out's other subscribers down. `run_all_must_succeed` (src/hook.rs:332) collects errors and continues, so lsp.lua still flushes didChange. The containment is still required — the throw skips every later consumer in the chain — but the reason is narrower than rev 7 claimed. Criteria 46f (record isolation), 46g (snapshot iteration), and 46h (lifecycle and priority validation) added; 46d's rationale corrected. Four new tests, all bite-verified by mutation, each failing only its target: shared record table (1), live-array iteration (1), unprotected tostring (1), bare number check (1), no-op removal (2). The suite also runs green under `--features lua54`. docs/agent-handoff.md said Stage 4a was awaiting approval while this branch had it implemented and in review. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
This commit is contained in:
parent
c7072b49e9
commit
aef4e98c26
|
|
@ -13,11 +13,12 @@
|
||||||
-- subscriber that reads the record, and offers that one read to
|
-- subscriber that reads the record, and offers that one read to
|
||||||
-- consumers registered through `pmacs.typed_edit.add_consumer`:
|
-- consumers registered through `pmacs.typed_edit.add_consumer`:
|
||||||
--
|
--
|
||||||
-- pmacs.typed_edit.add_consumer {
|
-- local handle = pmacs.typed_edit.add_consumer {
|
||||||
-- name = "auto-pair", -- for error reporting; must be unique-ish
|
-- name = "auto-pair", -- for error reporting
|
||||||
-- priority = 100, -- LOWEST runs FIRST
|
-- priority = 100, -- LOWEST runs FIRST
|
||||||
-- fn = function(rec) ... return claimed end,
|
-- fn = function(rec) ... return claimed end,
|
||||||
-- }
|
-- }
|
||||||
|
-- pmacs.typed_edit.remove_consumer(handle) -- -> true if it was live
|
||||||
--
|
--
|
||||||
-- A consumer returns whether it CLAIMED the edit; the first that claims
|
-- A consumer returns whether it CLAIMED the edit; the first that claims
|
||||||
-- stops the chain. "Claimed" means the chain stops, not that an edit was
|
-- stops the chain. "Claimed" means the chain stops, not that an edit was
|
||||||
|
|
@ -46,10 +47,19 @@ pmacs.typed_edit = pmacs.typed_edit or {}
|
||||||
-- order" is part of the stated contract, not an incidental property.
|
-- order" is part of the stated contract, not an incidental property.
|
||||||
local consumers = {}
|
local consumers = {}
|
||||||
|
|
||||||
-- Register a typed-edit consumer. Argument errors throw: registration
|
-- Handles are opaque to callers; only identity matters. An integer
|
||||||
-- happens at chunk-load or config-load time, where a throw is a visible
|
-- counter is enough because nothing ever reuses one.
|
||||||
-- startup failure rather than a silently missing feature. Nothing in
|
local next_handle = 0
|
||||||
-- the after-edit path throws --- see the fan-out below.
|
|
||||||
|
-- `math.huge` is the only portable spelling of infinity available in
|
||||||
|
-- both LuaJIT and 5.4, and NaN is the only value not equal to itself.
|
||||||
|
local INT32_MIN, INT32_MAX = -2147483648, 2147483647
|
||||||
|
|
||||||
|
-- Register a typed-edit consumer; returns an opaque handle for
|
||||||
|
-- `remove_consumer`. Argument errors throw: registration happens at
|
||||||
|
-- chunk-load or config-load time, where a throw is a visible startup
|
||||||
|
-- failure rather than a silently missing feature. Nothing in the
|
||||||
|
-- after-edit path throws --- see the fan-out below.
|
||||||
function pmacs.typed_edit.add_consumer(spec)
|
function pmacs.typed_edit.add_consumer(spec)
|
||||||
if type(spec) ~= "table" then
|
if type(spec) ~= "table" then
|
||||||
error("pmacs.typed_edit.add_consumer: spec must be a table", 2)
|
error("pmacs.typed_edit.add_consumer: spec must be a table", 2)
|
||||||
|
|
@ -58,9 +68,18 @@ function pmacs.typed_edit.add_consumer(spec)
|
||||||
if type(name) ~= "string" or name == "" then
|
if type(name) ~= "string" or name == "" then
|
||||||
error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2)
|
error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2)
|
||||||
end
|
end
|
||||||
if type(priority) ~= "number" then
|
-- A bare `type(priority) == "number"` admits NaN and the infinities,
|
||||||
|
-- and EVERY ordered comparison against NaN is false --- so a NaN
|
||||||
|
-- consumer silently lands wherever the insertion scan happens to give
|
||||||
|
-- up, and the lowest-first contract other consumers depend on stops
|
||||||
|
-- holding. Bounded integers match `pmacs.completion.register`, whose
|
||||||
|
-- priority is an i32 on the Rust side.
|
||||||
|
if type(priority) ~= "number" or priority ~= priority
|
||||||
|
or priority == math.huge or priority == -math.huge
|
||||||
|
or priority % 1 ~= 0
|
||||||
|
or priority < INT32_MIN or priority > INT32_MAX then
|
||||||
error("pmacs.typed_edit.add_consumer: " .. name ..
|
error("pmacs.typed_edit.add_consumer: " .. name ..
|
||||||
": priority must be a number", 2)
|
": priority must be a finite integer in [-2147483648, 2147483647]", 2)
|
||||||
end
|
end
|
||||||
if type(fn) ~= "function" then
|
if type(fn) ~= "function" then
|
||||||
error("pmacs.typed_edit.add_consumer: " .. name ..
|
error("pmacs.typed_edit.add_consumer: " .. name ..
|
||||||
|
|
@ -77,7 +96,27 @@ function pmacs.typed_edit.add_consumer(spec)
|
||||||
break
|
break
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
table.insert(consumers, at, { name = name, priority = priority, fn = fn })
|
next_handle = next_handle + 1
|
||||||
|
local handle = next_handle
|
||||||
|
table.insert(consumers, at,
|
||||||
|
{ handle = handle, name = name, priority = priority, fn = fn })
|
||||||
|
return handle
|
||||||
|
end
|
||||||
|
|
||||||
|
-- Unregister a consumer by the handle `add_consumer` returned. Returns
|
||||||
|
-- true if it was registered, false otherwise (so a double-remove is a
|
||||||
|
-- reportable no-op rather than a throw). Without this, re-evaluating a
|
||||||
|
-- config or reloading a package accumulates callbacks permanently ---
|
||||||
|
-- the leak COHERENCE.md §13 already records against `pmacs.hook.add`,
|
||||||
|
-- which this chain would otherwise inherit and spread.
|
||||||
|
function pmacs.typed_edit.remove_consumer(handle)
|
||||||
|
for i, c in ipairs(consumers) do
|
||||||
|
if c.handle == handle then
|
||||||
|
table.remove(consumers, i)
|
||||||
|
return true
|
||||||
|
end
|
||||||
|
end
|
||||||
|
return false
|
||||||
end
|
end
|
||||||
|
|
||||||
pmacs.hook.add("buffer.after-edit", function()
|
pmacs.hook.add("buffer.after-edit", function()
|
||||||
|
|
@ -92,19 +131,51 @@ pmacs.hook.add("buffer.after-edit", function()
|
||||||
-- fan-out on nil would leave both reading stale state.
|
-- fan-out on nil would leave both reading stale state.
|
||||||
local rec = ed.take_typed_edit and ed.take_typed_edit()
|
local rec = ed.take_typed_edit and ed.take_typed_edit()
|
||||||
|
|
||||||
for _, c in ipairs(consumers) do
|
-- Iterate a SNAPSHOT. A consumer may register or remove consumers
|
||||||
-- `buffer.after-edit` is all-must-succeed (builtin/hooks/default.lua):
|
-- while the chain is running, and `table.insert`/`table.remove` on
|
||||||
-- a throwing consumer would fail the fan-out for every OTHER
|
-- the live array shifts indices under `ipairs` --- a consumer that
|
||||||
-- subscriber, including lsp.lua's didChange flush. Contain it,
|
-- registers a lower-priority one shifts itself forward and runs
|
||||||
-- report it, and keep going --- a broken consumer must not be able
|
-- twice, and repeating that is unbounded. Registrations and removals
|
||||||
-- to stop the editor from telling the language server what changed.
|
-- made during a fan-out therefore take effect on the NEXT fan-out.
|
||||||
-- This matches pair.lua's existing never-throw-from-after-edit
|
local snapshot = {}
|
||||||
-- discipline; it does not weaken the hook's contract for anyone
|
for i, c in ipairs(consumers) do
|
||||||
-- else, because the chain itself still never fails.
|
snapshot[i] = c
|
||||||
local ok, claimed = pcall(c.fn, rec)
|
end
|
||||||
|
|
||||||
|
for _, c in ipairs(snapshot) do
|
||||||
|
-- Each consumer gets its OWN copy of the record. The table handed
|
||||||
|
-- out is plain Lua data, so a declining consumer could otherwise
|
||||||
|
-- edit `rec.char` in place and the next consumer would act on the
|
||||||
|
-- forged value --- auto-pairing reads `rec.char` to decide what to
|
||||||
|
-- close, so a rewritten `char` makes it insert a pair the user
|
||||||
|
-- never typed. Every field is a scalar or an opaque id, so a
|
||||||
|
-- shallow copy is a complete snapshot.
|
||||||
|
local mine = nil
|
||||||
|
if rec ~= nil then
|
||||||
|
mine = {}
|
||||||
|
for k, v in pairs(rec) do
|
||||||
|
mine[k] = v
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
-- Contain the consumer. A throw here would skip every LATER
|
||||||
|
-- consumer in the chain and mark the whole `buffer.after-edit` run
|
||||||
|
-- failed; the other subscribers still run, because all-must-succeed
|
||||||
|
-- collects errors and continues (`src/hook.rs`'s
|
||||||
|
-- `run_all_must_succeed`), but one broken consumer must not be able
|
||||||
|
-- to silently disable the ones behind it. This matches pair.lua's
|
||||||
|
-- existing never-throw-from-after-edit discipline.
|
||||||
|
local ok, claimed = pcall(c.fn, mine)
|
||||||
if not ok then
|
if not ok then
|
||||||
ed.set_status("typed-edit consumer '" .. c.name .. "' failed: " ..
|
-- Rendering is itself protected: a Lua error may be any value,
|
||||||
tostring(claimed))
|
-- including a table whose `__tostring` throws, and an escaping
|
||||||
|
-- error here would defeat the containment above.
|
||||||
|
local shown, rendered = pcall(tostring, claimed)
|
||||||
|
if not shown or type(rendered) ~= "string" then
|
||||||
|
rendered = "<unprintable error>"
|
||||||
|
end
|
||||||
|
pcall(ed.set_status,
|
||||||
|
"typed-edit consumer '" .. c.name .. "' failed: " .. rendered)
|
||||||
elseif claimed then
|
elseif claimed then
|
||||||
return
|
return
|
||||||
end
|
end
|
||||||
|
|
|
||||||
|
|
@ -149,9 +149,9 @@ If it does not, stop and repair the remote/fetch configuration.
|
||||||
### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch)
|
### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch)
|
||||||
|
|
||||||
- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua`
|
- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua`
|
||||||
(new, 112 lines), `pair.lua` re-expressed as one consumer,
|
(new), `pair.lua` re-expressed as one consumer,
|
||||||
`src/editor.rs` +15 (the `include_str!` and its ordering comment), and
|
`src/editor.rs` +15 (the `include_str!` and its ordering comment), and
|
||||||
`tests/typed_edit_chain_acceptance.rs` (new, 9 tests).
|
`tests/typed_edit_chain_acceptance.rs` (new, 13 tests).
|
||||||
**`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat
|
**`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat
|
||||||
main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is
|
main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is
|
||||||
criterion 46 checked at the diff, which is the only way it means
|
criterion 46 checked at the diff, which is the only way it means
|
||||||
|
|
@ -166,9 +166,26 @@ If it does not, stop and repair the remote/fetch configuration.
|
||||||
- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and
|
- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and
|
||||||
"ties broken by registration order" is a stated contract.
|
"ties broken by registration order" is a stated contract.
|
||||||
- **The chain `pcall`s each consumer** and reports through
|
- **The chain `pcall`s each consumer** and reports through
|
||||||
`set_status`. `buffer.after-edit` is all-must-succeed, so an
|
`set_status`. Rev 7 justified this by claiming an uncontained throw
|
||||||
uncontained throw fails the fan-out for every other subscriber
|
would fail the fan-out for every other subscriber including lsp.lua's
|
||||||
including lsp.lua's didChange flush.
|
didChange flush; **that is wrong** — `run_all_must_succeed`
|
||||||
|
(`src/hook.rs:332`) collects errors and continues, so the other
|
||||||
|
subscribers still run. The real consequence is narrower and still
|
||||||
|
worth containing: the throw skips every LATER consumer in the chain.
|
||||||
|
The rendering is protected too, because a Lua error may be a table
|
||||||
|
whose `__tostring` throws.
|
||||||
|
- **Round 8 (review) findings, all fixed on this branch:** each consumer
|
||||||
|
now gets its **own shallow copy** of the record (the same table let a
|
||||||
|
declining consumer rewrite `rec.char`, which pairing reads — typing
|
||||||
|
`x` could produce `x)`); the fan-out iterates a **snapshot** (a
|
||||||
|
consumer registering a lower-priority one shifted itself forward under
|
||||||
|
`ipairs` and ran twice, unbounded if repeated); `tostring` moved
|
||||||
|
inside the containment; **non-finite and non-integer priorities are
|
||||||
|
rejected** (NaN is a number and every ordered comparison with it is
|
||||||
|
false, so it landed wherever the insertion scan gave up and silently
|
||||||
|
voided the ordering contract); and `add_consumer` now returns a handle
|
||||||
|
with `remove_consumer` beside it, so re-evaluating a config no longer
|
||||||
|
leaks callbacks the way `pmacs.hook.add` does (COHERENCE §13).
|
||||||
- **Every acceptance test is bite-verified by mutation**, per the
|
- **Every acceptance test is bite-verified by mutation**, per the
|
||||||
standing rule that a test is not evidence until the mutation it
|
standing rule that a test is not evidence until the mutation it
|
||||||
targets has been shown to fail it:
|
targets has been shown to fail it:
|
||||||
|
|
@ -182,6 +199,11 @@ If it does not, stop and repair the remote/fetch configuration.
|
||||||
| drop the `pcall` | 1 chain |
|
| drop the `pcall` | 1 chain |
|
||||||
| skip consumers when `rec == nil` | 1 chain + **3 auto-pair** |
|
| skip consumers when `rec == nil` | 1 chain + **3 auto-pair** |
|
||||||
| load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) |
|
| load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) |
|
||||||
|
| hand every consumer the same record table | 1 chain (46f) |
|
||||||
|
| iterate the live array instead of a snapshot | 1 chain (46g) |
|
||||||
|
| render the error outside the `pcall` | 1 chain (46d) |
|
||||||
|
| accept any Lua number as a priority | 1 chain (46h) |
|
||||||
|
| make `remove_consumer` a no-op | 2 chain (46g, 46h) |
|
||||||
|
|
||||||
The first attempt at the last bite was WORTHLESS as written: moving
|
The first attempt at the last bite was WORTHLESS as written: moving
|
||||||
only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil
|
only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil
|
||||||
|
|
@ -194,9 +216,12 @@ If it does not, stop and repair the remote/fetch configuration.
|
||||||
- Verification on this branch (commit-then-gate, so this describes the
|
- Verification on this branch (commit-then-gate, so this describes the
|
||||||
pushed tree): `cargo fmt --check` clean; strict workspace Clippy
|
pushed tree): `cargo fmt --check` clean; strict workspace Clippy
|
||||||
clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45;
|
clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45;
|
||||||
typed-edit chain 9/9; M4 121; required GPU 202; **isolated-config
|
typed-edit chain 13/13 (and 13/13 again under `--no-default-features
|
||||||
workspace sweep 3,328 across 97 suites, zero failures** with
|
--features lua54`, since the fixes touch `math.huge`, `%`, and
|
||||||
`grep -c basedpyright` = 0; `git diff --check` clean.
|
`__tostring` behavior that differs between the backends); M4 121;
|
||||||
|
required GPU 202; **isolated-config workspace sweep 3,332 across 97
|
||||||
|
suites, zero failures** with `grep -c basedpyright` = 0; `git diff
|
||||||
|
--check` clean.
|
||||||
- Stage 4b (the input method) is NOT in this PR and not started.
|
- Stage 4b (the input method) is NOT in this PR and not started.
|
||||||
|
|
||||||
## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165)
|
## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165)
|
||||||
|
|
|
||||||
|
|
@ -88,10 +88,26 @@ commands, read `docs/active-work.md` immediately after this file.
|
||||||
config swap invalidates. The durable lesson is to heal at
|
config swap invalidates. The durable lesson is to heal at
|
||||||
**consumption** — the point where a stale record is handed out — not
|
**consumption** — the point where a stale record is handed out — not
|
||||||
at the moment of the swap.
|
at the moment of the swap.
|
||||||
- Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode
|
- **Stage 4a (typed-edit consumer chain) is implemented and in review
|
||||||
input method) are framed and awaiting approval; stages 5 (goal
|
as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev
|
||||||
panel), 6 (`#eval` output channel), and 7 (module hierarchy) are
|
8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the
|
||||||
framed but not scouted against current `main`.
|
single `buffer.after-edit` subscriber and the single one-shot read,
|
||||||
|
`pair.lua` becomes its first registered consumer, and
|
||||||
|
`tests/auto_pair_acceptance.rs` is unchanged by zero lines
|
||||||
|
(criterion 46, verified at the diff). No protocol change, no Lean
|
||||||
|
content. The three decisions that turned out load-bearing rather
|
||||||
|
than stylistic: consumers are called **even when the record is
|
||||||
|
nil** (three existing auto-pair tests assert the non-event through
|
||||||
|
it, and 4b abandons stale pending state on it); each consumer gets
|
||||||
|
its **own copy** of the record, because pairing reads `rec.char`
|
||||||
|
and a declining consumer could otherwise forge it; and the fan-out
|
||||||
|
iterates a **snapshot**, because a consumer that registers a
|
||||||
|
lower-priority one shifts itself forward under `ipairs` and runs
|
||||||
|
twice.
|
||||||
|
- Remaining: Stage 4b (the Unicode input method) is framed and
|
||||||
|
awaiting approval — not started; stages 5 (goal panel), 6 (`#eval`
|
||||||
|
output channel), and 7 (module hierarchy) are framed but not
|
||||||
|
scouted against current `main`.
|
||||||
|
|
||||||
- **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3;
|
- **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3;
|
||||||
merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU
|
merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU
|
||||||
|
|
|
||||||
|
|
@ -1496,7 +1496,7 @@ claim a reader must be able to check without reconstructing
|
||||||
| `builtin/runtime/typed_edit.lua` | new — the chain owner |
|
| `builtin/runtime/typed_edit.lua` | new — the chain owner |
|
||||||
| `builtin/runtime/pair.lua` | re-expressed as one registered consumer |
|
| `builtin/runtime/pair.lua` | re-expressed as one registered consumer |
|
||||||
| `src/editor.rs` | one `include_str!` line, before `pair.lua`'s |
|
| `src/editor.rs` | one `include_str!` line, before `pair.lua`'s |
|
||||||
| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e |
|
| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46h |
|
||||||
| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** |
|
| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** |
|
||||||
|
|
||||||
Rev 6 listed only the first three and then required criteria 46a–46e,
|
Rev 6 listed only the first three and then required criteria 46a–46e,
|
||||||
|
|
@ -2374,7 +2374,7 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage.
|
||||||
Per the no-renumbering rule above, round 5's additions take letter
|
Per the no-renumbering rule above, round 5's additions take letter
|
||||||
suffixes on both sides of the split.
|
suffixes on both sides of the split.
|
||||||
|
|
||||||
46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which
|
46a–46h live in a **new `tests/typed_edit_chain_acceptance.rs`**, which
|
||||||
is part of Stage 4a's declared footprint (Q#LN10) and a required gate
|
is part of Stage 4a's declared footprint (Q#LN10) and a required gate
|
||||||
for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which
|
for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which
|
||||||
criterion 46 requires to stay byte-identical.
|
criterion 46 requires to stay byte-identical.
|
||||||
|
|
@ -2394,14 +2394,44 @@ criterion 46 requires to stay byte-identical.
|
||||||
`include_str!` order happens to agree with intent.
|
`include_str!` order happens to agree with intent.
|
||||||
46c. A claiming consumer stops the chain — a later consumer does not
|
46c. A claiming consumer stops the chain — a later consumer does not
|
||||||
run — and a non-claiming one does not.
|
run — and a non-claiming one does not.
|
||||||
46d. A consumer that throws is contained: the fan-out still succeeds,
|
46d. A consumer that throws is contained: the later consumers still
|
||||||
the other consumers still run, and the failure reports through
|
run, and the failure reports through `set_status`. Bites against a
|
||||||
`set_status`. Bites against the `all-must-succeed` contract taking
|
chain where one bad consumer silently disables every consumer
|
||||||
the whole fan-out down with one bad consumer (Q#LN10).
|
behind it. (Round 8 correction: an uncontained throw would *not*
|
||||||
|
take the fan-out's other subscribers down — `run_all_must_succeed`
|
||||||
|
in `src/hook.rs` collects errors and continues, so `lsp.lua` still
|
||||||
|
flushes. Rev 7 claimed otherwise. The containment is still
|
||||||
|
required; the reason is narrower than stated.) Rendering the error
|
||||||
|
is itself protected: a Lua error may be any value, including a
|
||||||
|
table whose `__tostring` throws, and reporting outside the
|
||||||
|
containment reintroduces the escape it exists to prevent.
|
||||||
46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server
|
46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server
|
||||||
test — pairing's closer must be in the buffer before `lsp.lua`
|
test — pairing's closer must be in the buffer before `lsp.lua`
|
||||||
flushes `didChange` — still holds with pairing behind the chain.
|
flushes `didChange` — still holds with pairing behind the chain.
|
||||||
Falsified by moving the chain's registration after `lsp.lua`'s.
|
Falsified by moving the chain's registration after `lsp.lua`'s.
|
||||||
|
46f. **Each consumer's record is its own.** A declining consumer that
|
||||||
|
mutates the record it was handed cannot change what a later
|
||||||
|
consumer sees. Bites against handing every consumer the same
|
||||||
|
mutable table: pairing decides what to close from `rec.char`, so a
|
||||||
|
forged `char` makes it insert a pair the user never typed. Every
|
||||||
|
field is a scalar or an opaque id, so a shallow copy is a complete
|
||||||
|
snapshot.
|
||||||
|
46g. **The fan-out iterates a snapshot.** A consumer may register or
|
||||||
|
remove consumers while the chain runs; both take effect on the next
|
||||||
|
fan-out. Bites against iterating the live array, where a consumer
|
||||||
|
that registers a lower-priority one shifts itself forward under
|
||||||
|
`ipairs` and runs twice — unbounded if it re-registers each time.
|
||||||
|
46h. **The registrar has a lifecycle.** `add_consumer` returns an
|
||||||
|
opaque handle; `remove_consumer` unregisters it and reports whether
|
||||||
|
it was live, so a double-remove is a no-op rather than a throw.
|
||||||
|
Without it, re-evaluating a config or reloading a package
|
||||||
|
accumulates callbacks permanently — the leak `COHERENCE.md` §13
|
||||||
|
already records against `pmacs.hook.add`, which a teardown-less
|
||||||
|
chain would inherit and spread to every consumer. Priority is
|
||||||
|
validated as a **finite integer in i32 range**, matching
|
||||||
|
`pmacs.completion.register`: NaN is a number and every ordered
|
||||||
|
comparison with it is false, so a bare type check lets it land
|
||||||
|
wherever the insertion scan gives up and silently voids 46b.
|
||||||
|
|
||||||
**Stage 4b — the Unicode input method**
|
**Stage 4b — the Unicode input method**
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,11 +1,13 @@
|
||||||
//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a,
|
//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a,
|
||||||
//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46e).
|
//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46h).
|
||||||
//!
|
//!
|
||||||
//! The chain owns the single `buffer.after-edit` subscriber that reads
|
//! The chain owns the single `buffer.after-edit` subscriber that reads
|
||||||
//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in
|
//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in
|
||||||
//! priority order. These tests pin the chain's OWN behavior — take-once,
|
//! priority order. These tests pin the chain's OWN behavior — take-once,
|
||||||
//! priority ordering, claim-stops-chain, throw containment, and the
|
//! priority ordering, claim-stops-chain, throw containment, per-consumer
|
||||||
//! Q#AP7 flush ordering it inherited from `pair.lua`.
|
//! record isolation, snapshot iteration under re-entrant registration,
|
||||||
|
//! the registration lifecycle, and the Q#AP7 flush ordering it inherited
|
||||||
|
//! from `pair.lua`.
|
||||||
//!
|
//!
|
||||||
//! They deliberately do not re-test auto-pairing: criterion 46 requires
|
//! They deliberately do not re-test auto-pairing: criterion 46 requires
|
||||||
//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that
|
//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that
|
||||||
|
|
@ -324,9 +326,12 @@ fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() {
|
||||||
"#,
|
"#,
|
||||||
);
|
);
|
||||||
|
|
||||||
// `buffer.after-edit` is all-must-succeed: an uncontained throw
|
// An uncontained throw would abandon every LATER consumer in the
|
||||||
// would fail the fan-out for every other subscriber, including
|
// chain and mark the whole `buffer.after-edit` run failed. It would
|
||||||
// lsp.lua's didChange flush.
|
// NOT stop the hook's other subscribers — all-must-succeed collects
|
||||||
|
// errors and keeps going (`src/hook.rs`'s `run_all_must_succeed`) —
|
||||||
|
// so what this pins is that one broken consumer cannot silently
|
||||||
|
// disable the ones behind it.
|
||||||
type_str(&mut s, "(");
|
type_str(&mut s, "(");
|
||||||
|
|
||||||
let later_ran: bool = eval(&s, "return _G.later_ran");
|
let later_ran: bool = eval(&s, "return _G.later_ran");
|
||||||
|
|
@ -357,12 +362,43 @@ fn add_consumer_rejects_malformed_registrations() {
|
||||||
),
|
),
|
||||||
(
|
(
|
||||||
"pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }",
|
"pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }",
|
||||||
"priority must be a number",
|
"priority must be a finite integer",
|
||||||
),
|
),
|
||||||
(
|
(
|
||||||
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }",
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }",
|
||||||
"fn must be a function",
|
"fn must be a function",
|
||||||
),
|
),
|
||||||
|
// NaN is a number and every ordered comparison with it is
|
||||||
|
// false, so a bare type check lets it land wherever the
|
||||||
|
// insertion scan gives up — and the lowest-first contract the
|
||||||
|
// Lean expander depends on quietly stops holding. The
|
||||||
|
// infinities and non-integers go with it: priority matches
|
||||||
|
// `pmacs.completion.register`'s i32.
|
||||||
|
(
|
||||||
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = 0/0, \
|
||||||
|
fn = function() end }",
|
||||||
|
"priority must be a finite integer",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = math.huge, \
|
||||||
|
fn = function() end }",
|
||||||
|
"priority must be a finite integer",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = -math.huge, \
|
||||||
|
fn = function() end }",
|
||||||
|
"priority must be a finite integer",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1.5, \
|
||||||
|
fn = function() end }",
|
||||||
|
"priority must be a finite integer",
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"pmacs.typed_edit.add_consumer{ name = \"n\", priority = 4e9, \
|
||||||
|
fn = function() end }",
|
||||||
|
"priority must be a finite integer",
|
||||||
|
),
|
||||||
] {
|
] {
|
||||||
let err = s
|
let err = s
|
||||||
.lua_host
|
.lua_host
|
||||||
|
|
@ -378,6 +414,188 @@ fn add_consumer_rejects_malformed_registrations() {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn an_error_whose_rendering_throws_is_still_contained() {
|
||||||
|
// A Lua error may be any value, including a table whose
|
||||||
|
// `__tostring` throws. Rendering it outside the containment is a
|
||||||
|
// second, uncontained throw — the chain would stop at exactly the
|
||||||
|
// consumer it was trying to report.
|
||||||
|
let mut s = editor_with("");
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
r#"
|
||||||
|
_G.later_ran = false
|
||||||
|
local hostile = setmetatable({}, {
|
||||||
|
__tostring = function() error("rendering exploded") end,
|
||||||
|
})
|
||||||
|
pmacs.typed_edit.add_consumer {
|
||||||
|
name = "boom", priority = 1, fn = function() error(hostile) end,
|
||||||
|
}
|
||||||
|
pmacs.typed_edit.add_consumer {
|
||||||
|
name = "later", priority = 2,
|
||||||
|
fn = function() _G.later_ran = true; return false end,
|
||||||
|
}
|
||||||
|
"#,
|
||||||
|
);
|
||||||
|
|
||||||
|
type_str(&mut s, "(");
|
||||||
|
|
||||||
|
let later_ran: bool = eval(&s, "return _G.later_ran");
|
||||||
|
assert!(
|
||||||
|
later_ran,
|
||||||
|
"an unrenderable error must not escape the containment"
|
||||||
|
);
|
||||||
|
assert_eq!(buffer_text(&s), "()", "and pairing still ran");
|
||||||
|
let st = status(&s);
|
||||||
|
assert!(
|
||||||
|
st.contains("boom") && st.contains("<unprintable error>"),
|
||||||
|
"the consumer is still named, with a placeholder body, got {st:?}"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
// The record a consumer sees is its own
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn a_consumers_mutation_of_the_record_cannot_reach_the_next_consumer() {
|
||||||
|
// The record is plain Lua data. Handing every consumer the same
|
||||||
|
// table lets a DECLINING consumer rewrite provenance for the ones
|
||||||
|
// behind it — and pairing decides what to close from `rec.char`,
|
||||||
|
// so a forged `char` makes it insert a pair the user never typed.
|
||||||
|
let mut s = editor_with("");
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
r#"
|
||||||
|
_G.downstream_char = "unset"
|
||||||
|
pmacs.typed_edit.add_consumer {
|
||||||
|
name = "vandal", priority = 1,
|
||||||
|
fn = function(rec)
|
||||||
|
if rec then rec.char = "("; rec.codepoint = 40 end
|
||||||
|
return false
|
||||||
|
end,
|
||||||
|
}
|
||||||
|
pmacs.typed_edit.add_consumer {
|
||||||
|
name = "witness", priority = 2,
|
||||||
|
fn = function(rec)
|
||||||
|
_G.downstream_char = rec and rec.char or "nil"
|
||||||
|
return false
|
||||||
|
end,
|
||||||
|
}
|
||||||
|
"#,
|
||||||
|
);
|
||||||
|
|
||||||
|
type_str(&mut s, "x");
|
||||||
|
|
||||||
|
let downstream: String = eval(&s, "return _G.downstream_char");
|
||||||
|
assert_eq!(
|
||||||
|
downstream, "x",
|
||||||
|
"the next consumer sees the real typed character"
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
buffer_text(&s),
|
||||||
|
"x",
|
||||||
|
"and pairing, reading the same field, did not close a forged opener"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
// Re-entrant registration, and the consumer lifecycle
|
||||||
|
// ---------------------------------------------------------------------------
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn registering_or_removing_during_a_fan_out_takes_effect_on_the_next_one() {
|
||||||
|
// The fan-out iterates a snapshot. Iterating the live array instead
|
||||||
|
// lets a consumer that registers a LOWER-priority one shift itself
|
||||||
|
// forward under `ipairs` and run twice in a single fan-out — and
|
||||||
|
// repeating the registration makes that unbounded.
|
||||||
|
let mut s = editor_with("");
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
r#"
|
||||||
|
_G.order = {}
|
||||||
|
local function mark(tag)
|
||||||
|
return function() _G.order[#_G.order + 1] = tag; return false end
|
||||||
|
end
|
||||||
|
_G.doomed = pmacs.typed_edit.add_consumer {
|
||||||
|
name = "doomed", priority = 50, fn = mark("doomed"),
|
||||||
|
}
|
||||||
|
_G.did_register = false
|
||||||
|
pmacs.typed_edit.add_consumer {
|
||||||
|
name = "a", priority = 10,
|
||||||
|
fn = function()
|
||||||
|
_G.order[#_G.order + 1] = "a"
|
||||||
|
if not _G.did_register then
|
||||||
|
_G.did_register = true
|
||||||
|
pmacs.typed_edit.add_consumer { name = "b", priority = 5, fn = mark("b") }
|
||||||
|
pmacs.typed_edit.remove_consumer(_G.doomed)
|
||||||
|
end
|
||||||
|
return false
|
||||||
|
end,
|
||||||
|
}
|
||||||
|
"#,
|
||||||
|
);
|
||||||
|
|
||||||
|
type_str(&mut s, "x");
|
||||||
|
let first: String = eval(&s, "return table.concat(_G.order, ',')");
|
||||||
|
assert_eq!(
|
||||||
|
first, "a,doomed",
|
||||||
|
"`a` runs once even though it registered ahead of itself, and \
|
||||||
|
`doomed` still runs in the fan-out it was removed during"
|
||||||
|
);
|
||||||
|
|
||||||
|
exec(&s, "_G.order = {}");
|
||||||
|
type_str(&mut s, "y");
|
||||||
|
let second: String = eval(&s, "return table.concat(_G.order, ',')");
|
||||||
|
assert_eq!(
|
||||||
|
second, "b,a",
|
||||||
|
"both the registration and the removal land on the next fan-out"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn remove_consumer_unregisters_and_reports_whether_it_was_live() {
|
||||||
|
// Without removal, re-evaluating a config or reloading a package
|
||||||
|
// accumulates callbacks permanently — the leak COHERENCE.md §13
|
||||||
|
// already records against `pmacs.hook.add`. A chain with no
|
||||||
|
// teardown would inherit it and spread it to every consumer.
|
||||||
|
let mut s = editor_with("");
|
||||||
|
exec(
|
||||||
|
&s,
|
||||||
|
r#"
|
||||||
|
_G.runs = 0
|
||||||
|
_G.h = pmacs.typed_edit.add_consumer {
|
||||||
|
name = "temporary", priority = 1,
|
||||||
|
fn = function() _G.runs = _G.runs + 1; return false end,
|
||||||
|
}
|
||||||
|
"#,
|
||||||
|
);
|
||||||
|
|
||||||
|
type_str(&mut s, "x");
|
||||||
|
let runs: i64 = eval(&s, "return _G.runs");
|
||||||
|
assert_eq!(runs, 1, "registered consumers run");
|
||||||
|
|
||||||
|
let first_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)");
|
||||||
|
let second_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)");
|
||||||
|
assert!(first_removal, "removing a live consumer reports true");
|
||||||
|
assert!(
|
||||||
|
!second_removal,
|
||||||
|
"a double-remove is a reportable no-op, not a throw"
|
||||||
|
);
|
||||||
|
|
||||||
|
type_str(&mut s, "y");
|
||||||
|
let runs: i64 = eval(&s, "return _G.runs");
|
||||||
|
assert_eq!(runs, 1, "the removed consumer no longer runs");
|
||||||
|
// Removal is surgical: the chain itself, and pairing on it, survive.
|
||||||
|
exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())");
|
||||||
|
type_str(&mut s, "(");
|
||||||
|
assert_eq!(
|
||||||
|
buffer_text(&s),
|
||||||
|
"xy()",
|
||||||
|
"the rest of the chain is untouched"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
// 46e — the Q#AP7 flush ordering the chain inherited
|
// 46e — the Q#AP7 flush ordering the chain inherited
|
||||||
// ---------------------------------------------------------------------------
|
// ---------------------------------------------------------------------------
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue