neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

docs(lean4): correct Q#LN10's throw-containment rationale 

Q#LN10 still said a throwing consumer "fails the fan-out for everyone."
It does not: `run_all_must_succeed` (src/hook.rs:332) collects the error
and continues to the hook's remaining subscribers, so `lsp.lua` still
flushes didChange. The throw stops every LATER consumer in the chain,
which is a narrower consequence and still worth containing — the
failure is silent exactly where the abandoned consumers registered.

The module comment, criterion 46d, the test, and the ledger were all
corrected in the previous commit; Q#LN10 is the decision they descend
from, so leaving it stale would have made the disproven claim the
authoritative one. Also records the protected-rendering rule there.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
This commit is contained in:
Levi Neuwirth 2026-07-26 13:43:30 -04:00
parent aef4e98c26
commit ea9b8c379e
1 changed files with 22 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
docs/lean4-mode-framing.md
View File

@ -1523,11 +1523,28 @@ sees the exact record via `_capture_records`, and that the Q#AP7 ordering
against `lsp.lua`'s `didChange` flush still holds.
**What 4a deliberately does not do.** It does not change the `all-must-
succeed` contract, so a consumer that throws still fails the fan-out for
everyone. The chain owner therefore `pcall`s each consumer and reports
through `pmacs.editor.set_status`, matching `pair.lua`'s existing
never-throw-from-after-edit discipline — this is behavior-preserving for
pairing (which already never throws) and is the guardrail 4b needs.
succeed` contract. What that contract actually does on a throw was
stated wrongly through rev 7 and is corrected here, because this
paragraph is the authority the module comment, criterion 46d, the test,
and the ledger all descend from: `run_all_must_succeed`
(`src/hook.rs:332`) **collects** the error and continues to the hook's
remaining subscribers, marking only the run as failed. An uncontained
throw inside the chain therefore does **not** stop `lsp.lua` from
flushing `didChange`. What it does stop is every LATER consumer in the
chain — the chain is one subscriber, and a throw abandons the rest of
its loop.
That is a narrower consequence than rev 7 claimed and still worth
containing, because the failure is silent in the direction that matters:
a consumer that throws disables the consumers behind it with no signal
at the seam where they were registered. The chain owner therefore
`pcall`s each consumer and reports through `pmacs.editor.set_status`,
matching `pair.lua`'s existing never-throw-from-after-edit discipline —
this is behavior-preserving for pairing (which already never throws) and
is the guardrail 4b needs. The **rendering** of the caught error is
protected the same way: a Lua error may be any value, including a table
whose `__tostring` throws, so `tostring` outside the `pcall` would
reintroduce the escape the containment exists to prevent.
### Q#LN11 — Stage 4b data: vendor the table, generated, attributed