Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
b956792
fix(diff): answer every pending openDiff when Neovim exits
ThomasK33 Nov 12, 2026
be441d1
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
e94d6b1
test(diff): drop an unused variable from the exit spec
ThomasK33 Nov 12, 2026
1c384b7
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
1b89edc
fix(server): answer a call that an exit cut off during its setup
ThomasK33 Nov 12, 2026
4aa89f0
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
a81f6cf
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
cbc8b2f
docs(server): state what an exit answers, and test the order of the stop
ThomasK33 Nov 12, 2026
d5a74ff
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
f055e1e
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
f2862a7
docs: name both VimLeavePre autocmds in the Resource Cleanup section
ThomasK33 Nov 12, 2026
4179747
docs: state the exit answers once, in the root README
ThomasK33 Nov 12, 2026
ddb5253
docs(verify): say that a stop answers the openDiff calls that wait fo…
ThomasK33 Nov 12, 2026
a1acf2c
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
68fa74d
refactor(diff): make the exit reject pass a local function
ThomasK33 Nov 12, 2026
f2867bf
docs: scope the exit probes per fact and name what the exit spec covers
ThomasK33 Nov 12, 2026
b0fbbea
Merge remote-tracking branch 'origin/main' into fix/diff-answer-every…
ThomasK33 Nov 12, 2026
9e3e0aa
chore(skills): re-record the mention-queue and selection-tracking loc…
ThomasK33 Nov 12, 2026
43fc68d
refactor(diff): inline the exit reject pass into cleanup_at_exit, and…
ThomasK33 Nov 12, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .agents/skills/verify-claudecode-nvim/features/server.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ claudecode.nvim runs a WebSocket server on `127.0.0.1` and writes a lock file, `

- `server-status` `:ClaudeCodeStatus` prints `Claude Code integration is running on port <port>` or `Claude Code integration is not running`.
- `server-lock` the lock file is mode `0600` in a `0700` folder and holds nvim's `pid`, `ideName` `Neovim`, `transport` `ws`, the cwd in `workspaceFolders`, and a 32-character hex `authToken`.
- `server-stop` `:ClaudeCodeStop` deletes `<port>.lock`, answers each pending openDiff with `DIFF_REJECTED`, closes each client with code 1001, and prints `Claude Code integration stopped`.
- `server-stop` `:ClaudeCodeStop` deletes `<port>.lock`, answers each openDiff that waits for the user with `DIFF_REJECTED`, closes each client with code 1001, and prints `Claude Code integration stopped`.
- `server-start` `:ClaudeCodeStart` listens on a new random port, writes a new lock file with a new token, and prints `Claude Code integration started on port <port>`.
- `server-twice` Start while running warns `Claude Code integration is already running on port <port>`. Stop while stopped warns `Claude Code integration is not running`.
- `server-exit` quitting Neovim deletes the lock file.
Expand Down
11 changes: 8 additions & 3 deletions .agents/skills/verify-diff-lifecycle/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Claude calls `openDiff` and blocks until the plugin answers. If the plugin never
| `SavedDiffKept` | Only Claude tears down a diff the user accepted with `:w`, and never after its own client is gone. The user can too, once the file or its buffer holds the accepted text. | The user's accepted edits vanish before Claude writes them. |
| `DisconnectedCallsAnswered` | A disconnected client's waiting calls get answered without the user. | Orphaned diff windows linger (issue #248). |
| `NoRejectedLeftover` | A bulk close also closes a diff from its list that a `ClaudeCodeDiffClosed` handler denied while the loop ran. | The denied diff's windows linger after `:ClaudeCodeCloseAllDiffs`, a disconnect, or a server stop. |
| `ExitedCallsAnswered` | A call that an exit of Neovim cut off during its setup has been answered, by the server stop. | Claude waits on a call whose connection closes with no answer. |

## Run

Expand Down Expand Up @@ -54,7 +55,7 @@ The record has one group of lines per file: a `== <file>` header, the file's has

Covered blocks:

- In `diff.lua`: `_resolve_diff_as_saved`, `_resolve_diff_as_rejected`, `open_diff_blocking`, `_setup_blocking_diff`, `close_diff_by_tab_name`, `close_pending_diffs`, `close_diffs_for_client`, `close_active_diffs`, `_cleanup_all_active_diffs`, `_register_diff_state`, `_cleanup_diff_state`, `register_diff_autocmds` (the `:w` and buffer-delete paths), `_write_proposal` (what a write of the proposal does), `_register_reject_when_hidden` (the `:q` and buffer-switch paths, shared by both layouts), `fire_diff_event`, `accept_current_diff`, `deny_current_diff`.
- In `diff.lua`: `_resolve_diff_as_saved`, `_resolve_diff_as_rejected`, `open_diff_blocking`, `_setup_blocking_diff`, `close_diff_by_tab_name`, `close_pending_diffs`, `close_diffs_for_client`, `close_active_diffs`, `_cleanup_all_active_diffs`, `cleanup_at_exit` (the `VimLeavePre` callback), `_register_diff_state`, `_cleanup_diff_state`, `register_diff_autocmds` (the `:w` and buffer-delete paths), `_write_proposal` (what a write of the proposal does), `_register_reject_when_hidden` (the `:q` and buffer-switch paths, shared by both layouts), `fire_diff_event`, `accept_current_diff`, `deny_current_diff`.
- In `diff_inline.lua`: `setup_inline_diff`, `resolve_inline_as_saved`, `resolve_inline_as_rejected`.
- In `server/init.lua`: `M.stop`, `on_disconnect`, `M._handle_request`, `M._setup_deferred_response`.
- In `tools/init.lua` and `tools/open_diff.lua`: `M.handle_invoke`, and the openDiff `handler`.
Expand All @@ -76,6 +77,8 @@ A changed file with no changed block or call site still needs a look. A wrapper
| `CloseTabRejectsPending` | `close_diff_by_tab_name` rejects a pending diff before cleanup |
| `CloseEachByName` | `close_active_diffs` closes each match through `close_diff_by_tab_name` |
| `StopRejectsPending` | `M.stop` calls `close_pending_diffs`, then `stop_server`, then clears the senders |
| `ExitRejectsPending` | the `VimLeavePre` callback `cleanup_at_exit` rejects each pending diff before it calls `_cleanup_all_active_diffs`, so the final cleanup pass finds no pending diff |
| `ExitAnswersInFlight` | `M.stop` answers each request in `M.state.in_flight`, and `_handle_request` sends nothing after a stop that answered it |
| `StopPendingOnly`, `DisconnectPendingOnly` | the `status == "pending"` filters in `close_pending_diffs` and `close_diffs_for_client` |
| `DisconnectRejects` | `on_disconnect` schedules `close_diffs_for_client` |
| `UserCloseAllPendingOnly` | `:ClaudeCodeCloseAllDiffs` calls `close_pending_diffs`, never `close_all_diffs` |
Expand Down Expand Up @@ -119,8 +122,10 @@ Then decide which kind of failure it is:

## Scope and bounds

- The invariants run with 3 openDiff calls, 2 tab names and 2 clients, about 89,000 states. `DisconnectedCallsAnswered` runs with 2 calls, 2 tabs and 2 clients. It assumes weak fairness only on setup and on the scheduled disconnect cleanup. The user is never assumed to act, with one exception: the disconnect cleanup waits until Neovim allows window changes (`utils.when_windows_allowed`), so a user in the command-line window is assumed to leave it, and textlock is assumed to end.
- The invariants run with 3 openDiff calls, 2 tab names and 2 clients, about 93,000 states. `DisconnectedCallsAnswered` runs with 2 calls, 2 tabs and 2 clients. It assumes weak fairness only on setup and on the scheduled disconnect cleanup. The user is never assumed to act, with one exception: the disconnect cleanup waits until Neovim allows window changes (`utils.when_windows_allowed`), so a user in the command-line window is assumed to leave it, and textlock is assumed to end.
- In every run, a user `ClaudeCodeDiffOpened` handler (README "Diff Lifecycle Events") can accept or deny the diff during setup: `:ClaudeCodeDiffAccept`, `:ClaudeCodeDiffDeny`, or a `nested = true` autocmd that closes the proposal window. A default handler that closes the window resolves nothing, because WinClosed does not fire inside a non-nested autocmd. Other handler actions during setup are not modeled.
- `DiffCleanupAtExit` is the `VimLeavePre` callback of `diff.lua`: it rejects each pending diff, then calls `_cleanup_all_active_diffs("shutdown")`. It models neither a `ClaudeCodeDiffClosed` handler (the reject pass has none unless a `keep_empty` reject runs a cleanup) nor a saved diff lost at exit: Neovim quits right after the step, and its buffers go with it. The model represents `DiffCleanupAtExit` and `ServerStops` as separate atomic actions and explores both orders, because both are `VimLeavePre` autocmds. Neovim's own exit `BufUnload` loop, which rejects before `VimLeavePre`, is the `UserRejects` action.
- `ExitInSetup` is an exit inside a `nested = true` `ClaudeCodeDiffOpened` handler, while one call is in setup, so it needs `OpenedEventInSetup`. The call has no sender and its setup never returns, so only the server stop can answer it (`ExitAnswersInFlight`). The action runs both `VimLeavePre` autocmds in one order, diff cleanup first, then the server stop. The other order gives the same result, because each leaves the other nothing to do. A handler that runs `:ClaudeCodeStop` instead of an exit is not modeled: the handler returns after the stop, and `tests/unit/server/in_flight_request_spec.lua` checks that `_handle_request` then sends nothing. What Claude receives at an exit is in the root `README.md`, under Global Invariants.
- `SenderCleared` alone is caught by no rule, because the pending guards also stop a second answer. `--mutants` shows that `AtMostOneAnswer` breaks when both `SenderCleared` and `GuardRejected` are removed.
- `SavedDiffKept` knows which client owns each diff, and, while `:ClaudeCodeCloseAllDiffs` runs, which files or file buffers hold the accepted text. The model has no file or buffer contents: the command's first pass leaves the accepted text in any subset of the saved diffs' files or buffers, because the code skips a diff whose file buffer already has unsaved changes, or whose buffer it cannot change. The plugin never writes the file. That the first pass leaves the file on disk and the user's unsaved changes alone is checked by the unit tests, not here. A saved diff counts as lost when the user, a disconnect cleanup or a server stop tears it down, or when a client that does not own it does so while the owner is disconnected. A close by another client while the owner is connected counts as safe, because the owner got `FILE_SAVED` and can still write the file. The code is stricter than the rule: it keeps another client's saved diff in both cases. Ownership compares client ids, so a new connection must never get an old id. With `ClientIdsUnique` off, `ClientIdReused` lets a new connection take the id of a disconnected client.
- The split and unified layouts share the pending guards only because `resolve_inline_as_*` is reached through `_resolve_diff_as_*`. The inline functions have no guard of their own.
Expand All @@ -134,7 +139,7 @@ Then decide which kind of failure it is:
- a cleanup that raises partway. Neovim refuses window changes in the command-line window (E11) and under textlock (E565), and a close that raises there leaves its diff registered. The disconnect cleanup starts only when Neovim allows window changes. The other closes (`close_tab`, a replacing openDiff, the server stop) do not wait, and in those states they still raise
- the `keep_empty` new-file cleanup inside `_resolve_diff_as_rejected` (it runs after the answer)
- setup errors, which answer at once
- Neovim exit (`VimLeavePre`) and the plugin's own `M.stop` in `init.lua`, beyond the server stop it calls
- the plugin's own `M.stop` in `init.lua`, beyond the server stop it calls
- whether a sent response reaches a live socket
- two servers in one Neovim
- A pass covers this model at these bounds, for the facts `check.sh` reads, on `lua/` and `plugin/` exactly as recorded in `covered.lock`. Any other tree reads STALE.
25 changes: 23 additions & 2 deletions .agents/skills/verify-diff-lifecycle/check.sh
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ covered_block setup_deferred "$SERVER" '^function M\._setup_deferred_response\('
covered_block user_close_all "$MAIN" 'nvim_create_user_command\("ClaudeCodeCloseAllDiffs"'
covered_block close_active "$DIFF" '^local function close_active_diffs\('
covered_block cleanup_all "$DIFF" '^function M\._cleanup_all_active_diffs\('
covered_block exit_cleanup "$DIFF" '^local function cleanup_at_exit\('
covered_block inline_saved "$INLINE" '^function M\.resolve_inline_as_saved\('
covered_block inline_rejected "$INLINE" '^function M\.resolve_inline_as_rejected\('
covered_block handle_invoke "$TOOLS" '^function M\.handle_invoke\('
Expand Down Expand Up @@ -137,6 +138,26 @@ fact[ClientIdsUnique]=$(as_bool client_ids_unique)
fact[StopRejectsPending]=$(as_bool in_order 'diff\.close_pending_diffs\(' 'tcp_server\.stop_server\(' \
'_G\.claude_deferred_responses = \{\}' <<<"$server_stop")
fact[StopPendingOnly]=$(as_bool grep -qE '^ *return diff_data\.status == "pending"$' <<<"$close_pending")
# The VimLeavePre callback rejects each pending diff before it calls _cleanup_all_active_diffs, so a diff that no
# BufUnload rejected is rejected before the final cleanup pass.
FACTS+=(ExitRejectsPending)
exit_rejects_pending() {
in_order '^local function cleanup_at_exit\(\)$' 'diff_data\.status == "pending"' \
'pcall\(M\._resolve_diff_as_rejected, entry\.tab_name\)' \
'^ M\._cleanup_all_active_diffs\("shutdown"\)$' <<<"$exit_cleanup" &&
in_order '^vim\.api\.nvim_create_autocmd\("VimLeavePre", \{$' '^ callback = cleanup_at_exit,$' <"$DIFF"
}
fact[ExitRejectsPending]=$(as_bool exit_rejects_pending)
# A request has no answer until its handler returns, and a blocking tool has no sender before that. When Neovim exits
# inside the handler, M.stop answers the request, and _handle_request sends nothing after a stop that answered it.
FACTS+=(ExitAnswersInFlight)
exit_answers_in_flight() {
in_order '^ M\.state\.in_flight\[in_flight\] = true$' 'pcall\(handler, client, params\)' \
'^ if not M\.state\.in_flight\[in_flight\] then$' '^ return$' <<<"$handle_request" &&
in_order '^ for in_flight in pairs\(M\.state\.in_flight\) do$' 'M\.send_response\(in_flight\.client, in_flight\.id' \
'tcp_server\.stop_server\(' <<<"$server_stop"
}
fact[ExitAnswersInFlight]=$(as_bool exit_answers_in_flight)
fact[DisconnectRejects]=$(as_bool in_order 'vim\.schedule\(function\(\)' 'diff\.close_diffs_for_client\(client_id' \
<<<"$on_disconnect")
fact[DisconnectPendingOnly]=$(as_bool grep -qE \
Expand Down Expand Up @@ -199,7 +220,7 @@ fact[OpenedEventInSetup]=$(as_bool opened_event_in_setup)
mapfile -t COVERED < <(find lua plugin \( -name '*.lua' -o -name '*.vim' \) | sort)
SITE_RE='(_resolve_diff_as_|resolve_inline_as_|_cleanup_diff_state|_cleanup_all_active_diffs|close_[a-z_]*diffs|close_diff_by_tab_name|resolution_callback|claude_deferred_responses|_register_diff_state|active_diffs|_get_active_diffs|\.status *= *[^=])'

RULES=(AtMostOneAnswer AnswerMatchesDiff NoStrandedCall SavedDiffKept NoRejectedLeftover)
RULES=(AtMostOneAnswer AnswerMatchesDiff NoStrandedCall SavedDiffKept NoRejectedLeftover ExitedCallsAnswered)
LIVE=(DisconnectedCallsAnswered)
CONSTRAINT=AnswerBound

Expand All @@ -208,7 +229,7 @@ CONSTRAINT=AnswerBound
# it. SetupAnswerReturned=FALSE is caught only through that step, so its row also shows that the step is reachable.
EXPECT=(
[GuardSaved]=AnswerMatchesDiff [GuardRejected]=AnswerMatchesDiff
[ReplaceRejects]=NoStrandedCall [CloseTabRejectsPending]=NoStrandedCall [CloseEachByName]=NoStrandedCall [StopRejectsPending]=NoStrandedCall
[ReplaceRejects]=NoStrandedCall [CloseTabRejectsPending]=NoStrandedCall [CloseEachByName]=NoStrandedCall [StopRejectsPending]=NoStrandedCall [ExitRejectsPending]=NoStrandedCall [ExitAnswersInFlight]=ExitedCallsAnswered
[SetupAnswerReturned]=NoStrandedCall
[StopPendingOnly]=SavedDiffKept [DisconnectPendingOnly]=SavedDiffKept [UserCloseAllPendingOnly]=SavedDiffKept
[UserCloseKeepsAcceptedText]=SavedDiffKept
Expand Down
13 changes: 8 additions & 5 deletions .agents/skills/verify-diff-lifecycle/covered.lock
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ file lua/claudecode/config.lua 3afb1bdeff27bfb6
== lua/claudecode/cwd.lua
file lua/claudecode/cwd.lua 35b7af3572d13018
== lua/claudecode/diff.lua
file lua/claudecode/diff.lua ac01bc69a313e411
file lua/claudecode/diff.lua a1c57f34e79b17ce
block resolve_saved 4d34b0c7e34d561f
block resolve_rejected c7a620816abff9a1
block open_blocking 92067df7f9d4d4d9
Expand All @@ -20,6 +20,7 @@ block put_in_buffer c5dedfca8261379b
block held_for_other 3d1e2911d5310cc2
block close_active 446fbed632748300
block cleanup_all 43e7b595cf106229
block exit_cleanup 8bc9fbded77d818f
block accept_current 7577efa33506569e
block fire_event ef778bb39419d91a
block register_state 8cf78b6711a9ecc6
Expand All @@ -28,7 +29,7 @@ block diff_autocmds 01fff2946c5a2149
block write_proposal 9baeff1cd3273193
block reject_when_hidden dd45932e5cd7090d
block deny_current 94385d781b70d50c
site lua/claudecode/diff.lua: M._cleanup_all_active_diffs("shutdown") @ vim.api.nvim_create_autocmd("VimLeavePre", {
site lua/claudecode/diff.lua: M._cleanup_all_active_diffs("shutdown") @ local function cleanup_at_exit()
site lua/claudecode/diff.lua: M._cleanup_diff_state(tab_name, "diff rejected (keep_empty)") @ function M._resolve_diff_as_rejected(tab_name)
site lua/claudecode/diff.lua: M._cleanup_diff_state(tab_name, "diff tab closed after reject") @ function M.close_diff_by_tab_name(tab_name, client_id)
site lua/claudecode/diff.lua: M._cleanup_diff_state(tab_name, "diff tab closed after reject") @ function M.close_diff_by_tab_name(tab_name, client_id)
Expand Down Expand Up @@ -62,6 +63,7 @@ site lua/claudecode/diff.lua: for _, diff_data in pairs(active_diffs) do @ funct
site lua/claudecode/diff.lua: for _, diff_data in pairs(active_diffs) do @ function M.close_saved_diffs(reason)
site lua/claudecode/diff.lua: for _, other in pairs(active_diffs) do @ local function save_window_sizes(tab)
site lua/claudecode/diff.lua: for tab_name, _ in pairs(active_diffs) do @ function M._cleanup_all_active_diffs(reason)
site lua/claudecode/diff.lua: for tab_name, diff_data in pairs(active_diffs) do @ local function cleanup_at_exit()
site lua/claudecode/diff.lua: for tab_name, diff_data in pairs(active_diffs) do @ local function close_active_diffs(filter_fn, reason, client_id)
site lua/claudecode/diff.lua: function M._cleanup_all_active_diffs(reason) @ function M._cleanup_all_active_diffs(reason)
site lua/claudecode/diff.lua: function M._cleanup_diff_state(tab_name, reason) @ function M._cleanup_diff_state(tab_name, reason)
Expand Down Expand Up @@ -96,6 +98,7 @@ site lua/claudecode/diff.lua: local diff_data = active_diffs[tab_name] @ local f
site lua/claudecode/diff.lua: local entry = active_diffs[tab_name] @ function M._register_reject_when_hidden(tab_name, new_buffer, autocmd_ids)
site lua/claudecode/diff.lua: local existing_diff = active_diffs[tab_name] @ function M.open_diff_blocking(old_file_path, new_file_path, new_file_contents, tab_name, client_id)
site lua/claudecode/diff.lua: local function close_active_diffs(filter_fn, reason, client_id) @ local function close_active_diffs(filter_fn, reason, client_id)
site lua/claudecode/diff.lua: local ok, err = pcall(M._resolve_diff_as_rejected, entry.tab_name) @ local function cleanup_at_exit()
site lua/claudecode/diff.lua: local state = active_diffs[tab_name] @ function M._setup_blocking_diff(params, resolution_callback)
site lua/claudecode/diff.lua: resolution_callback = resolution_callback, @ function M._setup_blocking_diff(params, resolution_callback)
site lua/claudecode/diff.lua: return active_diffs @ function M._get_active_diffs()
Expand Down Expand Up @@ -146,10 +149,10 @@ file lua/claudecode/server/frame.lua 3c50766875878d56
== lua/claudecode/server/handshake.lua
file lua/claudecode/server/handshake.lua 3eca35d572094a55
== lua/claudecode/server/init.lua
file lua/claudecode/server/init.lua 8da8851fff781946
block server_stop 4dae0bf675cf2cc1
file lua/claudecode/server/init.lua dbc9b57cf9a7142b
block server_stop 506e2e53358dc947
block on_disconnect a0ce86cede4af786
block handle_request b74ff7dc2e55a2b8
block handle_request 3de5ff2f22d24871
block setup_deferred f9381caaae0fe517
site lua/claudecode/server/init.lua: _G.claude_deferred_responses = {} @ function M._setup_deferred_response(deferred_info)
site lua/claudecode/server/init.lua: _G.claude_deferred_responses = {} @ function M.stop()
Expand Down
Loading
Loading