Repository navigation
fix(server): log Authenticated after the token check and run git once per lookup - #539
Merged
Merged
Conversation
… per lookup Three small defects in code text and logging: - The server logged "Authenticated WebSocket client connected" from on_connect, which runs at the TCP accept, before the handshake and the token check. A client with a wrong token was logged as authenticated. on_connect now logs "awaiting authentication", and on_open (after the handshake passed the check) logs "Authenticated". - cwd.git_root ran `git rev-parse` twice for one lookup: once inside a pcall to see whether systemlist takes a list, and again for the result. It now keeps the first result. - The comment in tcp.lua said the PRNG is seeded once per process. The flag is a module local, so it is seeded once per load of the module. The comment is fixed, not the seeding: a second seed in one process is harmless and Neovim loads the module once.
… the authenticated log - README: git_root runs no git for a missing folder or a nil start folder, so `git rev-parse` runs at most once for each lookup. - server/init.lua: a server without a token runs no token check. The comment on the `Authenticated` log now says it is about a token.
# Conflicts: # lua/claudecode/README.md # lua/claudecode/server/README.md
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: Something went wrong. Try again later by commenting “@codex review”. ℹ️ 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 Review: Didn't find any major issues. Already looking forward to the next diff. 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". |
Member
Author
|
@codex security review |
🛡️ 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. |
This was referenced Nov 12, 2026
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
…ine and tcp.lua comment (#539)
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
#539 changed only debug log text in the on_connect callback of server/init.lua (when Authenticated is logged). The callback sends no selection, starts no timer and touches no selection state, so the model needs no change.
This was referenced Nov 12, 2026
ThomasK33
added a commit
that referenced
this pull request
Nov 12, 2026
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.
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…n tracking (coder#477) ## Status coder#524 is merged (`a41254a4`). It changed the flush on visual exit: the changedtick comparison is gone, and a `visual_entry` that the buffer listener marks takes its place. This PR models it. Codex round 4 (`91660323`) raised two P2 threads, fixed in round 5 (`f974ee06`: both lanes clean). The Opus and GPT verifiers of `f974ee06` found one documentation defect and three minors, fixed in this round 6 (the last). The replays also found a family of bugs that coder#524 left: any edit made while you select whose check has not run when the next key arrives. Three are reproduced (a mapping, a key that arrives during the plugin's callback, an autocmd edit at a mode change), and fix PR coder#540 fixes all three. Their replays print `BUG` on `main` until coder#540 merges. ## What this adds `.agents/skills/verify-selection-tracking/`: a TLA+ model of what Claude sees as the user's current selection (`lua/claudecode/selection.lua`), checked by TLC against guards that `check.sh` reads from the Lua code, on the shared harness from coder#450. The model has no clock, so it covers every `visual_demotion_delay_ms`. A change that removes or rewords a guard makes a rule break or the covered code read STALE. The model describes `main` as it is now: the four bugs it found are fixed (coder#452), and so are the cases that reviews found afterwards (coder#471, coder#481, and the recursion of coder#481's code that coder#493 fixed). ## The ten rules, as plain sentences | Rule | Plain sentence | | --- | --- | | `ReleaseSent` | Right after you release a selection in a file (Esc), Claude holds it, also when you made it faster than the 100 ms debounce (issue coder#246), and when a plugin edited another line or a `:write` ran while you selected. | | `NoPhantomSelection` | Claude only gets text you selected, never the text at the `'<,'>` marks after an operator such as `d` changed it. | | `NoTerminalSelection` | Claude never gets a selection in the Claude terminal buffer. | | `HeldUntilMoved` | Once events settle in a file, a selection you released stays with Claude while the cursor has not moved and its text is unchanged. | | `HeldInTerminal` | Once events settle in the Claude terminal, Claude still holds the selection you released while its text is unchanged. | | `HeldEndsWhenMoved` | Once events settle in a file, Claude holds a released selection only while the cursor has not moved since you released it. | | `SameFile` | Once events settle in a file, Claude's selection is in that file. | | `ClaudeSeesCursor` | Once events settle in a file, a cursor-only selection that Claude holds is where the cursor is, and in visual mode Claude holds the live selection. | | `NoDeletedText` | Once events settle, Claude holds no selection text that its buffer no longer has. | | `TimerClosedOnce` | No timer handle is closed twice (Neovim would raise `handle ... is already closing`). | "Once events settle" means no debounce or demotion timer runs, no timer callback waits in the `vim.schedule` queue, and the check that the buffer listener queued with `vim.schedule` has run. ## Bugs this model found The first version of the model broke four rules on the code before coder#452. Each path was replayed on Neovim 0.12.3. **coder#452 fixed all four**: 1. `HeldEndsWhenMoved`: Claude kept a released selection after the cursor left it (`vb` Esc `gv` `d`, or `ve` Esc `l` `h` inside 100 ms). 2. `NoDeletedText`: Claude kept a held selection after you edited its text without moving the cursor (`viw` Esc `x` `x`). 3. `SameFile`: with a long `visual_demotion_delay_ms`, Claude held another file's cursor (`:b b.txt`, `:b a.txt`). 4. `ClaudeSeesCursor`: with a long `visual_demotion_delay_ms`, Claude held a cursor position you had left (Esc `l`, wait, `h`). **coder#471** closed the case a Codex review of coder#452 found: an operator consumes a second selection and you enter the Claude terminal within the debounce. The model's flush-skip step (`FlushSkipReports`) describes the fixed code, and `tests/integration/selection_held_spec.lua` replays the path with a real terminal buffer. **coder#481** closed the case a reviewer of this PR found, and no step of the model could express it: Claude holds selection A, you go to the Claude terminal, and A's file changes while you are there (Claude rewrites it and Neovim reloads it, or a plugin deletes the selected text). Claude kept the deleted text until you came back. The model now has a step for it (`YouEditOtherBuffer`) and three facts: `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText`. `replays/held_after_reload_in_terminal.lua` and `replays/held_after_edit_in_terminal.lua` replay the two triggers on real Neovim. **coder#524** closed the case an advisor of this PR found, and no step of the model could express it: you select, a plugin edits another line (or a `:write` runs) while you are still in visual mode, and you press Esc inside the 100 ms debounce. The flush took a moved changedtick for an operator that consumed the selection, so Claude got the cursor and not the selection. The model now has two steps that move only the changedtick (`YouEditByPluginInVisual`, `YouWriteInVisual`) and three facts for the new code (`FlushSkipsOperator` rewritten, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit`). `FlushIgnoresTick` is the old comparison as a fact: it reads `FALSE` on the code before coder#524, and the model then breaks `ReleaseSent` and `HeldUntilMoved` (`NoPhantomSelection` still holds, because the old guard did stop operators). Three replays (`release_after_plugin_edit_in_visual.lua`, `release_after_plugin_append_in_visual.lua`, `release_after_write_in_visual.lua`) print `BUG` on `fcea49af` (the commit before coder#524) and `OK` on `main`, on Neovim 0.12.3 and 0.8.0. **Still open, found by the replays:** the flush on Esc skips a selection that has an edit nobody checked yet, and the check that clears a plugin's edit runs in `vim.schedule`, after the command or callback that made the edit returns. When a key comes first, the flush takes the edit for an operator's and Claude gets the cursor, not the selection, although its text is untouched. The model runs that check in the step of the edit, so it does not show this, and a PASS says nothing about it. Three ways to get there print `BUG` on Neovim 0.8.0 and 0.12.3 (3 of 3 runs each): a mapping that edits another line and presses Esc in one typeahead (`release_in_same_typeahead_as_plugin_edit.lua`), a key that arrives while a timer callback of the plugin still runs (`release_with_key_during_plugin_callback.lua`, with `nvim_input`; the Opus verifier found it with an attached UI), and an autocmd that edits when visual mode starts with the Esc already in the typeahead (`release_after_autocmd_edit_in_visual.lua`, a `ModeChanged` handler for `n:v`; the GPT verifier found it). In a tree with coder#540 (a `vim.on_key` listener runs the check at the next key) all 16 replays print `OK` on both versions. A plugin edit whose check runs before the next key is not affected (`release_after_plugin_edit_in_visual.lua`). **coder#457** and **coder#463** changed `getCurrentSelection` and moved the terminal check into `M.is_claude_terminal_buffer`. The model follows that move (`FlushSkipsTerminal`, `UpdateSkipsTerminal`). It makes no claim about what `getCurrentSelection` answers when nothing is tracked. ## What changed from the model that found those bugs - The model now describes the fixed code: `clear_held_state`, `reconcile_held_selection` (called from `CursorMoved`, `BufEnter` and `TextChanged`), the changedtick record `selection_tick`, `cursor_at_flush.left` and `.away`, and the flush-skip report. That adds nine facts (21 in all), the coder#481 guards add three (24 in all), and the coder#524 guards add three more (27 in all). - `SameFile` and `ClaudeSeesCursor` no longer break on the code as written. The special case that ran their mutants with `DelayBelowDebounce = TRUE` is gone, and the check uses `FALSE` (every delay). - Five guards break no rule alone, because another guard covers for them (`FlushSkipReports` only together with `EntryClearsHeld`). `--mutants` removes each with its partner (four `A+B` keys in `EXPECT`): `DemotionClearsHeldState` + `MoveReports` and `PendingClearsHeld` + `ReconcileOnCursorMoved` break `ClaudeSeesCursor`, `ElseClearsHeldState` + `LeaveNoted` breaks `SameFile`, `EntryClearsHeld` + `FlushSkipReports` breaks `HeldEndsWhenMoved`. I found these pairs by running each such guard together with each other guard. SKILL.md lists them. - The model has a `YouEditByPlugin` step: `TextChanged` without `CursorMoved`. In the model, `ReconcileOnTextChanged` and `TextChangeReports` each break `NoDeletedText` alone because of it. On real Neovim they do not: the buffer listener (`on_lines`) also fires for an edit of the current buffer and runs the same check. `replays/held_after_plugin_edit.lua` prints `OK` with either call removed from `lua/` (I removed each: all 18 replay runs print `OK`, while `check.sh` reports `BROKEN: NoDeletedText`). So a `BROKEN` trace for these two guards is a counterexample of the model, not a failure of the running plugin. SKILL.md says so. `--mutants` still requires both guards, because the model has no other way to end the hold at that edit. - The model keeps the changedtick as one bit on the visual entry ("moved since visual mode started"), not as a number per buffer: the code before coder#524 only compared it with the value recorded at entry, and a changedtick only grows. A number per buffer multiplies the states and the `--mutants` time by an estimated 5 to 10 and adds no behavior (I did not build it). The bit is kept only while an entry exists and a guard reads it, so the main run has fewer states (129,986) than before (178,962). - `LeaveNoted` breaks `HeldEndsWhenMoved` alone only when the user can visit a second file, so `--mutants` runs that rule with two files. - The model has a `YouEditOtherBuffer(b)` step: the text of a buffer that is not current changes, `TextChanged` does not fire for it, and the plugin sees the change only through its `nvim_buf_attach` listener (`on_lines`, `on_reload`, `on_detach`) or when you come back. The listener only queues its check with `vim.schedule`, so the model sets a queued-check bit at the edit and runs the check in its own step (`ListenerCheckRuns`), after any other step (Codex round 2). `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText` are the guards of coder#481 that break `NoDeletedText` when removed. - `HeldInTerminal` is new in this round (Opus verifier). `HeldUntilMoved` only holds in a file, so two regressions that drop a released selection in the Claude terminal passed every rule: `update_selection` in the terminal that reports the cursor although the text did not change, and a demotion in the terminal that publishes the cursor of the held buffer. The new rule says that Claude keeps the selection there. It passes on the model, and six guard removals break it, so it is not vacuous. - The 16 replays (`replays/`) exit 0 on `OK` and 1 on `BUG`. Eleven replay a path that once broke a rule and show the promise kept (the three added for coder#524 are the plugin edit, the plugin append and the `:write` in visual mode). `held_after_line_inserted_above.lua` (a line inserted above a held selection makes Claude lose the selection and get the cursor, although the text still exists) and `v_escape_selects_one_character.lua` (a bare `v` and Esc selects the character under the cursor, so it is a selection) show things that are not rules. Three replay known bugs and print `BUG` until coder#540 merges (see "Still open"). `replays/run.sh` works without GNU `timeout` (macOS) and with a checkout path that has a space, a comma or a quote (Codex round 2). ## Proof All on this branch, Neovim 0.12.3, Java from mise: - `check.sh`: `main: pass (129986 distinct states found)`, `== RESULT: PASS` (exit 0, a fresh lock), all 27 facts `TRUE`. - `check.sh --mutants` (4486 s, about 75 min, at a load average of 22 to 31): 26 keys (22 single guards and four `A+B` pairs), `== mutants: every guard is caught`, no rule is vacuous (exit 0). The new facts are caught as `EXPECT` says: `FlushSkipsOperator` and `ListenerNotesVisualEdit` break `NoPhantomSelection`, `VisualCheckSparesPluginEdit` and `FlushIgnoresTick` break `ReleaseSent`. The run is on `c731ebae`. Since then the model changed only in its comments (the spec without comments is identical, and `check.sh` still reports 129,986 states), and `check.sh` changed in one regex and its comment (the `ListensToSelectionBuffer` regex now reads both forms of `on_lines`, see below). The TLC inputs of `--mutants` (model, constants, `EXPECT`, and the fact values, which are all `TRUE` on `main`) are the same, so I did not run it again. The verifiers ran it on `f974ee06` (Opus 5075 s, GPT 5201 s): 26 keys caught, exit 0. - The code before coder#524: `check.sh` runs on the `selection.lua` of `fcea49af` once two stand-in blocks (`visual_entry_of`, `note_visual_edit`, which the old code does not have) are added at the end of the file. Exactly four facts read `FALSE`: `FlushSkipsOperator`, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit` and `FlushIgnoresTick`. `check.sh` exits 1 with `main: BROKEN: ReleaseSent`, the first broken rule it prints (trace: you select, a plugin edits another line, you press Esc). TLC with that fact set breaks `ReleaseSent` and `HeldUntilMoved` (the Opus and GPT verifiers ran it too), `--mutants` lists `HeldInTerminal` as well for `FlushIgnoresTick`, and `NoPhantomSelection` holds. Putting the old comparison back into the `selection.lua` of this tree gives the same: `check.sh` exits 1, `FlushSkipsOperator FALSE`, `FlushIgnoresTick FALSE`, `main: BROKEN: ReleaseSent`. - Each new guard removed alone from `selection.lua` flips only its own fact: the flush condition (`FlushSkipsOperator`, `main: BROKEN: NoPhantomSelection`), the `note_visual_edit(entry)` call in `on_lines` (`ListenerNotesVisualEdit`, `NoPhantomSelection`), and the mode test of the check (`VisualCheckSparesPluginEdit`, `ReleaseSent`). - Scratch breaks on this tree (edit `lua/`, run, then `git checkout -- lua/` and an empty `git diff --shortstat`): - Dropping `reconcile_held_selection(not entered_buffer)` from `M.on_cursor_moved`: `check.sh` exits 1, `ReconcileOnCursorMoved FALSE`, `main: BROKEN: HeldEndsWhenMoved`, and `replays/held_after_quick_move.lua` prints `BUG the cursor moved after the release, but Claude still holds "alpha"`. - Making the `selection_text_is_there` test in `demote_if_selection_text_changed` always true: `check.sh` exits 1, `TextChangeReports FALSE`, `main: BROKEN: NoDeletedText`, and `replays/held_after_edit.lua` prints `BUG Claude holds "alpha" at 0-5, the buffer has "alphb" there`. - Dropping `watch_selection_buffer(bufnr)` from `record_selection_read`: `check.sh` exits 1, `ListensToSelectionBuffer FALSE`, `main: BROKEN: NoDeletedText`, and `replays/held_after_reload_in_terminal.lua` prints `BUG Claude holds "alpha", but a.txt is "beta gamma"`. - `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`. - Replays: 16 probes on Neovim 0.12.3 and 0.8.0, each at the default delay and with `DELAY_MS=50` (that setting changes only the two long-delay probes): 13 print `OK` and the three known-bug probes print `BUG` (coder#540). On `fcea49af` the three probes for coder#524 print `BUG` on both versions. In a tree with coder#540 (a scratch copy of the skill, not part of this PR) all 16 print `OK` on both versions, and the two new known-bug replays ran 4 times each on both versions with the same result. - At `91660323`, a script that removed each of the 24 guards from `selection.lua` alone showed that exactly its own fact turns `FALSE` (seven regexes read a second guard before; the Opus verifier found three of them). The regexes of `FlushOnVisualExit`, `ReconcileOnCursorMoved` and `ReconcileOnTextChanged` are anchored now, because a commented-out handler call used to leave the fact `TRUE`: with each call commented out in `selection.lua`, only its own fact reads `FALSE`. This round I did the same by hand for the three new guards (see above), and I rewrote the `ListensToSelectionBuffer` regex twice: in round 5 for the code after coder#524 (`on_lines` and `on_reload` call `check_soon` inside `if holds_selection_of(buf) then`), and in this round to read both forms (it read `FALSE` on the `selection.lua` of `fcea49af`, which listens). It is `TRUE` on `fcea49af` and on this head, and `FALSE` when `check_soon()` is removed from `on_lines` or from `on_reload`, and when `watch_selection_buffer(bufnr)` is removed from `record_selection_read` (only its own fact in each case). - `shfmt -i 2`, `shellcheck --exclude=SC1091,SC2016`, `stylua --check`, `prettier --check` and `treefmt --ci` (379 files, 0 changed): clean. `luacheck` 0 warnings in 181 files. `tests/selection_test.lua` and `tests/unit/visual_delay_timing_spec.lua`: 156 successes, 0 failures. This PR changes no `lua/` or `tests/` file. - `covered.lock` is recorded last. This round the flush, `on_mode_changed` and `watch_selection_buffer` blocks changed (coder#524), and `visual_entry_of` and `note_visual_edit` are new blocks. The file hashes of `init.lua` and `server/init.lua` changed with `main`. In round 6 the `on_connect` block changed too (coder#539 moved a debug log line: no send, no timer, no selection state), and the lock is re-recorded. I merged `origin/main` several times and read each diff of the covered code: coder#454 (`server.broadcast` returns, mention queue), coder#481, and coder#493, whose change in `demote_if_selection_text_changed` made the regex of `TerminalReportsHeldBuffer` read `FALSE`. I re-pointed it and re-recorded the lock. coder#467 and coder#491 touch no covered file of this skill. coder#497 changed one debug log argument in the `tools/call` handler of `server/init.lua`, and coder#499 changed the disconnect cleanup in the same file (`on_disconnect`: a client without a handshake owns no diff, and the cleanup waits until Neovim allows window changes). Both are outside `M.broadcast` and the `on_connect` callback, and neither can reach the selection state, a timer or a send, so only the file hash changed and I re-recorded the lock. ## Run it ```bash .agents/skills/verify-selection-tracking/check.sh # about 1 min .agents/skills/verify-selection-tracking/check.sh --mutants # about 1 to 1.5 h (4486 s in the last run), after you edit the model or a fact .agents/skills/verify-selection-tracking/check.sh --hash-only # about 5 s, only compares covered.lock with the code NVIM=~/.local/share/mise/installs/neovim/0.12.3/bin/nvim \ .agents/skills/verify-selection-tracking/replays/run.sh held_after_operator.lua ``` CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job, as for `verify-diff-lifecycle`. ## Review record - Codex round 1 (`ac7f243`): clean in both lanes. - Codex round 2 (`f91391f`): security clean. Code lane, three P2s: the model ran the listener check atomically with the edit, `replays/run.sh` needed GNU `timeout`, and it put raw paths into Neovim commands. All three are fixed. - GPT and Opus verifiers on `f91391f`: ISSUES. F1 (SKILL.md scope omitted a held buffer that becomes a Claude terminal, now a scope bullet) and minors F3 to F10 are applied, except F4 (six blind-spot mutants remove a guard's effect without touching a line a fact reads: the fact stays `TRUE`, but `covered.lock` reads STALE, so `check.sh` exits 3, not 0). F2 and the GPT finding of the same kind stay a disclosed limit: the model runs the buffer listener only for a buffer that is not current, although `on_lines` also fires for an edit of the current buffer, so a `BROKEN` trace for `ReconcileOnTextChanged` or `TextChangeReports` is a counterexample of the model, not a failure of the running plugin (SKILL.md, "Read the result"). - Codex round 3 (`e18a1cf`): clean in both lanes. - GPT and Opus verifiers on `e18a1cf`: ISSUES. Opus N2 (impact: the `HeldUntilMoved` row promised more than its rule checks, and two regressions in the terminal passed): new rule `HeldInTerminal`, rows fixed, `--mutants` rerun. GPT F1 (impact: SKILL.md said a bare `v` and Esc keeps the held selection, but Claude gets the one selected character): the text now says what the code does, and a replay shows it. Minors fixed: N1 anchored autocmd-call regexes, N3 a demotion in a terminal that only its name marks does not take Condition 3, N4 "once events settle" includes the listener's queued check, N5 the shrink step names the three two-file rules, N6 the update step names the listener operators, N7 the `held_after_plugin_edit.lua` comment, N8 statechart labels for the listener steps, N9 user impact of the listener and `holdLoose` items, N10 the `--hash-only` time. - Codex round 4 (`91660323`): security clean. Code lane, two P2 threads, both fixed in this round: the Rules table delimiter (`2c88f30e`) and the model that restricted `YouEditByPlugin` to normal mode, so TLC could not reach a moved changedtick on release (`YouEditByPluginInVisual`, `YouWriteInVisual`, `FlushIgnoresTick`). - GPT and Opus verifiers on `91660323`: PASS, with minors. Fixed here: M1 the Rules table, M4 the `holdLoose` exemption names `HeldInTerminal`, M5 "the rows whose rule is `none`", M6 the return for an unloaded buffer in the Claude terminal is in the not-modeled list (I replayed it on 0.8.0 and 0.12.3). M2 and M3 (a regex that misses a blind-spot mutant or reads through a shared helper) are not changed: the lock reads STALE for them, as for F4 above. - Codex round 5 (`f974ee06`): both lanes clean, CI green, no open threads. - Opus and GPT verifiers on `f974ee06`: ISSUES, one documentation defect (F1) and three minors, all fixed in round 6. F1: SKILL.md said that an edit from a timer, a job or an autocmd cannot hit the same-typeahead bug. The true boundary is any edit whose check has not run when the next key arrives. Two more ways to get there are reproduced and have replays (a key that arrives during the plugin's callback, an autocmd edit at a mode change), the model, replay and SKILL.md text now say so, and coder#540 fixes all three. M1: `check.sh` prints only the first broken rule, and `--mutants` shows the others. M2: the operator order sentence (`on_lines` first, with the mode already normal, then `ModeChanged`) is fixed. M3: the `ListensToSelectionBuffer` regex and the old fact set (four facts, shown with `check.sh` itself). - Codex round 6: this head (the last round). ## Notes for the reviewer - The diff is one new skill folder: SKILL.md, `check.sh`, `covered.lock`, `model/` (the TLA+ spec and a `/statechart` view) and `replays/`. It touches no `lua/` code. - `DEVELOPMENT.md` is not edited here: the skill-listing change belongs to the PR that owns it. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…queue (coder#523) ## What this adds `.agents/skills/verify-mention-queue/`: a TLA+ model of the @mention queue and the WebSocket clients it sends to, a `check.sh` on the shared harness `scripts/tla/check-lib.sh`, a `/statechart` view, and 12 headless Neovim replays. CI runs it in the `covered-lock` job with the other `verify-*/check.sh`. The model describes the code on main after coder#454 and coder#480: one queue, a deadline per mention (`connection_timeout + connection_wait_delay` after the send), a flush that waits until some connected client has been connected for `connection_wait_delay` since its handshake (`connected_at`), a broadcast to every connected client, the drain to a ready client past the deadlines, and the write reports, the refused write included. It has two client slots, so a broadcast can reach two clients and the readiness rule can count both. This PR also fixes the doc findings from the last verifier pass on coder#480, and adds the test the coder#480 advisor found missing: - `.agents/skills/verify-claudecode-nvim/features/send-at-mention.md`: a connected client that is not ready yet gets "Send timeout", not "Connection timeout", and the error comes at the deadline, 10.6 s after the send. - `lua/claudecode/config.lua`, `dev-config.lua`: the `queue_timeout` comments no longer say that mentions wait up to `connection_timeout`. - `fixtures/issue-70/init.lua`: the mention waits until its deadline, 10.6 s by default, not 10 s. - `lua/claudecode/types.lua`: `connection_timer` runs while the queue holds a mention, also while a ready client drains it. It is nil only after a deadline passed while a ready client was connected, until `queue_mention` or a flush with no ready client starts it again. - `tests/unit/mention_queue_spec.lua`: `D: a send 400 ms after the handshake waits until connection_wait_delay has passed since the handshake`, and the same at 540 ms. Each expects nothing 590 ms after the handshake and the mention by 610 ms. A flush that sends while under 20, 100 or 200 ms of the wait are left fails one of them. `D: the first ready client sends the queue, though a second client connected later is not ready yet` fails when readiness waits for the newest client (`math.max` in place of `math.min`). These change comments and tests only. No runtime code changes. ## What the model checks - `NoSilentDrop`: a mention you sent reaches Claude, or you see an error, unless you stopped the integration first. - `SentInOrder`: each Claude gets the mentions in the order you sent them. - `AtMostOnce`: each Claude gets each mention at most once. - `SentWhenReady`: a mention goes out only while some connected client has been connected for `connection_wait_delay` since its handshake. Default config only: with `disable_broadcast_debouncing` on, a send while the queue is empty skips this wait. That is a known bug, which a follow-up PR fixes (repro below). - `NothingAfterStop`: after `:ClaudeCodeStop`, no mention queued before the stop reaches Claude, and the queue raises no Lua error. - `NoStrandedMention` (liveness): every queued mention leaves the queue. - `ReadyDelivers` (liveness): while a ready Claude stays connected, every queued mention goes out to it. - `FlushDelivers` (liveness, with no deadline that passes): the flushes alone send a ready Claude every queued mention, so none waits for a deadline first. `check.sh` reads 19 guards from `init.lua`, `server/init.lua`, `server/tcp.lua` and `server/client.lua`, and runs the model with each one as the code has it. `FlushExpiresOverdue` alone breaks `NoStrandedMention`. `QueueKeepsDeadline` alone breaks no rule in this untimed model: the next flush with no ready client clears the overdue mentions, so only the time of the error changes. So `--mutants` checks it only as a pair with `FlushExpiresOverdue`. The unit tests `A, F4: a Claude whose handshake comes 10.3 s after the send …` and the `S:` churn tests at 700/300 and 650/500 ms catch it alone. A code change that keeps every fact TRUE reads only STALE, for example a change of the readiness wait or a deadline that never comes. `SKILL.md` names such changes, and the unit tests catch them. ## Bugs it found, and the fixes The first model, on the code before coder#454, broke five of its six rules. Each finding was replayed on real Neovim. coder#454 fixed all nine: 1. A: a mention that waited for a slow Claude start was dropped at the flush as older than `queue_timeout`, with no error. 2. H: Claude dropped during the 600 ms wait, and the plugin sent the mention to no client and logged success. 3. E: a send during the wait overtook the mention queued before it. 4. C: `:ClaudeCodeStop` during the wait raised a Lua error, and a stop and a start sent the old mention to the new Claude. 5. B: the connection timer stayed set after it fired, so later mentions never timed out. 6. S: a send while connected started no timer, so a drop within the 50 ms debounce stranded the mention. 7. F: a client that sent its CLOSE frame still counted as connected. 8. D: the flush hook ran at the TCP accept, before the handshake, so a send in between waited for the timeout while Claude was connected. 9. G: a queued mention kept its raw path, while a connected send was made absolute. Four more came up in review of coder#454's fixes and while coder#480 was built, and this model's second version found one. coder#480 fixed all five. Items 13 and 14 were in coder#480's own intermediate commits and never reached main: 10. A second client's handshakes postponed a due flush (Codex, round 6 on coder#454). 11. A write that libuv refused at once dropped the mention with no error. 12. Clients that connected and left without overlap kept a mention waiting with no error. 13. On a head of coder#480 before its drain rule (cefe258), with many mentions queued while Claude started, the first deadline cleared the rest while a ready Claude was taking them, 25 ms apart. With 100 mentions and a handshake 8.6 s after the send, fewer than half arrived, and the count changed with the host's load. `drain.lua` passes only when all 100 arrive, in order, with no error. 14. Found by this model: when Neovim ran the handshake's `on_open` callback late, the deadline found Claude ready before any flush was due, cleared nothing and stopped. When that Claude left before `on_open` ran, nothing sent or cleared the queue. The spared deadline now schedules a flush. ## Proof On the head of this PR, after merging main at 9bfc39c. The statechart runs ran on 195c1d8. The model and `statechart-view.ts` are unchanged since then, and the main merges after it change no mention-queue behavior: - `check.sh`: PASS, exit 0. `main` 270,120 distinct states, `live-NoStrandedMention` 57,814, `live-ReadyDelivers` 57,814, `live-FlushDelivers` 24,692. All 19 facts read TRUE. - `check.sh --mutants`: exit 0 on 86e2359 (the round-3 verifier's run, 2494 s). Every guard is caught by the rule `EXPECT` names, and every rule breaks at least once. Since then the model changed only in comments, `check.sh` and `scripts/tla/` are byte-identical, and the merged code still reads all 19 facts TRUE, so each mutant run gets the same TLC input. - A scratch break of one guard in `lua/` (`expire_mentions` spares a ready client's queue without scheduling a flush) makes `check.sh` exit 1: `SparedQueueFlushes` reads FALSE and `live-NoStrandedMention` is BROKEN. After the restore, `git diff --shortstat` is empty. - `scripts/tla/test-check-lib.sh`: 44 cases, 0 failed. - `replays/run.sh`, the same replays on four trees, old trees on Neovim 0.12.3: - this head: 12 of 12 kept their promise on Neovim 0.8.0 and 12 of 12 on 0.12.3. - b92e7ac (the code before coder#454): 0 of 12. Each replay prints its bug, for example `order` gets `second.txt, first.txt`, `stop-in-wait` gets `init.lua:234: attempt to index field 'server' (a nil value)`, and `churn` loses the mention with no error. - 08dbcae (the code before coder#480) and d1a6724 (a coder#480 head before the deadline per mention): 11 of 12. `churn` keeps the mention queued with no error. - `churn`, 10 runs on this head: 10 kept, the mention cleared with one error 10605 to 10655 ms after the send. The replay now refreshes the loop clock before the send and reads the send and the clearing on that clock, the one that stamps the deadline. Before, it read real time against a loop clock that lagged 17 to 26 ms after `setup()`, and printed BROKEN on correct code in about half the runs. - `order` with a scratch loss of the second mention (a second `table.remove(queue, 1)` in the flush): BROKEN, exit 1. On this head: KEPT. Before, its verdict counted a lost second mention as kept. The other replays pass their verdict expression straight to `L.verdict`, so a `false` or `nil` reads BROKEN there. - `replays/run.sh` portability (Codex round 2): from a checkout path with a space, with `OUT=./rel-logs` and `NVIM=./bin/nvim`, 2 of 2 replays kept, and every `XDG_*_HOME` sits under the absolute `OUT`. On the same path, eb16b3a's `run.sh` printed no verdict (`E518: Unknown option`). Each run is now bounded by `perl -e 'alarm 120; exec @argv'`, not GNU `timeout`: the same wrapper with `alarm 2` ended a hung headless Neovim after 2 s. - `replays/run.sh` exit codes (Codex round 5): a replay counts as `KEPT` only when it printed `KEPT` and its Neovim exited 0. I added two scratch replays to a copy of this head. One prints `KEPT` and then exits 1: it reads `BROKEN … Neovim exited 1 after the verdict "KEPT …"`. The other prints `KEPT` and quits as `L.verdict` does: it reads `KEPT`. The 12 real replays read `KEPT` on Neovim 0.8.0 and on 0.12.3. - `replays/run.sh` on Neovim 0.8 (Codex round 3): each replay now runs through `:luafile`, as `.github/workflows/test.yml` does, since `nvim -l` needs Neovim 0.9. On 0.8.0 and 0.12.3, from a checkout path with a space and with a relative `OUT`, a replay that raises before its verdict reads `BROKEN … printed no verdict` within 3 s, with its error in the log. - `statechart-view.ts`: `/statechart` refuses a view whose regions change between states, so every state now has the regions "Sent early", "Lua error" and "Sent after a stop". Each one reads "no" until its harm happens. The generator charted three scratch breaks with 1 mention and 1 connect, and each exited 1 with a chart: - `StopClearsQueue` off, against `NothingAfterStop`: the flush after the stop raises a Lua error. - `FlushWaitsForReady` off, against `SentWhenReady`. - `StopClearsQueue` off, against `~leaked` alone: the last state shows "Sent after a stop: a mention queued before :ClaudeCodeStop reached a Claude after the stop". Pele 1.9.0 rendered each chart to SVG. On the same leak input, 93fb4cb's view exited 2 ("Return the same regions for every state") and charted nothing. - `verify-diff-lifecycle/check.sh`: PASS. Main's coder#539 added a log line to `on_open` and changed a comment in `tcp.lua`. The flush is still scheduled the same way, so I re-recorded the mention model's `covered.lock` after `check.sh` read all 19 facts TRUE. - busted, full suite, shuffled (seed 12345): 1709 successes, 0 failures, 0 errors, 25 pending. luacheck: 0 warnings in 181 files. `treefmt --ci`: 0 files changed. shellcheck (`--exclude=SC1091,SC2016`) on `check.sh` and `replays/run.sh`: clean. <details> <summary>Repro of the known bug: <code>disable_broadcast_debouncing</code> skips the readiness wait</summary> It runs the real plugin in a headless Neovim with a loopback Claude, sends right after the handshake, and measures on the loop clock that stamps `connected_at`. Save it as `repro-immediate.lua` in the repo root, then run from there (`IMMEDIATE=0` is the default config): ```bash repo=$PWD dir=$(mktemp -d) cp repro-immediate.lua "$dir" && cd "$dir" for imm in 1 0; do CLAUDE_CONFIG_DIR="$dir/claude" REPLAY_LIB="$repo/.agents/skills/verify-mention-queue/replays/lib.lua" IMMEDIATE=$imm \ nvim --headless -u NONE -i NONE --cmd "set rtp^=$repo" -c 'luafile repro-immediate.lua' -c 'cquit 1' done ``` ```lua -- Does a send right after Claude's handshake reach Claude before connection_wait_delay has passed? -- IMMEDIATE=1 sets disable_broadcast_debouncing = true; otherwise the default config (control). -- Times are on the loop clock that the plugin stamps connected_at with (vim.loop.now()). local uv = vim.uv or vim.loop local L = dofile(vim.env.REPLAY_LIB) local immediate = vim.env.IMMEDIATE == "1" local cc = require("claudecode") cc.setup({ terminal = { provider = "none" }, track_selection = false, disable_broadcast_debouncing = immediate }) assert(cc.state.server, "the server did not start") local c = L.connect() assert(L.upgrade(c), "no handshake") local connected_at for _, info in ipairs(require("claudecode.server.init").get_status().clients or {}) do if info.state == "connected" then connected_at = info.connected_at end end assert(connected_at, "no connected_at") uv.update_time() local sent_age = uv.now() - connected_at L.send(L.file("early.txt")) local got_age vim.wait(2000, function() if #L.received(c) > 0 then uv.update_time() got_age = uv.now() - connected_at return true end return false end, 1) local wait = cc.state.config.connection_wait_delay io.stdout:write( string.format( "RESULT disable_broadcast_debouncing=%s connection_wait_delay=%d sent %d ms after the handshake; Claude got it %s; queue=%d; %s\n", tostring(immediate), wait, sent_age, got_age and (got_age .. " ms after the handshake") or "never (2 s)", #(cc.state.mention_queue or {}), (got_age and got_age < wait) and "BEFORE READY" or "after ready" ) ) vim.cmd("qall!") ``` Output: ```text NVIM v0.12.3: RESULT disable_broadcast_debouncing=true connection_wait_delay=600 sent 4 ms after the handshake; Claude got it 7 ms after the handshake; queue=0; BEFORE READY NVIM v0.12.3: RESULT disable_broadcast_debouncing=false connection_wait_delay=600 sent 4 ms after the handshake; Claude got it 600 ms after the handshake; queue=0; after ready NVIM v0.8.0-1210-gd367ed9b2: RESULT disable_broadcast_debouncing=true connection_wait_delay=600 sent 3 ms after the handshake; Claude got it 3 ms after the handshake; queue=0; BEFORE READY NVIM v0.8.0-1210-gd367ed9b2: RESULT disable_broadcast_debouncing=false connection_wait_delay=600 sent 3 ms after the handshake; Claude got it 600 ms after the handshake; queue=0; after ready ``` </details> ## How to run ```bash .agents/skills/verify-mention-queue/check.sh # about 60 s .agents/skills/verify-mention-queue/check.sh --mutants # 25 to 50 min NVIM=nvim .agents/skills/verify-mention-queue/replays/run.sh # about 2 min ``` --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…split layouts (coder#551) ## Why When a user empties the proposal buffer (`ggdG` or `:%delete`) and saves it with `:w`, Claude must get what Neovim's own `:w` writes. Neovim writes no bytes for an emptied buffer. With `'eol'` on, the `vertical` and `horizontal` layouts answered `" "`, so Claude wrote a one-byte file where the user had asked for an empty one. The F14 verifier found this. PR coder#542 listed it as a known, pre-existing defect that this PR fixes. ## What changed `_resolve_diff_as_saved` in `lua/claudecode/diff.lua` saves the lines of the proposal buffer, joined with line breaks. It adds a final line break when the buffer's `'eol'` is on. A buffer with no lines at all (Neovim shows "--No lines in buffer--") still gives one empty string through `nvim_buf_get_lines`. So the save could not tell it from a buffer with one empty line, and it added the line break. The save now counts the bytes of the buffer with `vim.fn.wordcount().bytes`, run inside `nvim_buf_call`. The count is 0 for an empty buffer and at least 1 for a buffer with one empty line when `'eol'` is on. The line break is added only when the count is not 0 and `'eol'` is on. That replaces the check `#content_lines > 0`, which was always true. I tried `nvim_buf_get_offset` and `line2byte` first. Both gave wrong sizes for a buffer that `ggdG` had emptied (a stale line cache), so I did not use them. Other changes: - `tests/mocks/vim.lua` gets `wordcount()` and an `empty = true` flag for a mock buffer. `nvim_buf_call` in the mock now names the buffer that the callback acts on. - `tests/unit/diff_ui_cleanup_spec.lua` gets one fixture line. The mock's `nvim_buf_call` refuses a buffer that does not exist, and that spec saved a buffer that the mock never had. - `lua/claudecode/README.md`: one bullet replaces coder#542's bullet about the saved content of the split layouts. It states both rules, `'eol'` from the proposal and the empty buffer. It also says that a buffer with one empty line is saved as `"\n"` when `'eol'` is on and as `""` when it is off. - `.agents/skills/verify-diff-lifecycle/covered.lock` is re-recorded (see Blast Radius). ## Scope - The `vertical` and `horizontal` layouts share one code path, so one change fixes both. - The `unified` layout is unchanged. It answers with the proposal, not with the buffer, so what the user does to its buffer never reaches Claude. The new spec runs it as a control. - With `'eol'` on, a buffer with one empty line is still saved as `"\n"`. With `'eol'` off, it is saved as `""`, as before. A buffer with any line is saved as before. - On `main` (with coder#542), this PR changes the answer only for a buffer that the user emptied. It changes no answer for an unedited proposal: coder#542 already makes an empty proposal give `""`, and the new spec has that case as a control. ### Minor findings that I declined Two verifiers (Opus and GPT) found these. None of them changes an answer that a user reaches with the default settings. - **A buffer set to `bomb` (Opus F3).** With `ggdG`, then `:setlocal bomb`, then `:w`, Neovim writes the 3-byte BOM. Both `main` and this PR answer without the BOM (`main` answers `"\n"` when `'eol'` is on and `""` otherwise, this PR answers `""`). The plugin never sets `'bomb'` on its scratch proposal buffer, and no answer of the plugin ever holds a BOM, so a user has to set a non-default option on a scratch buffer first. I left it. - **The `nvim_buf_call` wrapper is covered by the mock spec only (Opus F4).** If I delete the wrapper, only the mock unit spec fails. In the paths that save (`BufWriteCmd` and `accept_current_diff`) the current buffer is always the proposal buffer, so the wrapper is defensive and no live answer changes. I kept the wrapper, because `wordcount()` reads the current buffer, and I added no live test for a case that no path reaches. - **Cost of `wordcount()` (Opus F5).** It adds a second pass over the buffer. For a 33 MB proposal that is about 0.1 to 0.2 s (0.12.3: +112 ms, 0.8.0: +216 ms), about the cost of `nvim_buf_get_lines` plus the join. I accept that for one save. ## Blast Radius - User-visible: a proposal buffer that the user emptied is accepted as an empty string. Every other buffer gives the same text as before. - `wordcount()` runs in the proposal buffer through `nvim_buf_call`. It does not change the user's current buffer or window. Both functions exist in Neovim 0.8. I ran the specs on Neovim 0.12.3 only. The CI job `integration-tests (v0.8.0)` runs the new spec on 0.8. - `covered.lock`: the change touches `_resolve_diff_as_saved`, a covered block. `check.sh` printed STALE for the `diff.lua` file hash and the `resolve_saved` block hash only. It printed no changed call site, and all 21 code facts stay TRUE. The guard that lets only a `pending` diff resolve is unchanged, and so are the status change to `saved` and the one call of the resolution callback. The change only decides whether the `text` string of the `FILE_SAVED` answer ends in a line break. The model stores which kind of answer a call got, not its text, so no modelled transition changes. The model passed (`main`: 89205 distinct states, `live-DisconnectedCallsAnswered`: 5269). `check.sh --record` wrote the new lock and `check.sh --hash-only` reports that it matches. ### Merge with coder#542, coder#539 and coder#535 coder#542 (F14) landed first, on 2026-11-12 at 04:36Z, and coder#539 (F12) at 04:46Z. coder#538 and coder#550 later changed `diff.lua` too, and coder#549 renamed "proposed buffer" to "proposal buffer" in the README. This PR merged `origin/main` (9bfc39c) with merge commits. It ran `check.sh --record` after each change to `diff.lua` and kept main's README wording in the last one. Only the `diff.lua` file hash and the `resolve_saved` block hash differ from the lock on `main`. The full `check.sh` passes and `check.sh --hash-only` matches. - One README bullet replaces this branch's bullet and coder#542's bullet, because the two said almost the same sentence and this branch's sentence about one empty line was false once `'eol'` can be off. - coder#535 (F11) is still open. It touches neither `diff.lua` nor this README bullet. Its current head (`a5dfc81b`, with `main` merged) merges with this PR without a conflict. ## Verification Red before the fix, green after (same specs, only `lua/claudecode/diff.lua` swapped, on the merged head, so the red column is `main` at 9bfc39c with coder#542): | Spec | `main` (with coder#542) | with the fix | | --- | --- | --- | | `tests/unit/diff_saved_text_spec.lua` (4 cases, mock) | 3 successes, 1 failure | 4 successes, 0 failures | | `tests/integration/diff_accept_emptied_buffer_spec.lua` (40 cases, real Neovim, `:write`) | 28 successes, 12 failures | 40 successes, 0 failures | Against the older merge base (5acc100, before coder#542), the 38-case spec of round a had 24 red cases. Today's 40-case spec has 26 there: the 24 emptied cases plus the new control for an unedited empty proposal in both layouts. coder#542 fixes the 12 cases from proposals without a final line break (it sets `'eol'` off), so 12 stay red on `main`. The integration spec opens a real `openDiff` and edits the proposal window. For the `vertical` and `horizontal` layouts it runs 6 proposals (two lines and a final line break, one line and a final line break, one blank line, one line with no final line break, two lines with no final line break, and no text) with 2 ways to empty the buffer (`ggdG` and `:%delete`). Each case compares the answer with what Neovim's own `:w` writes: the spec edits a real file buffer with the same text and commands, runs `:write`, and reads the file bytes, which are empty. Five controls per layout give the right text before and after (a blank line left in the buffer, no edit, an empty proposal without an edit, one line deleted, and text typed into the emptied buffer). In the `unified` layout, 6 controls check that the answer is the proposal. Gates on the final commit, which merges `origin/main` (9bfc39c) into the branch (private XDG folders): - `mise run all`: native exit 0. luacheck: 0 warnings / 0 errors in 183 files. busted: 1710 successes / 0 failures / 0 errors / 26 pending. treefmt: 0 files changed. - `mise run format-check`: native exit 0 (360 files, 0 changed). - Diff specs (`tests/unit/diff*_spec.lua`, `opendiff_blocking_spec`, `new_file_reject_then_reopen_spec`, and the `open_diff_mcp`, `close_tab` and `close_all_diff_tabs` specs): 226 successes, 0 failures. - `scripts/run_integration_tests_individually.sh`: 457 successes, 0 failed, 0 errors. The new spec gives 40 successes. - `.agents/skills/verify-diff-lifecycle/check.sh --hash-only`: covered.lock matches the code. Two independent verifiers (Opus and GPT) checked the code at `ef8be297`. Both found the code correct. Their blockers were the README sentence and the stale base, and this head fixes both. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
… other path characters (coder#561) ## Why `cwd.git_root` must find the repository of a folder whatever its name is. A repository in a folder with a space or a comma in its path was not found when git could not run: the fallback gave nil, or the repository of Neovim's current folder. A folder named `[x] {y}` or `$HOME-like` was lost or changed even when git answered. A verifier of F12 found the first case (finding F12-P1, a space or comma in the path makes the `.git` fallback return nil). ## What changed Four problems in `lua/claudecode/cwd.lua`. The first two took a path as a pattern. The third stepped one folder down at a trailing `..`. The fourth is a flaw in my first version of the second step. 1. **The `.git` fallback** called `vim.fn.finddir(".git", start_dir .. ";")`. `finddir` reads its path as a list in `'path'` option syntax. A space or a comma split the path, and a `;` ended it. The fallback now walks up from the full path of `start_dir` and tests each folder for a `.git` folder with `vim.fn.isdirectory`. A relative `start_dir` now reaches the folders above the current one too. Before, a relative start gave a wrong answer or nil in some cases (for example `git_root("sub/deeper")` in the repository root). 2. **`normalize_dir`** passed every path through `vim.fn.expand`. `expand` reads `[`, `{`, `*`, `?`, `$` and `\` in a name as patterns or variables. A folder named `[x] {y}` or `it's` came back with a trailing slash. A folder named `$HOME-like` or `back\slash` came back nil. This also happened when `git rev-parse` answered. `normalize_dir` now returns a directory that exists as written, and expands any other string (`~`, `$VAR`). See step 4 for text that starts with `~` or `$`. 3. **`..` before Neovim 0.11.** Before 0.11, `fnamemodify(path, ":p")` keeps a last `..`, and `:h` of `a/b/..` is `a/b`. So a walk from a start folder that ends in `..` stepped one folder down and returned the wrong root. The walk now calls `simplify()` on the full path first. A verifier found this. 4. **Text that starts with `~` or `$`.** The first version of step 2 took a path that names an existing folder as written, on the raw text. `vim.fn.isdirectory` does not expand, so with `cwd = "~"` or `"$HOME"` and a stray folder of that literal name in Neovim's current folder (for example one that an unexpanded `mkdir "~/x"` made), `git_root` and `resolve` returned the stray folder where main returned the home folder. `normalize_dir` now sends text that starts with `~` or `$` through `expand` first, as a shell and `:cd` do. A verifier of the terminal change found this. `lua/claudecode/README.md` gets one new bullet that states this, with the rule for text that starts with `~` or `$`. It sits after the "Terminal cwd precedence" bullet. It names `git_root` and `resolve` only, and it says that the terminal still passes a static `cwd` and a `cwd_provider` result through `vim.fn.expand` itself. ## Scope - Only `cwd.lua` changes in code. Steps 1 and 2 are one change of idea: a path is a literal, not a pattern. Step 3 is a quirk of `fnamemodify` before Neovim 0.11. Step 4 closes a hole that step 2 opened. - `normalize_dir` serves `cwd.git_root` and `cwd.resolve`. Nothing in `lua/` calls `cwd.resolve`. The terminal calls `cwd.git_root` when `git_repo_cwd` is set, so this PR fixes folder names with `$` and `\` on that path: when git does not answer, the terminal now gets `$HOME-like`, `back\slash`, `[x] {y}`, a space and a comma right, where main gave nil or the repository of Neovim's current folder. A static `cwd` and a `cwd_provider` result do not go through `normalize_dir`: `terminal.lua:build_config` passes them through `vim.fn.expand` itself, so this PR does not change what the terminal does with those. An absolute start path that ends in `..` is fixed here, through the `simplify()` call above. - Two gaps stay for separate follow-ups. Main already has both, and this PR does not reach them. First, the fallback finds a `.git` folder only, not a `.git` file in a worktree or submodule. Second, the walk is lexical, so a link into another repository answers with the repository of the link's own folder, where git answers with the link target's repository. The terminal's `expand` of a static `cwd` and of a provider result is a third follow-up, and it has its own change. - `~` and `$VAR` still expand in `cwd.resolve` (the spec checks both). The spec's cases for `cwd.resolve` are named as `cwd.resolve` cases, because they do not test the terminal. - `git rev-parse` still runs first. Its result for a plain path is the same string as before. ## Blast Radius - User-visible: a repository in a folder with a space, a comma, a quote or another path character is now found when git cannot run. With git, `git_root` returns a folder with `[`, `{`, `*`, `?`, `$` or `\` in its name exactly. It does not reach the terminal through a `cwd_provider`: `build_config` still expands the provider's result, so the root README's example still loses `$` and `\` there (follow-up). A plain path gives the same result as before. - The fallback result is an absolute path with no `..` part. Before it could be relative. The one exception is a relative start whose name begins with `~`: Vim reads `~` as the home folder and `~name` as a user's home folder, so `:p` leaves `~name` relative and the result can be the relative `~name`. That is a pathological case, and no caller in `lua/` passes a relative path (the terminal passes the file's folder from `expand("%:p")` or `getcwd()`). - A string that names an existing folder is taken as written, except text that starts with `~` or `$`. That text always goes through `expand` first, so a folder named `~` or `$HOME` in Neovim's current folder does not take the place of the home folder, as on main. The cost: a relative folder name that starts with `$` and reads as a variable (`$HOME-like`, `$odd/sub`) is expanded and not found, as on main. A lone relative `$odd` that names no variable is left unchanged by Vim and is still found. An absolute path never starts with `~` or `$`, so every folder name this PR fixes keeps working. The change applies to `git_root`'s `start_dir` and to `cwd.resolve`. The terminal's own `expand` of a static `cwd` and a provider result is a separate change. - Neovim 0.8: the code uses `vim.fn.isdirectory`, `vim.fn.fnamemodify` and `vim.fn.simplify`, which exist there. I ran the new spec on Neovim 0.8.0, 0.10.0 and 0.12.3. The `..` case fails on 0.8.0 and 0.10.0 without the `simplify()` call, and passes on 0.12.3 either way. - `covered.lock`: `cwd.lua` is the terminal's working-directory lookup. `check.sh` printed STALE for the file hash of `cwd.lua` only, with no changed block or call site. The change cannot reach diff state, an openDiff answer, a disconnect or a diff command. The model passed (`main`: 89205 distinct states, `live-DisconnectedCallsAnswered`: 5269). `check.sh --record` wrote the new lock and `check.sh --hash-only` reports that it matches. ### Merge with coder#539 (F12) coder#539 landed first. This PR's merge commit with `origin/main` resolves the interplay: it re-records `covered.lock` and changes the one stale test in coder#539's `cwd_spec.lua` (see Verification). F11 (coder#535) merges with this PR without a conflict. ## Verification Red before the fix, green after (same spec, only `lua/claudecode/cwd.lua` swapped): | Spec | origin/main | with the fix | | --- | --- | --- | | `tests/integration/cwd_path_characters_spec.lua` (37 cases, real Neovim, 0.8.0 and 0.12.3) | 20 successes, 17 failures | 37 successes, 0 failures | | the new case "goes up from a start folder that ends in .." at `ede2f733` (before the `simplify()` call) | fails on 0.8.0 and 0.10.0, passes on 0.12.3 | passes on 0.8.0, 0.10.0 and 0.12.3 (35 successes when added, 37 at the final head, 0 failures on each) | | the two cases "expands a leading ~ / $ even when Neovim's cwd holds a folder named ~ / $HOME", with `cwd.lua` from `ca9e61c0` (before the guard) | 35 successes, 2 failures on 0.8.0 and 0.12.3 | 37 successes, 0 failures on each | The spec makes real folders and runs `cwd.git_root` on them, in two modes. In the first mode git is off `PATH` (the shell keeps its absolute path), so `git` ends with "not found" and a list command raises E475, as on a host without git. In the second mode a real `git init` makes the repository. The folder names are: a space, a comma, a semicolon, single and double quotes, brackets and braces, parentheses, non-ASCII letters, a star and a question mark, a percent sign and a hash, a backslash, a dollar sign, a leading tilde, and a plain name. Each name runs from the repository folder and from a folder two levels below it, and the answer must equal the repository path with no trailing slash. A folder that is not a repository returns nil, whatever its name. Seven more cases cover a relative start folder, a start folder that ends in `..`, `cwd.resolve` with `git_repo_cwd`, a static `cwd` with brackets and a star in `cwd.resolve`, `~` and `$VAR` in a setting of `cwd.resolve`, and two cases where Neovim's current folder holds a folder named `~` or `$HOME` and the setting must still expand. The 17 red cases are 10 of the no-git names, 4 of the git names, the relative start, `resolve`, and the static `cwd`. Gates on the final head `f12368bd`, which contains a merge of `origin/main` (05b9785, with coder#551, coder#535, coder#494, coder#545, coder#553, coder#555 and coder#557) (private XDG folders). An independent verifier passed `c73ab044`. Since then the branch has three changes of its own and two merges with main. The changes are a docs commit (the README sentence about where the walk starts), the fix for text that starts with `~` or `$` (step 4, with two spec cases and the README clause), and the `covered.lock` record for it. For the lock I ran the full `check.sh`: the model passed (89205 distinct states, 5269 live states, every fact TRUE), and only the file hash of `cwd.lua` was stale, with no changed block or call site. - `mise run all`: native exit 0. luacheck: 0 warnings / 0 errors in 186 files. busted: 1756 successes / 0 failures / 0 errors / 29 pending. treefmt: 0 files changed. Since coder#545, `mise run all` also runs the static proofs of the `verify-claudecode-nvim` skill, and they pass. - `mise run format-check`: native exit 0 (428 files, 0 changed). - `scripts/run_integration_tests_individually.sh` on Neovim 0.12.3: 564 successes, 0 failed, 0 errors, native exit 0. On Neovim 0.8.0: 427 successes, 0 failed, 0 errors, native exit 0 (the 0.8.0 run skips the specs that need 0.9). The new spec gives 37 successes on both. It starts about 100 processes (git and a shell), so it takes about 6 s on a quiet host and can pass the runner's 40 s limit at a load average above 100. A TIMEOUT line there means the host was slow, not that the spec hung. - All four `.agents/skills/verify-*/check.sh --hash-only` match their `covered.lock`. The merge with `origin/main` had two parts to resolve in an earlier commit. `covered.lock` conflicted on the hash line of `cwd.lua`, so I ran the full `check.sh` and `check.sh --record`. coder#539's `tests/unit/cwd_spec.lua` had a test that stubbed `vim.fn.finddir`, which the fallback no longer calls, so that test now walks up real folders. It does not depend on where `TMPDIR` is: it passes with `TMPDIR` inside a git checkout too. `cwd.lua` itself merged without a text conflict. The two latest merges needed no `covered.lock` change: coder#551 conflicted only in `tests/mocks/vim.lua`, where the branch keeps both its `simplify` entry and coder#551's `wordcount`, and coder#535 and coder#494 merged without a conflict. An independent verifier found the `..` case, the README wording and the other points that this body now states. The `terminal.lua` expand and `.git` files in worktrees are gaps that main already has. They are follow-ups, not part of this PR. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
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.
Why
The plugin's code text and debug log must say what the code does. Three small places did not. A client with a wrong token was logged as authenticated. One git lookup started two git processes. A comment gave the wrong scope for the PRNG seed.
What changed
lua/claudecode/server/init.lua).on_connectruns at the TCP accept, before the handshake and the token check. With an auth token it loggedAuthenticated WebSocket client connectedthere, so a client with a wrong token got that line before the server rejected it.on_connectnow logsWebSocket client connected, awaiting authentication.on_openruns after the handshake passed the check and now logsAuthenticated WebSocket client connected. The line without a token (WebSocket client connected (no auth)) is the same.lua/claudecode/cwd.lua).git_rootcalledvim.fn.systemlistinside apcallonly to see whether it takes a list, then called it again for the result. It now keeps the result of the first call. The shell-string fallback for asystemlistthat refuses a list is the same.lua/claudecode/server/tcp.lua). The comment said the PRNG is seeded once per process.rng_seededis a module local, so it is seeded once per load of the module. I fixed the comment and left the seeding alone. A second seed in one process is harmless, because it mixes in the time and a sub-second source. Neovim loads the module once, so a fresh Neovim still seeds once, which is all that [BUG] find_available_port probe-then-rebind races; create_server has no retry → EADDRINUSE with parallel Neovim instances (regression in #282) #283 needs. A real once-per-process guard would need global state that nothing else uses.READMEs:
lua/claudecode/server/README.mddescribeson_open,on_connectand the seeding scope.lua/claudecode/README.mdsays git runs at most once for each lookup (a missing folder or a nil start folder runs no git). The seeding line has the same text as the line on thedocs-gtz7branch, so the two merge without a conflict.Scope
No behavior changes except the two log lines and the number of git processes. The handshake, the token check and the shell fallback in
git_rootare untouched. I added no test for the comment, because it has no behavior to test. A real Neovim probe confirms its new claim (see Verification).Blast Radius
Authenticated WebSocket client connected: <id>moves from the TCP accept to after the handshake. Nobody parses it in this repo (I grepped code, tests, scripts, fixtures and docs).git_root: one process fewer for each lookup. The result and theshell_errorit checks come from the call that remains.covered.lock: the diff touches three covered files (cwd.lua,server/init.lua,server/tcp.lua) and none of their covered blocks.check.shprinted STALE for the three file hashes only. It printed no changed block and no changed call site. The change cannot reach diff state, an openDiff answer, a disconnect or a diff command.on_disconnect,M.stopand the request handlers are unchanged.on_connectandon_openonly gain or move alogger.debugcall.tcp.luachanges a comment.cwd.luais the terminal's git root lookup. The model passed (main: 89205 distinct states,live-DisconnectedCallsAnswered: 5269).check.sh --recordwrote the new lock andcheck.sh --hash-onlyreports that it matches.Verification
Red before the fix, green after (same specs, only the three
lua/files swapped):tests/unit/server/connect_log_spec.lua(4 new cases: log order and noAuthenticatedfor a TCP-only client or a wrong token)tests/unit/cwd_spec.lua(5 new cases: git invocations per lookup)Real Neovim probes (loopback server with a raw TCP client, and a real git repository), before and after:
server: Authenticated WebSocket client connected: client_1was logged first, thenRejected client_1: Invalid authentication token. After the fix the wrong-token client has noAuthenticatedline. The right-token client gets it afterClient authenticated successfully. Lines withAuthenticatedfor the two clients: 2 before, 1 after.git_rooton a real repository: 2 git invocations before, 1 after.tcp.luaseeding: 1 seed for one load and two port searches. 2 seeds after a reload of the module and one more search.Gates on the final commit, which merges
origin/main(036427a) into the branch (private XDG folders):mise run all: native exit 0. luacheck: 0 warnings / 0 errors in 180 files. busted: 1691 successes / 0 failures / 0 errors / 24 pending. treefmt: 0 files changed.mise run format-check: native exit 0 (357 files, 0 changed).tests/unit/server/,server_spec,server_tool_call_log_spec,cwd_spec,terminal_specandtests/unit/terminal/): 556 successes, 0 failures.scripts/run_integration_tests_individually.sh: 331 successes, 0 failed, 0 errors..agents/skills/verify-diff-lifecycle/check.sh --hash-only: covered.lock matches the code.The merge with
origin/mainconflicted inlua/claudecode/README.mdandlua/claudecode/server/README.md, where the README refresh (#533) rewrote the lines this PR edits. I kept main's text and reapplied this PR's two changes (theat most oncewording and theon_openlog). Two independent verifiers (Opus and GPT) checked the head before the merge withorigin/main. Both found no introduced defect. They reran the red and green specs, reverted each code change alone to see the new specs fail, and ran real loopback clients against the server. Their wording findings are in the branch (the README line says "at most once", and theon_opencomment says "with a token").Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh