fix(diff): answer every openDiff call that is open when Neovim exits by ThomasK33 · Pull Request #558 · coder/claudecode.nvim

ThomasK33 · 2026-11-12T11:44:42Z

Why

The goal is that every openDiff call that reached the server gets one answer when Neovim exits. A pending diff gets DIFF_REJECTED. A call that the exit cut off during its setup gets a -32603 error. Before, two cases left Claude waiting on a connection that then closed with 1001.

Case 1: diffs that no BufUnload reaches. At exit, Neovim fires BufUnload for each loaded buffer before VimLeavePre, and a proposal buffer's BufUnload autocmd rejects its diff. That loop stops as soon as an autocmd deletes the buffer it fired for (src/nvim/main.c in v0.12.3, the bufref_valid check). Three things leave a diff without its BufUnload:

The keep_empty reject of a new-file diff (diff_opts.on_new_file_reject, the default), in a tab that the diff did not open, deletes its proposal buffer. The diffs after it get no BufUnload.
Another plugin's buffer that deletes itself in its own BufUnload stops the loop the same way, so a single diff can lose its BufUnload.
SIGTERM and SIGHUP run VimLeavePre without the loop.

Such a diff reached the VimLeavePre autocmd of diff.lua pending, which removed it without an answer. server.stop then found nothing to reject. The docs verifier found the first case (B1).

Case 2: an exit inside a handler, during setup. A nested = true ClaudeCodeDiffOpened handler that runs :qa! exits Neovim while the openDiff call is still in setup. That call has no response sender yet, because the server stores one only after the tool handler yielded. The exit never unwinds the stack, so the early answer of the setup never leaves. A verifier of this PR found it, and it also exists on origin/main.

Repro with a real WebSocket client that plays Claude (a plugin server, auto_start = true, default diff_opts). The client sends openDiff for a new file (id 1), then for an existing file (id 2):

Neovim 0.12.3, 0.11.5, 0.10.4, 0.9.5, 0.8.0	origin/main	this PR
`qa!` once both diffs are open	`DIFF_REJECTED` for id 1 only, then Close 1001	`DIFF_REJECTED` for id 1 and for id 2, once each, then Close 1001
a handler runs `qa!` during the setup of id 2	`DIFF_REJECTED` for id 1 only, then Close 1001	`DIFF_REJECTED` for id 1, a -32603 error for id 2, then Close 1001

What changed

lua/claudecode/diff.lua. The VimLeavePre callback (now the local cleanup_at_exit) first rejects each diff whose status is pending, oldest first. It runs _resolve_diff_as_rejected under pcall, so one diff that fails to reject cannot leave the others waiting. Then it calls M._cleanup_all_active_diffs("shutdown"). The pass is inline because it has one call site, as AGENTS.md (Code Shape) asks.
lua/claudecode/server/init.lua. _handle_request records each request in M.state.in_flight while its handler runs. M.stop answers every request still recorded with -32603 "Internal error" before it stops the TCP server, and _handle_request sends nothing for a request that stop answered. A call in setup gets this error, and a waiting call keeps getting DIFF_REJECTED from the reject pass.
Tests. Three specs run under mise run test, and one real-Neovim spec runs in the integration runner. One test checks the order of the stop: the -32603 answer must leave before the TCP server stops. See Verification.
Model. verify-diff-lifecycle gets the exit modeled. See Verification.
Docs. The root README.md has one bullet, "Exit answers" (under Global Invariants), that states what Claude gets for each kind of call in each kind of exit. Each fact in it was probed. The other docs describe only the mechanism that they own and link to that bullet: ARCHITECTURE.md (the Resource Cleanup section and the Resource Cleanup bullet under Performance & Security: which autocmd runs what, in which order), lua/claudecode/README.md (the BufUnload loop and the two passes), the server README (what M.stop sends), SKILL.md, check.sh, the comments of diff.lua, and two test headers.
covered.lock of verify-diff-lifecycle records the new hashes of diff.lua and server/init.lua. It was re-recorded on the merged tree each time main moved, after the full check.sh passed. The locks of verify-mention-queue and verify-selection-tracking also cover server/init.lua, so each records its new file hash (see Gates, item 7).

Scope

Not changed:

_cleanup_all_active_diffs. It still removes every entry, in any status. A saved diff is removed at exit as before, and it gets no second answer.
close_pending_diffs in server.stop. It stays for a stop that is not an exit (:ClaudeCodeStop). At exit the diff autocmd runs first, so it finds nothing pending there.
SIGKILL, a crash, and a quit from inside an autocmd that is not nested. They run no VimLeavePre, so no diff gets an answer, Claude's socket closes with 1006, and the lock file stays. No code in the plugin runs then, so the plugin cannot change this. The READMEs say so.

Follow-up PR (after this merges)

README.md (Global Invariants, "Exit answers") says that with "close_window" both diffs have their answers before the first ClaudeCodeDiffClosed fires. That holds for :qa! and SIGTERM, the exits that were probed. For a nested :qa! during the setup of a diff, the call that the exit cuts off gets its -32603 from server.stop, after the ClaudeCodeDiffClosed events. Every call still gets exactly one answer before Close 1001. Every call still gets its answer, so this does not block the merge. A follow-up PR limits that README sentence to waiting calls and says that a call cut off in its setup gets its -32603 after the ClaudeCodeDiffClosed events.
tests/integration/diff_exit_reject_spec.lua skips the unified layout below Neovim 0.9, with the comment "The unified layout needs Neovim 0.9". fix(diff): say the unified layout runs on Neovim 0.8.0, and run its specs there #564, now on main, removed that claim and those skips. The same follow-up PR drops the three skips and the comment, so the 14 unified scenarios also run on v0.8.0 (28 pass there in a trial run).

Blast Radius

Only a call that is open at exit, or a call whose handler a non-exit server.stop interrupts, changes.

A pending diff that gets no BufUnload (an exit through SIGTERM or SIGHUP, or another autocmd that deletes its buffer first) went unanswered on main, and now gets DIFF_REJECTED. A single pending diff that gets its BufUnload behaves as before, because the new pass finds nothing pending.
The ClaudeCodeDiffClosed event of a diff that the new pass rejects carries the reason shutdown. In the vertical and horizontal layouts, a new-file diff with keep_empty in a tab it did not open fires diff rejected (keep_empty) instead, as it does for a BufUnload reject. The unified layout keeps the reason shutdown. That event fires while a later diff is still pending, so a ClaudeCodeDiffClosed handler can see a later diff that is not rejected yet. The README says so.
server.stop answers a request whose handler is still running with an error. Before, an exit inside a handler answered nothing. A stop that is not an exit and runs inside a handler (for example :ClaudeCodeStop from a ClaudeCodeDiffOpened handler) also answered nothing: the handler's result came after the stop, when send_response sends nothing. Now the call gets the error once, before Close 1001.

Verification

Red, then green, run again at the head. The new specs fail on origin/main code and pass with the fix.

Spec	`origin/main` code	This PR
`tests/unit/diff_exit_reject_spec.lua` (6 tests)	4 red, 2 green	6 green
`tests/unit/diff_exit_during_setup_spec.lua` (2 tests: the exit inside a handler, both orders of the two autocmds)	2 red	2 green
`tests/unit/server/in_flight_request_spec.lua` (6 tests)	5 red, 1 green. Two of the red tests, "a finished request" and "a request whose handler raised", fail on main only at `next(server.state.in_flight)`, because the table does not exist there. Main answers those requests correctly, so they guard the new table.	6 green
`tests/integration/diff_exit_reject_spec.lua` (28 scenarios, a child Neovim does the real exit)	11 red, 17 green on 0.12.3, 0.11.5, 0.10.4 and 0.9.5. On 0.8.0, 7 red and 7 green (14 run)	all green on all five versions

The integration scenarios are 20 for :qa! (split and unified layout, keep_empty and close_window, 5 open orders), 4 for SIGTERM and for a buffer that deletes itself in its own BufUnload (both layouts), and 4 for the exit inside a handler (both layouts). On Neovim 0.8.0 the unified layout is pending, so 14 run there.

Mutants of the code (one edit each), against the three unit specs and the integration spec on Neovim 0.12.3:

Mutant	unit red	integration red
`M.stop` answers nothing	5	4
`M.stop` sends the answer after `stop_server`, or after `M.state.server = nil` (it never reaches Claude)	1	0
`M.stop` keeps the entry, so the handler sends a second answer	2	0
`_handle_request` sends after a stop	2	0
`_handle_request` never removes an entry	4	2
the reject pass sorts by tab name, not by open order	1	0
the reject pass skips unified diffs	0	2
no reject pass, or the pass after the cleanup	5	7

Probes of the exit facts. A real WebSocket client plays Claude: it sends openDiff for a new file (id 1), then for an existing file (id 2). A ClaudeCodeDiffClosed handler logs the status of every diff. Each scenario ran at the head 43fc68d619e218995dbba2fc07a128c6ff1fbaee on Neovim 0.12.3, 0.11.5, 0.10.4, 0.9.5 and 0.8.0, and gave the same result on all five:

Scenario	Claude gets	Close	Lock file left
`:qa!`	id 1 and id 2 `DIFF_REJECTED`, once each	1001	no
SIGTERM, or SIGHUP	the same	1001	no
id 1 accepted (`FILE_SAVED`), then `:qa!`	id 1 `FILE_SAVED` once, id 2 `DIFF_REJECTED` once	1001	no
a nested `ClaudeCodeDiffOpened` handler runs `:qa!` during the setup of id 2	id 1 `DIFF_REJECTED`, id 2 a -32603 error, once each	1001	no
the same handler runs `:ClaudeCodeStop`, which is not an exit	the same	1001	no
SIGKILL	nothing	1006	yes
`:qa!` inside an autocmd that is not `nested`	nothing	1006	yes

Order of ClaudeCodeDiffClosed, with one new-file diff and one existing-file diff, in the vertical and horizontal layouts, for :qa! and SIGTERM (40 runs). With keep_empty, the handler of the new-file diff runs while the existing-file diff is still pending. With close_window, both diffs are rejected before the first ClaudeCodeDiffClosed fires. A crash was not probed, and SIGKILL stands in for it.

Order of the two VimLeavePre autocmds. A probe fixed the order that ARCHITECTURE.md states. A real WebSocket client holds two open diffs, tracer autocmds sit before and after setup, and wrappers log each call. All 15 runs gave one sequence: the BufUnload loop answers the first diff, tracer 1, the diff.lua autocmd (the reject pass of cleanup_at_exit answers the second diff, then _cleanup_all_active_diffs("shutdown")), the init.lua autocmd (stop, lockfile.remove, tcp.stop_server), tracer 2. The runs cover Neovim 0.12.3, 0.11.5, 0.10.4, 0.9.5 and 0.8.0, each with a plain setup, a second setup call, and claudecode.diff loaded before setup. The client got DIFF_REJECTED for ids 1 and 2, then close code 1001, and no lock file stayed. The order holds because M.setup loads diff.lua before it registers its own autocmd.

Model (verify-diff-lifecycle). The exit was not modeled, and the model's Idle condition excluded a call in setup, so the model could not see the case 2 gap. The model now has the action ExitInSetup (an exit inside an opened handler during one call's setup), the fact ExitAnswersInFlight (read by check.sh from _handle_request and M.stop), and the rule ExitedCallsAnswered. A call that nothing answered gets the new phase gone. From the first round the model also has DiffCleanupAtExit and the fact ExitRejectsPending.

check.sh --mutants ends with every guard is caught. ExitAnswersInFlight=FALSE is caught by ExitedCallsAnswered, so the action is reachable and the old behavior breaks the rule. ExitRejectsPending=FALSE is caught by NoStrandedCall and DisconnectedCallsAnswered. Every other guard is caught as before, and no rule is vacuous.
After --record, check.sh reports PASS: main: pass (93477 distinct states found) and live-DisconnectedCallsAnswered: pass (5557 distinct states found). Before this PR the counts were 89205 and 5269. check.sh --hash-only reports covered.lock matches the code.

The model runs the two VimLeavePre autocmds of an exit in setup in one order, and it does not model a ClaudeCodeDiffClosed handler in the exit pass or a saved diff lost at exit, because Neovim quits right after. SKILL.md says so.

Gates. The head is 43fc68d619e218995dbba2fc07a128c6ff1fbaee. It merges origin/main at f7f89cb5. Items 1 to 5 and 7 ran at that head, on a host where nothing else of mine ran:

mise run all (BUSTED_SEED=97531) exits 0. 1751 successes, 0 failures, 0 errors, 29 pending. luacheck: 0 warnings, 0 errors in 189 files. The 29 pending tests need a real Neovim.
The unit specs of the diff and server modules (484 tests) exit 0 with 0 not ok. The three new specs in shuffled order, seeds 1 to 6: each exits 0 with 14 ok.
scripts/run_integration_tests_individually.sh exits 0 on Neovim 0.12.3 (Total Success 555, Failed 0, Errors 0) and on Neovim 0.8.0, the version of the integration-tests (v0.8.0) job (Total Success 404, Failed 0, Errors 0).
mise run format-check (430 files, 0 changed) and check.sh --hash-only exit 0. The full check.sh exits 0 with main: pass (93477 distinct states found) and live-DisconnectedCallsAnswered: pass (5557 distinct states found).
ExitRejectsPending is the only fact of check.sh that reads the reject pass. This is with check.sh as it stands at the head. It reads TRUE at the head. With the pass removed from cleanup_at_exit, or moved after the cleanup, it reads FALSE, check.sh exits 1, and NoStrandedCall and DisconnectedCallsAnswered break.
check.sh --mutants of verify-diff-lifecycle ends with every guard is caught. It caught ExitRejectsPending=FALSE by NoStrandedCall and DisconnectedCallsAnswered, and ExitAnswersInFlight=FALSE by ExitedCallsAnswered. An independent verifier ran it on a clean checkout of the head 43fc68d6 (exit 0, 22 guard rows caught).
CI runs the check.sh of all four verify-* skills. verify-mention-queue and verify-selection-tracking cover lua/claudecode/server/init.lua, and their locks went stale. Only the file hash changed in each. No covered block changed. The change cannot reach a queue, a timer, the handshake, a broadcast or the selection state: M.stop sends the response of a request whose handler still runs, before it stops the TCP server. The full check.sh of each skill passes (mention queue: main 270120 distinct states, three live properties; selection tracking: main 129986). The 12 mention-queue replays all kept their promise, among them restart-leak and stop-in-wait, which go through M.stop. The four --hash-only runs exit 0. Both locks were recorded again after the last commit, which only wraps a comment in server/init.lua.

Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

At exit Neovim fires BufUnload for each loaded buffer before VimLeavePre, and a proposal buffer's BufUnload autocmd rejects its diff. That loop stops as soon as an autocmd deletes the buffer it fired for. The keep_empty reject of a new-file diff deletes its proposal buffer, so the diffs behind it got no BufUnload. They reached the VimLeavePre autocmd pending, which removed them without an answer, and server.stop then found nothing to reject. Claude waited on an openDiff that was never answered. The VimLeavePre callback now rejects every diff that is still pending, oldest first, before it removes any entry. A diff that a BufUnload already rejected is skipped, so each openDiff gets one answer. One diff that fails to reject cannot leave the others waiting. The new caller resolves diffs, so the verify-diff-lifecycle model gets an exit action and a fact for the guard: the fact set to FALSE breaks NoStrandedCall and DisconnectedCallsAnswered, and check.sh --mutants catches every guard. covered.lock records the new hash. A unit spec drives the VimLeavePre callback over the states exit can leave. An integration spec runs a real :qa! in a child Neovim for 20 scenarios.

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

luacheck reports senders as mutated but never accessed.

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

A nested ClaudeCodeDiffOpened handler that runs :qa! during the setup of an openDiff exits Neovim with that call pending and no response sender yet, because the server stores the sender only after the tool handler yielded. The exit never unwinds the stack, so the early answer of the setup never left. Claude got the answers of the earlier calls, then Close 1001. _handle_request now records each request in M.state.in_flight while its handler runs. M.stop answers every request still recorded with -32603 before it stops the TCP server, and _handle_request sends nothing for a request that stop answered. The reject pass at exit then needs no sender of its own: a call in setup gets the error, a waiting call gets DIFF_REJECTED. The model gets the action ExitInSetup, the fact ExitAnswersInFlight and the rule ExitedCallsAnswered, so Idle no longer hides this case. With the fact FALSE, ExitedCallsAnswered breaks, and check.sh --mutants catches every guard. covered.lock records the new hashes. Verifier findings of the first round: - Order assertion: the unit spec opens c.txt, a.txt and b.txt, so a sort by tab name no longer passes. - SIGTERM, a buffer that deletes itself in its own BufUnload, and the unified layout in the exit pass each get an integration scenario. - Docs: the keep_empty reject deletes its proposal buffer only in a tab the diff did not open. SIGTERM and SIGHUP run VimLeavePre without the BufUnload loop, and SIGKILL or a crash runs no VimLeavePre. - SKILL.md: exit is modeled, and the two exit actions are separate actions. - The README sections the docs refresh wrote now state the fixed behavior.

…-pending-diff-at-exit

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

The verifiers of the second round found two README lines that the PR made false, three wording slips and one test gap. - server README: M.state lists in_flight. - README.md and lua/claudecode/README.md: not every exit answers each pending diff. A quit from inside an autocmd that is not nested runs no VimLeavePre, like SIGKILL or a crash: Claude gets no answer, its socket closes with 1006, and the lock file stays. A pending diff whose setup has not finished gets -32603, not DIFF_REJECTED. Each sentence was checked against a probe on Neovim 0.8.0 to 0.12.3. - server/init.lua: the comment names a nested ClaudeCodeDiffOpened handler. - SKILL.md: a handler that runs :ClaudeCodeStop is not modeled. - A new unit test records what reaches the socket and asserts that stop sends the -32603 answer before it stops the TCP server. A move of that answer after stop_server or after M.state.server = nil passed every test and left the call unanswered on a real socket. covered.lock records the new hash of server/init.lua.

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

ARCHITECTURE.md named only the ClaudeCodeShutdown autocmd of init.lua. A second VimLeavePre autocmd, in the ClaudeCodeMCPDiff group of diff.lua, now answers every pending openDiff call with DIFF_REJECTED before it closes the diffs. The section now names both, says what each one does, and gives the order they run in. A probe fixed the order: 15 runs (Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5, 0.12.3; default, a second setup call, and diff.lua loaded before setup) with tracer autocmds before and after setup gave BufUnload loop, tracer 1, the diff.lua autocmd (_reject_pending_diffs, then _cleanup_all_active_diffs), init.lua stop (lockfile.remove, tcp.stop_server), tracer 2. The Security Considerations bullet names both autocmds, and says that a SIGKILL, a crash, or a quit from inside a non-nested autocmd skips both.

Three rounds of review found a false claim about what Claude gets at an exit, each time in another file, because each doc restated the rule in its own words. Round c found two more: ARCHITECTURE.md said the diff.lua autocmd answers every pending call with DIFF_REJECTED, but a call that the exit cuts off during its setup gets a -32603 error from the server stop (its reject stays in setup_result and sends nothing). README.md said that every pending diff is rejected before any is removed, but a keep_empty reject removes its own diff, so a ClaudeCodeDiffClosed handler can see a later diff still pending. The root README now has one bullet, "Exit answers", that states what each kind of call gets, in each kind of exit, with only probed claims. The other docs describe the mechanism they own and link to it: ARCHITECTURE.md (which autocmd runs what, in which order), lua/claudecode/README.md (the BufUnload loop and the two passes), lua/claudecode/server/README.md (what M.stop sends), SKILL.md and check.sh (what the model reads), and two test headers. Two comments in diff.lua said the same wrong thing and now describe the mechanism. The change to diff.lua is comments only: the lines that are not comments are identical to the previous head. covered.lock records the new file hash.

…r the user A call still in setup gets a -32603 error from the stop. The root README lists it under Exit answers.

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

AGENTS.md (Code Shape, #552) puts a function on a module table only when another module, the documented API or Neovim calls it. reject_pending_diffs has one caller, the module-local cleanup_at_exit, and no test calls it, so it is now a local function. The behavior is identical. The names change in check.sh (three regexes), SKILL.md, the model comments, the READMEs and ARCHITECTURE.md. covered.lock records the new hashes of the renamed blocks.

The root README said every exit fact was probed on Neovim 0.8.0 and 0.12.3. A probe set on the final code now covers each fact on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3: :qa!, SIGTERM, SIGHUP, SIGKILL, a quit from a non-nested autocmd, a call cut off in setup, :ClaudeCodeStop from such a handler, a saved diff at exit, and the ClaudeCodeDiffClosed order with keep_empty and close_window in the vertical and horizontal layouts. A crash was not probed, and SIGKILL stands in for it. The README named only the vertical layout for the early removal of a new-file diff with keep_empty. The horizontal layout does the same, so the sentence says both. The header of the exit integration spec now names the four exits that it runs and the ones that it does not.

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock # lua/claudecode/README.md

ThomasK33 · 2026-11-12T11:44:49Z

@codex review

ThomasK33 · 2026-11-12T11:44:54Z

@codex security review

chatgpt-codex-connector · 2026-11-12T11:45:04Z

Codex Review Summary: ✅ Completed

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-12T13:25:35.925913Z	`43fc68d`	Manual request
🔒 Security Review	✅ Completed 2026-11-12T13:25:51.687517Z	`43fc68d`	Manual request

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector · 2026-11-12T11:48:23Z

Codex Review: Didn't find any major issues. Swish!

Reviewed commit: b0fbbead58

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

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".

chatgpt-codex-connector · 2026-11-12T11:48:46Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: b0fbbead58

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

…ks after the server stop change Both models cover lua/claudecode/server/init.lua, which this PR changes in M._handle_request and M.stop. Only the file hash changed in each lock. No covered block changed, and the change cannot reach a queue, a timer, the handshake, a broadcast or the selection state: M.stop now sends the response of a request whose handler is still running, before it stops the TCP server. The full check.sh of each skill passes (mention queue: main 270120, live 57814/57814/24692 distinct states. selection tracking: main 129986). The twelve mention-queue replays all kept their promise, among them restart-leak and stop-in-wait, which go through M.stop.

ThomasK33 · 2026-11-12T12:11:03Z

@codex review

ThomasK33 · 2026-11-12T12:11:08Z

@codex security review

chatgpt-codex-connector · 2026-11-12T12:15:25Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 9e3e0aa3b2

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9e3e0aa3b2

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

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".

… wrap the long lines Codex review, round 2, on 9e3e0aa: 1. AGENTS.md (Code Shape, one-off logic) keeps a single-use function only when it is recursive, a named algorithm, or when inlining adds flags or two levels of nesting. reject_pending_diffs had one caller, and inlining it adds none of those, so its body now sits in cleanup_at_exit. The behavior is identical. check.sh reads the loop from the cleanup_at_exit block (the reject_pending block is gone), and the docs and model comments name cleanup_at_exit. 2. One comment line in server/init.lua was 131 columns wide. It and three other added Lua lines over 120 columns, in two test files, are wrapped. The three covered.lock files that cover the changed files are re-recorded after the full check.sh of each skill passed.

ThomasK33 · 2026-11-12T13:22:05Z

@codex review

ThomasK33 · 2026-11-12T13:22:09Z

@codex security review

chatgpt-codex-connector · 2026-11-12T13:25:34Z

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 43fc68d619

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

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".

chatgpt-codex-connector · 2026-11-12T13:25:50Z

🛡️ Codex Security Review

Security review completed. No security issues were found in this pull request.

Reviewed commit: 43fc68d619

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

You comment "@codex security review"
A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

Keep this branch's keepalive paragraph in lua/claudecode/server/README.md and take main's new notification, deferred-response and in-flight bullets. Take main's verify-diff-lifecycle covered.lock and record the three locks that the comment edits of tcp.lua and main's server/init.lua changes (#539 on_open log, #558 in-flight replies in M.stop) made stale: verify-diff-lifecycle, verify-mention-queue and verify-ws-connection. The ws model still fits: the in-flight replies are ordinary writes to a connected client before stop_server.

… exit answers docs (coder#572) ## Why Keep the exit tests and the "Exit answers" docs true after coder#558 and coder#564. 1. coder#564 made the unified layout work on Neovim 0.8.0 and removed the "needs Neovim 0.9" skips from eight specs. `diff_exit_reject_spec.lua` came in with coder#558 and still skipped the unified layout below 0.9 in three places. So 14 unified exit scenarios stayed pending in the v0.8.0 job, and the file kept a comment that is no longer true. 2. The advisor and the verifier of coder#558 found README sentences that say more than the code does. They concern the exits that run no `VimLeavePre`. ## What changed - `tests/integration/diff_exit_reject_spec.lua`: - The three skips and the comment "The unified layout needs Neovim 0.9" are gone. - Three new cases (each in the vertical and unified layouts) start the exit inside an autocmd, with two waiting calls. A direct `:qa!` in an autocmd that is not `nested`, and SIGTERM while such an autocmd waits in `vim.wait`: no call is answered. A direct `:qa!` in a `nested` autocmd: both calls get `DIFF_REJECTED`. Each case first checks that both calls were waiting. The two no-answer cases also check that the child ended by itself. - The spec has 34 passes on Neovim 0.8.0 and 34 on 0.12.3. On main it has 14 passes and 14 pending on 0.8.0, and 28 passes on 0.12.3. - `README.md`, Global Invariants, "Exit answers": - The `"close_window"` sentence now says "waiting calls". A call that a nested `:qa!` cuts off during its `openDiff` setup has no response sender yet. The server stop answers it with -32603 after the `ClaudeCodeDiffClosed` events. Every call still gets one answer before close code 1001. - The sub-bullet for exits without `VimLeavePre` keeps SIGKILL, a crash and a `:qa!` from inside an autocmd that is not `nested`, as on main, and adds `:noautocmd qa!` and a Lua `os.exit()`, which also run no `VimLeavePre`. It adds one rule: a `:qa!`, SIGTERM or SIGHUP that Neovim handles while an autocmd that is not `nested` is still running can end Neovim without `VimLeavePre` too. A synchronous LSP format on save, which waits in `vim.wait`, is the common example. It says "can" because Neovim looks only at the autocmd that runs when it handles the exit, so a `nested = true` handler that such an autocmd started (with `:doautocmd` or `nvim_exec_autocmds`) still gets `VimLeavePre`. It promises nothing for a signal during a plain Lua loop, because Neovim handles a signal only at its next event check. - `ARCHITECTURE.md`, `lua/claudecode/README.md` and the comment of `cleanup_at_exit` in `lua/claudecode/diff.lua` say the same. ## Scope Tests and docs. The only change under `lua/` is that comment in `diff.lua`. `verify-diff-lifecycle` passes (93,477 distinct states, and 5,557 for the live case), and its `covered.lock` records the new file hash. The plugin does not answer calls in the exits that the README lists as running no `VimLeavePre` (SIGKILL, a crash, `:noautocmd qa!`, `os.exit()`, and `:qa!` in an autocmd that is not `nested`), because none of its exit code runs in them. The docs say so. ## Blast Radius None at runtime. The v0.8.0 CI job runs 20 more tests of this spec, and the stable job runs 6 more. ## Verification - Spec on Neovim 0.8.0 and 0.12.3: 34 passes, 0 failures, in 5 of 5 runs on each version, and in 3 of 3 runs again after the last commits, which change comments, docs and the lock only. Mutants: - The autocmd's `:qa!` replaced by a no-op: the first no-answer case is red on both versions (the file then runs into the runner's 40 s limit, because each affected case waits 20 s). - `cleanup_at_exit` returns at once: 8 cases are red on both versions, among them the nested `:qa!` case in the vertical layout. The no-answer cases stay green, because they pin what Neovim does. A Neovim that changes it turns them red, and the README has to change. - Probes on 0.8.0 and 0.12.3 (vertical and unified, two waiting calls, 6 runs per row, a `VimLeavePre` marker and the answers in one log). In an autocmd that is not `nested`, each of these runs no `VimLeavePre` and answers no call, in all 54 runs per version: a direct `:qa!`, a timer `:qa!` during `vim.wait`, SIGTERM and SIGHUP during `vim.wait`, SIGTERM and SIGHUP in the Lua part of a handler that waits later, SIGTERM in the first of two handlers when the second waits, SIGTERM in a Vim script loop, and SIGTERM in a `:%s` loop. In a `nested = true` autocmd the same cases answer both calls. With no autocmd, a timer `:qa!`, SIGTERM and SIGHUP answer both calls (18 of 18). `:noautocmd qa!` and a Lua `os.exit()` from a timer run no `VimLeavePre` and answer no call (9 of 9 on each version, three layouts), and a plain `:qa!` and `:cq` run it and answer both calls (9 of 9). A non-nested autocmd that starts a `nested = true` handler which waits in `vim.wait`, with SIGTERM during the wait, runs `VimLeavePre` and answers both calls (6 of 6 on each version). - Waiting calls with `close_window`, `:qa!` and SIGTERM, three layouts: both answers come before the first `ClaudeCodeDiffClosed` (6 of 6 on each version). A nested `:qa!` that cuts a call off in its setup: the -32603 comes after every `ClaudeCodeDiffClosed` event (12 of 12 on each version), and no id is answered twice. - Independent reads with a real WebSocket client on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3: a verifier (330 runs), an advisor (225 runs) and two claim checks (375 runs in the first, and 140 runs for the nested-handler case in the second). They found that the first wording dropped the direct `:qa!` case, that the second promised `VimLeavePre` for a signal during a Lua loop, and that "ends" is false when the running autocmd started a `nested` handler. The sub-bullet above says only what survives all three, with "can". A last narrow check found only that "Without `VimLeavePre`" was too general, because `eventignore` can skip `VimLeavePre` and a `:qa!` still rejects diffs while buffers unload. The README now says "In these exits". - At the head after the merge of main (coder#573): `mise run format-check` and `mise run all` pass (1892 successes, 0 failures, 0 errors, 35 pending), and the integration runner passes on 0.12.3 (844) and on 0.8.0 (840). The commits of this PR change comments, docs, the spec header and the lock only. `check.sh --hash-only` passes for the four verify skills, and the full `verify-diff-lifecycle` check passes (93,477 and 5,557 states). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

… 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`_

…iff is replaced (coder#536) ## Why Claude waits for an answer to every `openDiff`. When the plugin never answers a call, Claude waits forever. One order on `main` leaves a call without an answer. A handler of the user runs the event loop (`vim.wait`), so that Claude's queued second call for the same tab name runs inside it. The verifiers of coder#512 found this order while they checked a candidate. That candidate newly reaches it, but `main` has it without any of its code, so I fix it here first. **A close handler.** An `openDiff` A for a tab name replaces the open diff X. A `ClaudeCodeDiffClosed` handler of the user runs the event loop while X closes, so a queued call B registers a diff for the tab name. When X is a new file, A then cleans up the diff that is registered for the tab name, and that is B's. Nothing answers B, and its tab or windows can stay. When X is an existing file, B can instead stay open with no answer, or A fails with E95. When X is an existing file and B shares A's proposal name, A fails with E95 as well, and A's failure cleanup removes B the same way. ## What changed 1. The replace step of `open_diff_blocking` is a loop. It rejects the diff that is registered for the tab name (if it is pending) and cleans it up, as before, and repeats while another diff is registered. It cleans up only the diff that it handled, so a diff that registered meanwhile is never removed without an answer. Each pending call that A replaces gets one `DIFF_REJECTED` answer, B included, and A sets up on a free tab name. The change is 11 added and 5 removed lines in `lua/claudecode/diff.lua`. 2. `tests/integration/diff_answer_every_call_spec.lua` has 9 cases. Four of them run the close handler order in both layouts, with X a new file and with X an existing file. Five pin what `main` does today after a plugin reload inside a setup (see "A reload" below). 3. `lua/claudecode/README.md` and the `verify-diff-lifecycle` skill describe the loop. The skill lists the order as not modeled, its `ReplaceRejects` and `ReplaceKeepsOthersSaved` facts read `while existing_diff do`, and `covered.lock` has the new hashes. **A reload.** An earlier version of this PR also registered a diff in the new module after a plugin reload inside a setup. I removed that step. A reload inside a setup behaves as on `main`, with and without the event loop in the reload: the diff finishes its setup in the old module, so `:ClaudeCodeDiffAccept`, `:ClaudeCodeDiffDeny` and `:ClaudeCodeCloseAllDiffs` of the new module do not reach it. `:w`, `:q` and `:bwipeout!` in its window still answer it, and the user can end it from there. This PR does not promise one `ClaudeCodeDiffClosed` per diff after a reload, because `main` does not either. Every order that the scenarios below cover, except the close handler order, ends as it does on `main`. ## Evidence Real headless Neovim, one instance per scenario, `tools.handle_invoke` and the real commands, a stub in place of the `claude` CLI. The rows below come from the head before the last main merge (`c7d4f61b`) and `origin/main` at `48ca93be`. On the final head `b001b741`, which merges `origin/main` at `f28eba7d`, an independent verifier reran the close handler probe (0 of 224 runs with a problem, 220 of 224 on `main`) and a probe of the newly merged split and CRLF paths. No row is worse than `main`. Neovim 0.12.3 and v0.8.0 give the same rows. | Order | `main` | this head | | --- | --- | --- | | Close handler, split layout, X a new file | X rejected, B never answered, A opens | X and B rejected, A opens and is answered at accept | | Close handler, split layout, X an existing file | A fails with E95, B never answered, 2 tabs | X and B rejected, A opens, 1 tab | | Close handler, unified layout, X new or existing, with or without a leftover buffer | B never answered | B rejected, A opens | | Close handler, split layout, with a leftover buffer, B an existing file that shares A's proposal name | A and B fail with E95 | same as `main` | | Close handler, split layout, with a leftover buffer, B a new file | A fails with E95, B never answered, 2 tabs | A fails with E95, B rejected, 1 tab | | Reload inside A's setup (every reload scenario) | unchanged | same as `main` | **Spec.** 9 cases. On `main`, 4 fail and 5 pass, on both Neovim versions. The 4 that fail are the close handler order: `answers a call that a ClaudeCodeDiffClosed handler lets register while the old new-file diff is replaced` and the same title with `existing-file`, each in the vertical and the unified layout. The 5 that pass are the controls: `:w` in A's window after a reload answers A once, and `:q` or `:bwipeout!` on a new-file proposal after a reload, with and without the event loop in the reload, fires one open and one close event, also after `close_tab` and close-all. This head passes all 9. **Mutation.** 6 mutants of the loop, all red on both Neovim versions: the replace step runs once, it cleans up what it did not handle, it does not read the registry again, it does not reject a pending diff, it does not clean up, and it rejects only on the first pass. Removing the `assert` after the cleanup changes no result, because it only states what the cleanup already did. **Reload equals `main`.** The verifier's N1 spec (a reload inside A's setup, a queued call B in the new module, and a close handler that closes A's window) gives the same rows on `main` and on this head, on both versions (2 cases, both pass). The verifier's D1 probe (a reload inside A's setup, then `:q`, `:bwipeout!`, deny or write in A's window, then `close_tab`; 16 runs per tree) gives the same 16 rows on both trees. **Other orders.** I ran 776 scenarios on `main` and on this head, on both versions (1552 runs per tree): the 657 scenarios of the first verifier of coder#512 (the core set, the event matrices with and without notifications, three-deep, three queued calls, the window orders, the V3 orders and the reload-after-action orders), the reload, I1, V2, W1, N1, three-deep and three-queued scripts of the second verifier and its 90-scenario harness, and my own close handler orders. 1538 runs give the same output on both trees. 14 differ, which are 7 scenarios on each version, and all 7 are the close handler order: the four split and unified orders without a leftover buffer, the two unified orders with one, and `f3_diffclosed_pump`. In each, `main` leaves a call unanswered and this head answers every call once with its own text and leaves no extra window or tab. **Gate** on the final head (`b001b741`, which contains `origin/main` at `f28eba7d`, coder#558 and coder#573 included): `mise run clean && mise run all` exit 0 (1904 successes, 0 failures, 37 pending, luacheck 0 warnings in 201 files). The spec runs 9 of 9 on Neovim 0.12.3 and on v0.8.0. The coder#558 specs pass too: `tests/unit/diff_exit_reject_spec.lua` 6 of 6, and `tests/integration/diff_exit_reject_spec.lua` 34 of 34 on both versions. The coder#573 specs `diff_close_save_spec` (77 of 77) and `diff_left_window_spec` (40 of 40) pass on both versions. The integration runner passes with 865 successes and 0 failures on Neovim 0.12.3 and 861 and 0 on v0.8.0, each also under a `TMPDIR` with a space and a `%`. `check.sh` PASS (93477 and 5557 states) and `--hash-only` is fresh for all five verify skills. The 6 mutants of the loop are red on both versions. On `main` the spec fails 4 of 9 cases and passes 5. ## Not in this PR - A reload inside a setup, and a reload after a setup has finished: the old module keeps the diff, as the module README says. A fix needs a design for what the new module may take over. The leftover-buffer case is coder#512's. - A `WinClosed`, `BufWipeout` or `BufHidden` handler that runs the event loop while the diff X is cleaned up (not in the `ClaudeCodeDiffClosed` event) also lets B register. The last step of `_cleanup_diff_state` then removes B without an answer in some variants (a `BufWipeout` or `BufHidden` handler on a new file still answers B), and X's `ClaudeCodeDiffClosed` fires twice, on `main` and on this head. A guard on that step reaches every cleanup, not only a replace, so it changes more orders than the one here. - A second `openDiff` that registers while the first one is still inside its setup in the same module, without a reload: B is never answered and an extra tab can stay, on `main` and on this head. coder#512 handles it with a refusal. - The four leftovers that the last verifier found (the `accept_other` order, one SKILL.md line, a `FileType` handler that closes the proposal window during setup, and a call that registers during exit) are tracked in coder#603. The last two are on main too. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 added 17 commits November 12, 2026 01:57

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

be441d1

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

test(diff): drop an unused variable from the exit spec

e94d6b1

luacheck reports senders as mutated but never accessed.

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

1c384b7

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

4aa89f0

…-pending-diff-at-exit

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

a81f6cf

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

d5a74ff

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

f055e1e

…-pending-diff-at-exit # Conflicts: # lua/claudecode/README.md

docs(verify): say that a stop answers the openDiff calls that wait fo…

ddb5253

…r the user A call still in setup gets a -32603 error from the stop. The root README lists it under Exit answers.

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

a1acf2c

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock

Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…

b0fbbea

…-pending-diff-at-exit # Conflicts: # .agents/skills/verify-diff-lifecycle/covered.lock # lua/claudecode/README.md

chatgpt-codex-connector Bot reviewed Nov 12, 2026

View reviewed changes

Comment thread lua/claudecode/diff.lua Resolved

Comment thread lua/claudecode/server/init.lua Resolved

ThomasK33 added this pull request to the merge queue Nov 12, 2026

Merged via the queue into main with commit 48ca93b Nov 12, 2026
9 checks passed

ThomasK33 deleted the fix/diff-answer-every-pending-diff-at-exit branch November 12, 2026 17:04

github-actions Bot mentioned this pull request Nov 12, 2026

chore(release): 0.5.0 #444

Open

ThomasK33 mentioned this pull request Nov 12, 2026

feat(skills): add verify-ws-connection, a TLA+ model of the WebSocket connection lifecycle #474

Merged

Conversation

ThomasK33 commented Nov 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why

What changed

Scope

Follow-up PR (after this merges)

Blast Radius

Verification

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ThomasK33 commented Nov 12, 2026 •

edited

Loading

chatgpt-codex-connector Bot commented Nov 12, 2026 •

edited

Loading