Repository navigation
fix(selection): send no terminal cursor and do not recurse when the held buffer becomes a Claude terminal - #493
Merged
Merged
Conversation
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b4b0392025
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
🛡️ 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. |
…e Claude terminal
…st comment back The verified triggers are termopen() in the held buffer and a rename to a term://...claude name. update_selection also cancels the demotion timer in the terminal. The on_reload comment belongs above its own case. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
Member
Author
|
@codex review |
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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 87b9e0174c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
… the Claude terminal
…inal itself While you are in a Claude terminal, the buffer of the held selection can become a Claude terminal too (a rename to a term://...claude name, or termopen() in it). Its text then changes, and the held-text check took the buffer for an ordinary one and sent its cursor, with a term:// path, to Claude. The check now treats a held buffer that is a Claude terminal like the case where you are in it: nothing is sent, the read is forgotten and a pending demotion is cancelled. Tests: a unit case and a real-Neovim case for the new path (red on the previous head). The cases of the earlier commits now also assert that Claude keeps the selection it had and that no selection or cursor reached the broadcast. The verify-diff-lifecycle lock is re-recorded (only the hash of selection.lua changed). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
ThomasK33
changed the title
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
|
Codex Review: Didn't find any major issues. What shall we delve into next? Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
ThomasK33
added a commit
that referenced
this pull request
Nov 11, 2026
… fact regex to its own guard #493 changed demote_if_selection_text_changed (a held buffer that is a Claude terminal sends no cursor), so the regex of TerminalReportsHeldBuffer read FALSE. It now reads the new lines. Seven regexes read more than their own guard: removing one guard from selection.lua turned a second fact FALSE (FlushSkipsOperator and FlushSkipReports, FlushRecordsCursor and ReadRecordsTick, UpdateSkipsTerminal and UpdateChecksHeldText, PendingKeepsHeld and PendingClearsHeld, DebounceIgnoresStale and DemotionIgnoresStale with ClearsBeforeClose, ReadRecordsTick and ListensToSelectionBuffer). Each regex now anchors on lines of its own guard only. A script that removes each of the 24 guards alone shows that exactly its own fact turns FALSE. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
ThomasK33
added a commit
that referenced
this pull request
Nov 11, 2026
… user sees there - A held buffer that becomes a Claude terminal (the recursion fixed by #493) is named in the scope list. - ReconcileOnTextChanged and TextChangeReports break NoDeletedText only in the model: the buffer listener also covers an edit of the current buffer on real Neovim. The text now says so, and so does the replay section. - Each not-modeled item says what a user sees. A new replay shows the line-inserted-above limit. - HeldEndsWhenMoved says "in a file", the listener is in the list of what ends a hold, the not-covered list names the two utf8 helpers, and the terminal-check remark says no TLC run tested the difference. - The state count and the update steps follow the queued listener check. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
ThomasK33
added a commit
that referenced
this pull request
Nov 11, 2026
The model passes on the merged tree (178,962 distinct states) and all 24 facts read TRUE. The change of #493 sits in demote_if_selection_text_changed: a held buffer that is a Claude terminal sends no cursor, cancels a pending demotion and forgets the read. It is outside the model (SKILL.md names it in the scope list). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
This was referenced Nov 11, 2026
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 12, 2026
…swap file and catch an overflow (coder#496) ## Two gaps in the real-Neovim cases of coder#493 coder#493 added three cases to `tests/integration/selection_held_spec.lua` that make a buffer look like the Claude terminal. The verifier of coder#493 found two gaps in them. Both are in the test only. No `lua/` code changes. 1. **A stale swap file fails the cases with E325.** Each case renames a buffer to the fixed name `term://x//1:claude`. Neovim opens a swap file under the new name at the rename. If a Neovim that a timeout killed left a swap file with that name, or if concurrent runs share one `HOME`, the rename raises `E325: ATTENTION` and the case fails for a reason that has nothing to do with the plugin. The new helper `rename_to_claude_terminal(buf)` sets `swapfile = false` on the buffer before the rename, so no swap file exists under that name. 2. **The "demotion is pending" case did not check `v:errmsg`.** It asserted only that nothing was broadcast, so it passed on code that overflows the stack at that point. It now clears `v:errmsg` before the edit and asserts that it is still empty afterwards, as the first of the three cases does. ## Proof - Real Neovim, with a stale swap file `term:%%x%%1:claude.swp` in `$XDG_STATE_HOME/nvim/swap` (left by a Neovim that I killed with SIGKILL after it renamed a modified buffer): - Spec from `main` (before this PR), 0.12.3: the three cases fail with `E325`. - Spec from this PR, with the same swap file: 14 of 14 pass on Neovim 0.12.3 and on v0.8.0. - With the `selection.lua` from before coder#493 (`5faad5b`), the spec of this PR fails 3 cases, including the "demotion is pending" case. The spec from `main` fails only the other 2 on that code. - `mise run format-check` and `mise run check` are clean. `mise run test`: 1396 successes, 0 failures (seed 1794381885). --- _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
…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`_
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.
A held selection's buffer becomes a Claude terminal
When the buffer of a held selection becomes a Claude terminal after the selection was read, and its text changes, two things went wrong. Neovim raised
stack overflowfromCursorMoved,TextChangedandvim.schedulecallbacks, and a cursor of the terminal buffer, with aterm://...path, could reach Claude. This PR fixes both. It is a follow-up to #481, found by the review of that PR and by the verifier of this one.Claude must never get a selection or a cursor of a Claude terminal buffer: its text is Claude's own prompt. The flush and
update_selectionignore such a buffer, and this PR makes the held-text check from #481 do the same.How it happens
A buffer becomes the Claude terminal after a selection was read in it with
termopen(), or with a rename to aterm://...claudename. The held-text check (demote_if_selection_text_changed, added in #481) then runs on a buffer that is a terminal:update_selectiondoes nothing in the Claude terminal, except that since fix(selection): end a held selection when its file changes while you are in the Claude terminal #481 it calls the check there. The check ended every selection in the current buffer withM.update_selection(). If the current buffer is the terminal and also the buffer of the selection, the two functions call each other until the stack overflows. The reviewer of fix(selection): end a held selection when its file changes while you are in the Claude terminal #481 reproduced this with the rename, and I did the same on real Neovim 0.12.3. A customterminal_cmdafter a plugin reload did not reproduce it: the native provider adopts the old terminal at the first terminal check.handle_selection_demotionknows only the terminal that the provider registered. It then sends the cursor of the terminal buffer (found by Codex in round 2, confirmed by the verifier).term://...path. This path exists onmainsince fix(selection): end a held selection when its file changes while you are in the Claude terminal #481 (found by the verifier).The fix (
lua/claudecode/selection.lua)In
demote_if_selection_text_changed, one branch handles a held buffer that is a Claude terminal while you are in a Claude terminal (the same one, or another):M.update_selection()only when the current buffer is not a Claude terminal, so the two functions cannot call each other.cursor_at_flush,last_active_visual_selection), as before.M._cancel_demotion_timer()).selection_tick), so nothing checks that buffer again and its listener detaches at its next change.cursor_in_other_bufferis called only for a held buffer that is not a Claude terminal, which is the fix(selection): end a held selection when its file changes while you are in the Claude terminal #481 case that stays as it was.Claude keeps the selection it already has: nothing in this branch replaces
latest_selection.Proof
start()path: selectalpha, press Esc, rename the buffer toterm://x//1:claude, deletealphawithnvim_buf_set_text. Onorigin/main:Error in CursorMoved Autocommands,Error in TextChanged Autocommands, andLua callback: stack overflowinv:errmsg. With the fix: no error, and no broadcast.tests/selection_test.lua(3 cases for this PR): no recursion, a pending demotion is cancelled, and nothing is sent when you are in another Claude terminal. Each asserts that nothing was broadcast and thatget_latest_selection()still returns the held selection (alpha). The recursion case also asserts the held state is gone, the read is forgotten and the listener detaches at its next change. The case for path 3 is red on the previous head (it sends theterm://cursor). A mutant that also clearslatest_selectionin the new branch fails all three.tests/integration/selection_held_spec.lua(real Neovim, 3 cases): the same three paths. Each records everyselection_changedbroadcast and asserts that none was sent and thatget_latest_selection()is stillalpha. The first and third also assert that the read is forgotten, and the first also asserts thatv:errmsgstays empty. The case for path 3 is red on the previous head. The whole spec passes on Neovim 0.12.3 and v0.8.0 (14 of 14).mise run format-check,checkandtest: 1344 successes, 0 failures.selection.luaand the integration spec have 0 luacheck warnings, andtests/selection_test.luahas the one thatorigin/mainhas..agents/skills/verify-diff-lifecycle/covered.lockis re-recorded: only the hash ofselection.luachanged.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh