Repository navigation
fix(queue): keep the readiness wait for a send with broadcast debouncing off - #541
Merged
Merged
Conversation
…s wait after a handshake With disable_broadcast_debouncing on and an empty queue, a send right after Claude's handshake must reach Claude only once connection_wait_delay has passed, as a queued mention does. A send once Claude is ready still goes out at once. Both tests fail on main: Claude gets the mention 3 to 6 ms after its handshake.
…ing off With disable_broadcast_debouncing set and an empty queue, _broadcast_at_mention broadcast at once and skipped the readiness check, so a Claude whose handshake came less than connection_wait_delay ms ago got the mention while it was still starting up (3 to 7 ms after the handshake on Neovim 0.8.0 and 0.12.3). The immediate path now runs only while some connected client is ready. Otherwise the mention goes through the queue, which sends it once a client is ready. With no client that reports its handshake time, the immediate path still runs and fails at once as before.
…iness fix in init.lua
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…g in verify-mention-queue The model now has the user's disable_broadcast_debouncing as a variable, either value, fixed for the run. With it set, a send while Claude is connected and the queue is empty broadcasts at once, while some connected client is ready (new fact ImmediateWaitsForReady, read from _broadcast_at_mention). Otherwise it queues as before. With the fact FALSE, SentWhenReady breaks. FailedWriteReported now also reads the immediate path's report_unwritten.
…s with debouncing off; tidy the replay runner - tests/unit/mention_queue_spec.lua: a send 20 ms before the readiness wait ends must queue and go out at the flush, not at once. A readiness check that lets sends within 100 ms of ready through no longer survives. - replays/run.sh: exit 2 when NVIM names no Neovim, put bash's "Alarm clock" note in the replay's log, and drop the VimLeavePre example (Neovim exits 0 after a VimLeavePre error). - drain.lua, SKILL.md: say "an 8.6 s wait before Claude connects". SKILL.md: SentWhenReady and the scope now cover disable_broadcast_debouncing on and off, with the new ImmediateWaitsForReady fact.
…readiness fix in init.lua Both hash all of init.lua. The fix changes only _broadcast_at_mention, which neither model reads, and both models pass on the new code.
A NVIM in a missing folder made the absolute-path step print a cd error and turn NVIM into /nvim. The runner now keeps the given path then, and the Neovim check names it.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
|
Codex Review: Didn't find any major issues. Keep them coming! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…t_at_mention, and pin a send 1 ms before ready Verifier minors on #541 at 700cbf6: - check.sh: ImmediateWaitsForReady reads TRUE only when the guard is the first broadcast or queue_mention line of _broadcast_at_mention, so an unguarded broadcast added before it reads FALSE. - tests/unit/mention_queue_spec.lua: the near-ready send now comes 1 ms before ready, not 20 ms, so a readiness check with any tolerance of 2 ms or more fails it. The fake clock makes the 1 ms exact. - SKILL.md: the state counts double, since each run checks both values of disable_broadcast_debouncing.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
|
Codex Review: Didn't find any major issues. Keep them coming! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
Record the verify-ws-connection lock: main's #541 changed the file hash of lua/claudecode/init.lua in M._broadcast_at_mention, which the model does not cover. The covered blocks are unchanged.
This was referenced Nov 12, 2026
Merged
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 14, 2026
… connection lifecycle (coder#474) Adds `.agents/skills/verify-ws-connection`: a TLA+ model of one WebSocket connection between Claude and the plugin, checked with TLC against guards that `check.sh` reads from the Lua source. It is the second `verify-*` skill on the shared harness (`scripts/tla/check-lib.sh`, coder#450), after `verify-diff-lifecycle`. It describes the keepalive as coder#488 merged it (d63c9b3, with the fix for the fresh clock at the tick). On the code of coder#479 it reads STALE, and its facts for the new design read FALSE. ## What it checks Six rules, from the TCP accept through the handshake, requests, Close frames, keepalive pings and server stop: | Rule | Plain sentence | | --- | --- | | `NoRequestAfterEnd` | A request from Claude runs only after its 101 reply was written, and never after the plugin started to close the connection or saw it end. | | `DisconnectReportedOnce` | `on_disconnect` runs at most once per client. | | `StatusCloseDelivered` | A Close frame for a protocol error (1002, 1003, 1007, 1009) or a server stop (1001) is written before the plugin closes the socket, as long as Claude keeps reading. A Claude whose queue makes no progress for one keepalive window loses the frame to the deadline of `close_client`, which closes the socket (not modeled). | | `NoFalseTimeout` | A Claude that answers each ping before the next tick is never dropped by the ping timer, whatever blocks Neovim or sleeps the machine. A tick reads a fresh clock, only pings and stamps the oldest unanswered ping. The check that drops a client runs after a poll that read the sockets, judges nothing when its poll comes more than 1.5 intervals after its tick, and any bytes read from the client clear the stamp. A Claude that stopped once is not covered. A pong that comes later than one interval is not covered either: when a callback blocks inside the poll phase and refreshes the loop time, the poll can miss it, and the check closes that client once its ping is 2.5 intervals old (the verifier's probe on Neovim 0.12.3 dropped a peer that answered 2.4, 1.4 and 0.4 intervals late. Main does the same.) A real Claude answers a ping at once. The rule holds for any limit above `interval * 1.5`, the window in which a check still judges: a limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. The code keeps 2.5. | | `DeadClientDropped` | A client whose Claude hung up or stopped answering, or whose connection the plugin started to close, eventually leaves `server.clients` with its `on_disconnect`. | | `DroppedSocketCloses` | Once a client left `server.clients`, or the server stopped, its socket eventually closes, as long as Claude reads again. | `covered.lock` hashes the five files the model describes (`server/client.lua`, `tcp.lua`, `handshake.lua`, `server/init.lua`, `init.lua`) and the blocks inside them, so a change there reads `STALE` until someone confirms the model still fits. The model describes the keepalive judgement only. The stall rule of coder#467 (`judge_stall`) and the deadline of a Close frame are not modeled, and `SKILL.md` says what a user sees for each. ## Bugs this model found Its first run broke three rules on the code as it was. Each one was replayed with real sockets and fixed in coder#455. Reviews of this PR then found four more false timeouts that the first model could not see. coder#479 and coder#488 (three rounds of it) fixed them: - `NoFalseTimeout`: a main loop blocked during the handshake got a Claude that answers every ping dropped with 1011 before any ping reached it. Since coder#488 a client has no stamp until a tick pings it, so no block can time it out. - `DeadClientDropped`: after a protocol error while Claude's window was full, the client stayed in `server.clients` (and `is_claude_connected()` stayed true) until Claude read again. - `DroppedSocketCloses`: a stop between Claude's Close frame and the scheduled `on_close` left the plugin's socket in `CLOSE_WAIT`. - `NoFalseTimeout`, again (coder#479): a tick that Neovim ran late after a block of 1.0 to 1.5 intervals can run before the plugin reads Claude's pong, and found the last pong 2.3 intervals old. libuv runs timers before it reads sockets: with libuv 1.44, which Neovim 0.8 bundles, after a block in any callback, and with newer libuv after a block in a check or I/O callback, not after one in `vim.schedule` or a timer callback. - `NoFalseTimeout`, a third time (coder#488): libuv 1.44 runs the timers at the end of a pass of the main loop and again at the start of the next, with Neovim's `vim.schedule` callbacks between. Two ticks ran with no read between them, and coder#479 dropped a Claude that answered every ping. No counter of ticks fixes that, so a tick now only pings and a libuv check handle, which runs after the poll, does the dropping. - `NoFalseTimeout`, a fourth time (the review of coder#488): the check ran on a poll that did not reach Claude's answer. A pong waits behind more unread data than the socket holds (any bytes from the client now clear the stamp), or the machine sleeps between a tick and its poll (the check judges nothing after a block longer than 1.5 intervals). Each of the two guards alone leaves one path open. The model has both, and a replay for each. - `NoFalseTimeout`, a fifth time (Codex's review of coder#488): the tick read `vim.loop.now()` before it called `update_time()`. libuv runs all timers of a pass with the loop time of the start of the pass, so after a sleep or a block of more than 1.5 intervals in an earlier timer callback of the same pass the tick saw no gap, kept the old stamps, and the check dropped a Claude that had no time to answer. The tick now updates the loop time first. There is no replay for it (a replay cannot make a timer callback run before the ping timer inside one pass), so the unit test of coder#488 and the model pin it: with `ClockFreshAtTick` off, `NoFalseTimeout` breaks. The model in this PR describes the fixed code (18 guards, all read TRUE). ## Round 7 (the one extra review round that the maintainer allowed) This push carries the prepared fixes for the last findings of the two verifiers of `77bb6e2`, and merges of main. The model (`model/`) and the `EXPECT` map are the same as in `77bb6e2`. - The limit that the promise holds for. `NoFalseTimeout` holds for any limit above `interval * 1.5`, not for one interval or more. A limit of 1.2 intervals passes the model, and real Neovim drops a Claude that answered within 100 ms when a read callback blocks about 1.3 intervals in the poll after the tick. `SKILL.md` says so now. The code keeps 2.5. - Which test catches which clock mutation. `SKILL.md` named the wrong test for one of them. Deleting `update_time()`, or moving it after `local elapsed` without reading `now` again, turns red only "ages a ping from when it was sent...". Moving it after the wake test and reading `now` again turns red only "takes a tick for a wake...". I ran both mutations. - The README and the comment of `start_ping_timer` say that the first check that finds the oldest unanswered ping `interval * 2.5` old closes a silent Claude, and that a block inside the poll phase refreshes the loop time. - `check.sh`: the record pattern lists `write(client, ` and `handle:close()`, so a change to one of those lines reads STALE. The `DispatchGuard` fact needs the `end` of its `if` right after `on_message`. The `StopWaitsForCloseWrite` fact rejects `release_socket`, `abandon_close_frame` and `drop_client` in `stop_server`. Five wording fixes in `SKILL.md`, and a note that the `sleep` case of the bytes-only contrast on Neovim 0.8.3 depends on timing. - Merges of main (the last one is coder#577). The server README keeps this PR's keepalive paragraph and takes main's new bullets. After the first two merges three locks read STALE and are recorded again: `verify-diff-lifecycle` and `verify-mention-queue` (the hash of `tcp.lua`, which differs from main only in the comment of `start_ping_timer`), and `verify-ws-connection` (`tcp.lua`, and `M.start` and `M.stop` in `server/init.lua`, where main's coder#539 changed a log line in `on_open` and coder#558 answers in-flight requests before `stop_server`). The second merge made the ws lock stale once more: main's coder#541 changed `M._broadcast_at_mention` in `init.lua`, which the model does not cover, and the covered blocks have the same hashes. The model still fits: those answers are ordinary writes to a connected client, the case the model has. The last two merges (coder#544 and coder#577, terminal and diff files only) needed no new record. ## What changed since the first version of this PR - The model follows coder#488: the facts `DropsOnSecondOverdueTick`, `AliveTickClearsOverdue`, `PongResetsAge`, `WakeResetsPong` and `UpgradeStartsKeepalive` are gone. `JudgesAfterRead`, `ClockFreshAtTick`, `StampKeepsOldestPing`, `BytesClearStamp`, `GapSkip` and `WakeClearsStamp` replace them. The environment steps are `StaleLoopTime`, `PollMissesPong` and `SleepInWindow`. A `stale` tick (an earlier callback of the pass blocked or slept) is a wake that only a tick with a fresh clock sees. - **`NoFalseTimeout` no longer counts awake time.** The first model added one tick of awake time on a late tick, so its own sentence ("a block does not count as awake time") was false, and a drop at a late tick while a pong waited unread passed. The rule now asks whether a Claude that never stopped answering was dropped, and the ticks run at any point between reads. A variant that judges at the tick (`JudgesAfterRead` off) breaks it in 12 states. - The text of `SKILL.md` is fixed: the libuv wording, the timings, the exit codes of `--hash-only`, the numbering of the update steps, the order of the `/statechart` steps (the kept directory is deleted after the view is handed over), the sentence about `--mutants` (`RejectClosesSocket` is caught only together with `UnlistedDisconnectReleases`), and each item that is not modeled now says what a user sees. That includes a client that sends bytes and never reads (coder#467 handles that stall) and a client that writes data but never answers a ping, which coder#488 keeps by design. ## What this PR changes outside the skill - `server/README.md` and the comment of `start_ping_timer` described the silent close and the promise wrongly. A silent Claude is closed by the first check that finds its oldest unanswered ping `interval * 2.5` old: 90 s after the ping when ticks come on time. One late tick delays it, because a late tick moves the ticks after it back. Two late ticks in a row, or a poll that a block delays after a tick, bring it as early as 75 s (2.6 intervals in the probes, never earlier). A tick more than `interval * 1.5` after the tick before it is a wake and restarts the count, so a block of more than half an interval just before a tick is enough, not only one of 1.5 intervals. The promise of no false close is now for a Claude that answers each ping before the next tick, as the model checks it, and the README says what a pong later than one interval costs under a block in the poll phase. - A comment in `connection_lifecycle_spec.lua` still named the pong rule and `pong_overdue`, which coder#488 removed. It names the keepalive and the stall rule now. - The comment-only edits to `client.lua`, `tcp.lua` and the spec that this PR carried for the design of coder#479 are gone, because coder#488 replaced that code. - `DEVELOPMENT.md`: the two paragraphs about `covered.lock` name every `verify-*` lock, not only that of `verify-diff-lifecycle` (unchanged in this push). ## Proof - `check.sh` on this branch (checked on the head before the last merge): all 18 facts TRUE and `RESULT: PASS`. `main` 262,285 states, `live-NoFalseTimeout` 256,264, `live-DeadClientDropped` 11,701, `live-DroppedSocketCloses` 11,701. It took 256 s and 271 s in two runs at a host load average of 14 to 40, and 2 to 6 min in other runs. The `check.sh` of the other four skills (`verify-diff-lifecycle`, `verify-mention-queue`, `verify-selection-tracking`, `verify-terminal-lifecycle`) all pass too, and all five locks match the code (`--hash-only`). - `check.sh --mutants` (one TLC worker): I ran it uninterrupted on the head of this push, before the last three merges of main (they change no covered block of this skill): 18 rows, every guard caught, exit 0, 5,753 s at a load average of 14 to 40. Both verifiers of `77bb6e2` had run it uninterrupted too (Opus: 4761 s, gpt: 4814 s, 18 rows each). `git diff 77bb6e2 HEAD -- .agents/skills/verify-ws-connection/model` is empty and the `EXPECT` map is the same in all three runs. The new and changed guards are caught by `NoFalseTimeout` (`JudgesAfterRead`, `ClockFreshAtTick`, `BytesClearStamp`, `GapSkip`, `WakeClearsStamp`) and `DeadClientDropped` (`KeepaliveReaps`, `StampKeepsOldestPing`). `RejectClosesSocket` alone is caught by no rule, because `_disconnect_client` also closes the socket of a client that left the server, so it is removed together with `UnlistedDisconnectReleases`. - A design check outside `check.sh` for the fresh clock: with the `ClockFreshAtTick` fact forced FALSE, `main` passes (264,485 states) and `live-NoFalseTimeout` breaks. So the fact is needed, and the model shows why. - A design check outside `check.sh`: with a clear of the stamp on a PONG only, in place of the any-bytes clear (the design before the any-bytes rule of coder#488), `NoFalseTimeout` breaks through `PollAndCheckPartial`, the poll that reads only the first frame. So `BytesClearStamp` is needed, and the model shows why. The verifier's run of that variant found 83,746 states. The count depends on how the variant is cut, so I give no count of my own. - Fact fidelity: both verifiers removed each guard in the Lua and every one of the 18 facts flipped to FALSE (26 direct removals in Opus's run). Eight mutants that no fact saw now flip one: five in `tcp.lua` (no `table.insert(pinged, client)`, no ping sent, `judge_silence` called at the tick, `fn` run at once in `after_next_poll`, the `end` of the gap `if` moved above the call), and three guard moves from the last round (the `end` of the `DispatchGuard` if above `on_message`, and `abandon_close_frame` with `release_socket`, or `drop_client`, in the `stop_server` loop). I reran the verifier's 42 mutations on the new `check.sh`: none is blind. - `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`. - Replays (real Neovim, real sockets), run again on the head before the last three merges of main, on Neovim 0.12.3 and on 0.8.3: `gap-during-handshake` 3 of 3, `short-block-after-ping` 3 of 3, `two-blocks-before-read` 3 of 3, `blocks-before-the-poll` 3 of 3, `protocol-close-window-full` 5 of 5, `stop-before-on-close` 4 of 4. `protocol-close-window-full.lua` changed for the merged code: it uses an interval of 500 ms and checks the open socket after half a keepalive window, because the deadline of `close_client` (merged on main since the replay was written) closes a socket whose Close frame makes no progress for one window, so it no longer stays open for ever while Claude does not read. The first three of the older replays keep `1 of 3`, `3 of 5` and `2 of 4` on main before coder#455 (3d4332c). `short-block-after-ping` keeps `2 of 3` on main before coder#479 (b65d266). `two-blocks-before-read` keeps `1 of 3` on the code of coder#479 on Neovim 0.8.3. `blocks-before-the-poll` keeps `0 of 3` on the first push of coder#488 (f3576ea) and with no clear of the stamp at all. With the gap skip and a clear on a PONG only it keeps `big-message` and `sleep` and breaks `two-blocks`. With the any-bytes clear and no gap skip it keeps `big-message` and `two-blocks` and breaks `sleep`. All on both Neovim versions. Both verifiers reproduced the contrast numbers of the other replays. The `sleep` run of the bytes-only build on Neovim 0.8.3 depends on timing: it kept all three once and two of three in five repeats. The last two replays run Claude in a second Neovim, because an in-process Claude answers only when the blocked loop runs again. - The full busted suite with CI's flags (`--coverage -v --shuffle`) on this branch: seeds 424242 and 9 on the head before the last two merges of main, each 1858 successes, 0 failures, 34 pending. Seed 424242 on `a929777` (merged with main at coder#544) 1887 successes, 0 failures, 34 pending. The last merge (coder#577, `diff.lua` and its spec) I did not run again as a whole suite. `luacheck` (with `--no-unused-args --no-max-line-length`) reports 0 warnings in 196 files. `treefmt` (stylua, prettier, shfmt, shellcheck) reports no change on the 16 files this PR touches. Every `covered.lock` matches the code (`--hash-only`) on the head of this push, and the full `check.sh` of `verify-diff-lifecycle` and `verify-terminal-lifecycle` pass on `a929777`. ## Run it ```bash .agents/skills/verify-ws-connection/check.sh # 2 to 6 min .agents/skills/verify-ws-connection/check.sh --mutants # about 80 min at a load average of 14, after you edit the model or a fact .agents/skills/verify-ws-connection/check.sh --hash-only # no TLC: compares covered.lock with the code NVIM=/path/to/nvim .agents/skills/verify-ws-connection/replays/run.sh blocks-before-the-poll.lua ``` CI's `covered-lock` job already runs every `.agents/skills/verify-*/check.sh`. `SKILL.md` has the rules, how to read a result, how to update the model, and its bounds. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this fixes
With
disable_broadcast_debouncing = trueand an empty queue,_broadcast_at_mentionbroadcast a send at once and skipped the readiness check. A Claude whose WebSocket handshake completed less thanconnection_wait_delayms ago (600 ms by default) got the mention while it was still starting up. On real Neovim 0.8.0 and 0.12.3 it arrived 3 to 10 ms after the handshake. With the default config the same send waits the full 600 ms.The option is not in the README or the
config.luadefaults. It is typed intypes.luaand described inlua/claudecode/README.md, so a user config can set it.The fix is in
lua/claudecode/init.lua(M._broadcast_at_mention): the immediate path now also needsms_until_a_client_is_ready()to be 0. That means some connected client completed its handshakeconnection_wait_delayms ago. Otherwise the mention goes through the queue, which sends it once a client is ready. Behavior is unchanged in two cases:The verify-mention-queue skill (#523, now on main) found this through a Codex review on its model. #523 excluded this config from its
SentWhenReadyrule as a known bug. #523 merged first, so this PR adds the model branch and flips that wording.The verify-mention-queue model now covers this path
model/MentionQueue.tla: a new variableimmediateholds the user'sdisable_broadcast_debouncing. Each run starts with either value and keeps it. With it on, a send while Claude is connected and the queue is empty broadcasts at once while some connected client is ready. Otherwise the send queues as before. The writes all succeed, all fail later, or are refused at once, as in a flush.check.sh: a new fact,ImmediateWaitsForReady, read from_broadcast_at_mention. It reads TRUE only when the readiness guard comes before every.broadcast(andqueue_mention(line of that function (a broadcast written as an indexed call or through an alias still reads TRUE; the unit tests catch those), so an unguarded broadcast added before the guard reads FALSE. With it FALSE,SentWhenReadybreaks.FailedWriteReportednow also reads the immediate send'sreport_unwritten("command", …).SKILL.md:SentWhenReadyholds withdisable_broadcast_debouncingon or off. The scope note now describes the check instead of a known bug, and the facts table lists the new fact.Tests
The first two tests were committed before the fix (ebcdb89) and failed on main:
tests/unit/mention_queue_spec.lua,D: with debouncing off, a send right after the handshake still waits for connection_wait_delay: a fake loop runs a send 100 ms after the handshake. It expects the mention in the queue, nothing at 590 ms and the mention at 610 ms. On main the queue stayed empty and the mention went out at once.tests/integration/mention_immediate_send_spec.lua(real Neovim, so CI runs it on stable and v0.8.0): a loopback Claude completes the handshake.connection_wait_delayhas passed. The time is measured on the loop clock that stampsconnected_at. On main:Claude got the mention 3 ms after its handshake, before 600 ms(0.8.0) and6 ms(0.12.3).tests/unit/mention_queue_spec.lua,D: with debouncing off, a send 1 ms before Claude is ready still waits in the queue(verifier F1 on 24b7ee7, tightened after the verifier on 700cbf6). The first two tests send 500 ms or more before ready, so a readiness check with a tolerance survived them. The fake clock makes the 1 ms exact on any Neovim. Each of these mutations of the guard fails only this test:< 2,< 20,<= 20and< 100. With the fix, the spec passes 53 of 53.Replay runner and wording (minor findings from #523 round 6)
replays/run.sh: it exits 2 before the first replay whenNVIMnames no Neovim, and the error names the path as given. ANVIMin a missing folder used to turn into/nvim. bash's "Alarm clock" note now goes to the replay's log, not the terminal. The comment no longer cites a VimLeavePre error, because Neovim exits 0 after one.drain.luaandSKILL.mdnow say "an 8.6 s wait before Claude connects" where they said "handshake".Checks run
The gates ran on 4a06553, with main at d123707. The head then merges main's 37ee1e3 (#554, #564):
diff_inline.lua, the integration runner and diff specs. None of them touches the mention queue or a file of this PR, and all fourcovered.lockfiles match the head. Two results ran on earlier commits:--mutantsran on 3980bc3. Since thencheck.shchanged only in how it readsImmediateWaitsForReady, which still reads TRUE, so each mutant run gets the same TLC input.The results on 4a06553:
verify-mention-queue/check.sh: PASS, 20 facts TRUE.main540,240 distinct states,live-NoStrandedMention115,628,live-ReadyDelivers115,628,live-FlushDelivers48,296. Three counts are exactly twice the old ones andlive-FlushDeliversis 1.96 times (24,692 before), because each run checks both values ofimmediate.verify-mention-queue/check.sh --mutants: exit 0 in 6543 s on a loaded host (load average about 60 to 118). Every guard is caught by the ruleEXPECTnames (ImmediateWaitsForReady=FALSEbySentWhenReady), and every rule breaks at least once.ImmediateWaitsForReady = FALSE,SentWhenReadybreaks./statechartwith the committed view still charts three scratch breaks,StopClearsQueueandFlushWaitsForReadyoff. All 3 exited 1 with a chart.verify-*/check.shpasses:verify-diff-lifecycle: 89,205 / 5,269 states. Its lock merged from main.verify-selection-tracking: 129,986 states.verify-terminal-lifecycle: 263,060 states.init.lua, so I re-recorded theircovered.lockfiles after the fix. Neither model reads_broadcast_at_mention.replays/run.sh: 12 of 12 kept on Neovim v0.8.0 and 12 of 12 on v0.12.3, on the head.NVIM=/nonexistent/nvim,./no-such-nvimornvim-not-on-path, it exits 2 before any replay and names the path.scripts/run_integration_tests_individually.sh: Neovim v0.8.0, 400 successes, 0 failed, 0 errors. Neovim v0.12.3, 537 successes, 0 failed, 0 errors.mention_immediate_send_spec.luapassed 2 of 2 on each version.ImmediateWaitsForReadyreads TRUE on the head. With an unguarded broadcast before the guard (the verifier's probe R4), it reads FALSE.treefmt --ci: 0 files changed.Repro
tests/integration/mention_immediate_send_spec.luais the runnable form.Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:xhigh