feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking by ThomasK33 · Pull Request #477 · coder/claudecode.nvim

ThomasK33 · 2026-11-10T18:19:23Z

Status

#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 #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 #540 fixes all three. Their replays print BUG on main until #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 #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 (#452), and so are the cases that reviews found afterwards (#471, #481, and the recursion of #481's code that #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 #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 #452. Each path was replayed on Neovim 0.12.3. #452 fixed all four:

HeldEndsWhenMoved: Claude kept a released selection after the cursor left it (vb Esc gv d, or ve Esc l h inside 100 ms).
NoDeletedText: Claude kept a held selection after you edited its text without moving the cursor (viw Esc x x).
SameFile: with a long visual_demotion_delay_ms, Claude held another file's cursor (:b b.txt, :b a.txt).
ClaudeSeesCursor: with a long visual_demotion_delay_ms, Claude held a cursor position you had left (Esc l, wait, h).

#471 closed the case a Codex review of #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.

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

#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 #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 #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 #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).

#457 and #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 fix(selection): end a held selection when its file changes while you are in the Claude terminal #481 guards add three (24 in all), and the fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 fix(selection): end a held selection when its file changes while you are in the Claude terminal #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 fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 fix(selection): check a plugin's edit in visual mode at the next key #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 fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 (fix(selection): check a plugin's edit in visual mode at the next key #540). On fcea49af the three probes for fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #524 print BUG on both versions. In a tree with fix(selection): check a plugin's edit in visual mode at the next key #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 fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 (fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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 (fix(server): log Authenticated after the token check and run git once per lookup #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: fix(mention): deliver queued @mentions once, in order, or report an error #454 (server.broadcast returns, mention queue), fix(selection): end a held selection when its file changes while you are in the Claude terminal #481, and fix(selection): send no terminal cursor and do not recurse when the held buffer becomes a Claude terminal #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. fix(server): drop a client that answers pings but never reads #467 and fix(diff): keep the sign column and diff mode the user sets in windows a closed diff leaves #491 touch no covered file of this skill. fix(tools): answer malformed tools/call and close_tab with -32602 #497 changed one debug log argument in the tools/call handler of server/init.lua, and fix(server): hold the disconnect cleanup until Neovim allows window changes #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

.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 fix(selection): check a plugin's edit in visual mode at the next key #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 • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

…n tracking Model-checks what Claude sees as the user's current selection (lua/claudecode/selection.lua) against guards read from the code, with nine rules, 21 code facts, and five headless-Neovim replays of the paths that once broke a rule (fixed by #452 and #471). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…ging main #454 changed what `server.broadcast` returns (`true` only when a connected client took the message) and moved the mention queue from `on_connect` to `on_open`. `send_selection_update` ignores the return value and `on_connect` still sends no selection, so no rule or fact changes. `M.stop` changed only a comment. The model still passes (89,313 distinct states), the five replays still print OK. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 · 2026-11-10T18:20:04Z

@codex review

ThomasK33 · 2026-11-10T18:20:06Z

@codex security review

chatgpt-codex-connector · 2026-11-10T18:20:17Z

Codex Review Summary: ✅ Completed

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

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-11-12T07:12:15.471673Z	`0a1d9fd`	Manual request
🔒 Security Review	✅ Completed 2026-11-12T07:12:55.910463Z	`0a1d9fd`	Manual request

ℹ️ About Codex in GitHub

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

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

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

chatgpt-codex-connector · 2026-11-10T18:23:08Z

Codex Review: Didn't find any major issues. 🚀

Reviewed commit: ac7f243677

ℹ️ About Codex in GitHub

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

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

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-11-10T18:24:35Z

🛡️ Codex Security Review

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

Reviewed commit: ac7f243677

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

…ify-selection-tracking An independent review of #477 found two guards that the model called redundant: - `LeaveNoted` breaks `HeldEndsWhenMoved` alone when the user can visit a second file. `--mutants` ran that rule with one file, so it never saw it. It now runs with two. - `ReconcileOnTextChanged` looked redundant because no model step fired `TextChanged` without `CursorMoved`. Real Neovim shows it matters: a plugin edit of the held text keeps the old selection without it. The model gets a `YouEditByPlugin` step, and `replays/held_after_plugin_edit.lua` replays the path. Also: the `FlushSkipsTerminal` regex no longer matches the later operator-skip `return`, `run.sh` prints its usage with no argument and exits 1 on BUG, and SKILL.md states what the operator step, the one text version per buffer and typeahead mean for the model. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

The run now has 21 keys and runs HeldEndsWhenMoved with two files: 2853 s on a host with a load average of 60, about 30 minutes on a quiet one. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…-selection-tracking The model gets a YouEditOtherBuffer step (a reload or a plugin edit of a file that is not the current buffer: no TextChanged, no BufEnter) and three facts, ListensToSelectionBuffer, TerminalReportsHeldBuffer and UpdateChecksHeldText, for the guards that #481 added to selection.lua. NoDeletedText covers the path now. FlushSkipReports breaks no rule alone any more, because the terminal's debounce check finds the stale text: it is caught with EntryClearsHeld. NoDeletedText runs with two files in --mutants. Two replays, a reload and a plugin edit while you are in the Claude terminal, are red on main before #481. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 · 2026-11-11T04:18:55Z

@codex review

ThomasK33 · 2026-11-11T04:18:57Z

@codex security review

chatgpt-codex-connector · 2026-11-11T04:22:12Z

🛡️ Codex Security Review

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

Reviewed commit: f91391f1ca

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: f91391f1ca

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

…ny checkout path replays/run.sh used `timeout`, which macOS lacks, and put the checkout path into `set rtp^=` and `luafile` commands, so a path with a space broke the run. The watchdog is plain bash now. The paths go through the environment, and Neovim's Lua API escapes them (the lua directory is also on package.path, because a comma in 'runtimepath' is not enough for require). --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…-tracking model The listener on the buffer of a held selection only queues its check with vim.schedule (check_soon). The model ran that check at the edit. It now sets a queued-check bit (`chk`) at the edit, and a separate step `ListenerCheckRuns` runs demote_if_selection_text_changed in whatever state the user is in by then. `Settled` waits for the queue to be empty. The main run grows to 178,962 distinct states and still passes. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

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

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

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

`check.sh --mutants` took 4957 s on the head with the queued listener step, at a load average near 25 (3012 s and 3082 s before it, at about 10). The plain run takes about a minute now. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

#497 changed one debug log argument in the tools/call handler of lua/claudecode/server/init.lua (`tostring(params.name)`). It is outside M.broadcast and the on_connect callback, which the model describes, and it cannot reach the selection state, a timer, or a send. Only the file hash changed. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 · 2026-11-11T09:09:51Z

@codex review

ThomasK33 · 2026-11-11T09:09:53Z

@codex security review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 91660323be

ℹ️ 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 visual-mode edit limit The HeldInTerminal row had four cells, the HeldUntilMoved row two, and the delimiter four (Codex round 4, P2). Each row has three cells again, and the table renders. Codex round 4 also found a path that the model cannot reach: a plugin edits another line while you are in visual mode, and you press Esc inside the 100 ms debounce. The flush takes the moved changedtick for an operator that consumed the selection, so Claude gets the cursor and not the selection (replayed on Neovim 0.12.3). The model has no edit step in visual mode and one text version per buffer, so SKILL.md names it as a limit of the code with what a user sees, and a new replay shows it. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…on-tracking

…y in verify-selection-tracking #524 replaced the changedtick comparison in the flush with a visual_entry that the buffer listener marks. Read the new guard (FlushSkipsOperator), the listener that counts a visual edit (ListenerNotesVisualEdit) and the check that spares a plugin's edit (VisualCheckSparesPluginEdit), and keep the old comparison as the fact FlushIgnoresTick (FALSE on the code before #524). The model gets two steps that move only the changedtick while you select: a plugin's edit of another line and a :write.

…are in the Claude terminal (coder#481) ## What Claude holds is what you see, one case more Claude keeps the text you selected after a file changes under it, as long as you stay in the Claude terminal. You select `alpha`, press Esc, go to the Claude terminal and ask a question. Claude rewrites the file on disk, Neovim reloads it (`autoread`, `:checktime`, or a focus change), and `getCurrentSelection` still answers `alpha` for a file that no longer has it. The same happens when a plugin edits the file. Coming back to the file heals it. Until then Claude answers about text that is gone. This PR ends the hold in that case: Claude gets the cursor of the file, in the window where you left it. ## Why coder#452 missed it A selection survives a visit to the Claude terminal (issue coder#246), and nothing updates the selection while the terminal is current. coder#452 ends the hold when the held text changes, but it checks that from `TextChanged` and `BufEnter`. `TextChanged` fires only for the current buffer, and a reload or a plugin edit of the file does not fire `BufEnter` either. `demote_if_selection_text_changed` also returned when the selection's buffer was not the current one. The verify-selection-tracking model (coder#477) had no step that edits a buffer that is not current, so it could not see this. A reviewer of coder#477 found it. ## The fix (`lua/claudecode/selection.lua`) 1. Each time a visual selection is read (`record_selection_read`, in the flush and in the in-visual update), the plugin also attaches a listener to that buffer with `nvim_buf_attach` (`on_lines`, `on_reload`, `on_detach`). It is attached once per buffer: `watched_buffers` records it, and the entry is cleared only when the listener detaches (`on_lines` returns `true`, or Neovim calls `on_detach`). The exception is a module reload without `disable()`: the old module's listener stays on the buffer, and the new module attaches its own. 2. The listener detaches itself at the next `on_lines` after Claude no longer holds a selection of that buffer (the callback returns `true`). While it is attached, one change, or a burst of them (`:%s`), schedules one check. 3. `demote_if_selection_text_changed` now also runs when the Claude terminal is current and the selection's buffer is another one: if the changedtick moved and the held text is no longer at its range, it clears the held state and sends the cursor of that buffer. `update_selection` cannot do that, because it does nothing in the Claude terminal. The cursor is where a window shows the buffer. A buffer in no window gets the position where you released the selection, kept inside the text that is there now. 4. `:edit` and `:edit!` detach the listener (Neovim calls `on_detach`), so `on_detach` attaches it again from a `vim.schedule` callback when the buffer still holds the selection, and checks it at once. A synchronous re-attach inside `on_detach` makes Neovim loop for ever, because it detaches the listener that was just attached. `:checktime` and autoread keep the listener and call `on_reload`, whose return value Neovim ignores, so only `on_lines` can detach it. `on_detach` also fires for `:bdelete`, `:bunload` and `:bwipeout`. An unloaded buffer is left alone: `nvim_buf_attach` returns `false` for it, and a `watched_buffers` entry set before that would stay set and block the next listener after the buffer loads again. 5. `update_selection` runs the same check when the Claude terminal is current, before it returns. A new Claude terminal is not registered when `BufEnter` fires, so a file that changed while you were in another file, just before you opened the terminal, finds the check false at `BufEnter`. The 100 ms debounce is the first event that knows the terminal. The verify-selection-tracking model (coder#477) found this combination. On real Neovim the terminal's own events happen to run the check in the cases I replayed, so I could not show a stale selection there, and I did not want the fix to depend on those events. 6. When no window shows the buffer, the fallback cursor goes through `code_point_start`, so a byte column that falls inside a multibyte character moves to its first byte (`db3b731`, Codex round 3). `cursor_selection` is the table that `M.get_cursor_position` built, moved into a helper so the new code can build one for a buffer that is not current. Entering the terminal, a `:w`, an edit that leaves the held text in place, and a reload that leaves it in place all keep the selection, as before. The listener runs in the file's buffer, not only while the terminal is current. For the current buffer it is the same check as `TextChanged`, a moment earlier. ## Proof **Probes on real Neovim 0.12.3**, through the real `start()` path with real timers, on `origin/main` and on this branch: | Path (Claude holds `alpha` in a.txt, you are in the Claude terminal) | main | this PR | | --- | --- | --- | | a plugin deletes `alpha ` (`nvim_buf_set_text`), a.txt is in no window | `BUG Claude holds "alpha", a.txt is "beta gamma"` | `OK`, Claude holds the cursor at 0:4 | | Claude rewrites a.txt on disk, `:checktime` reloads it, a.txt stays in its own window | `BUG Claude holds "alpha", a.txt is "beta gamma"` | `OK`, Claude holds the cursor at 0:4 | **Tests.** All five new integration cases and 14 of the 19 new unit cases fail on `origin/main`'s `selection.lua` and pass here. Five unit cases pass on main too, because they check that something does not happen: "keeps the selection when the change leaves its text in place", "does not send a cursor while you are in another file", "does not read a buffer that was unloaded while you stay in the terminal", "does not read a buffer that was unloaded", and "stops listening when tracking is disabled". - `tests/integration/selection_held_spec.lua` (real Neovim): five new cases. A plugin edit with the file in no window, a reload with the file in its own window, a reload that leaves the text in place (the selection stays, and the next change is seen), `:bunload!` then `:buffer` then a new selection then a plugin edit (a new listener is attached), and three select-and-reload cycles that must attach one listener, not three. All five fail on `origin/main`'s `selection.lua` and pass here, on Neovim 0.12.3 and on v0.8.0. - `tests/selection_test.lua`: 19 new cases for the listener: attached once, the cursor from the window, the position kept inside the text and on the first byte of a multibyte character (`db3b731`), `:edit!` that detaches the listener, `:checktime` that keeps it (`on_reload`), one listener after a reload while only a cursor is held, a buffer unloaded and loaded again, a change that leaves the text in place, the current buffer and another file left alone, a burst checked once, detaching when nothing is held or tracking is off, and the debounce check for a terminal that was not registered at `BufEnter`. The mock of `nvim_buf_attach` now behaves like Neovim: it keeps a listener after `on_reload` whatever the callback returns, returns `false` for an unloaded buffer, and calls `on_detach` while the other listeners are still attached (a listener attached from inside `on_detach` is detached in turn, and a loop is cut after 20 calls), with `vim.schedule` running later. - Mutants. My own check: 14 mutants of the new code (no listener, never detach, clear before reading the position, no unloaded guard in the check, no re-attach, no dedupe, no window cursor, terminal not required, no row clamp, no multibyte snap, `on_reload` forgets its buffer, `on_reload` does nothing, no `nvim_buf_is_loaded` in `on_detach`, re-attach in `on_detach` without `vim.schedule`). The unit tests kill all 14. The root's verifier also ran mutants of the code at `62a11e4` (27, six survived) and at `e97f6f3`. What survived and what I did: - the `nvim_buf_is_loaded` guard in `on_detach` (it brought the bug back after `:bunload!`, `:buffer`, a new selection, the terminal and a plugin edit): killed by a unit case and a real-Neovim case, and by a mock that returns `false` for an unloaded buffer. The guard in `demote_if_selection_text_changed` has its own case. - the re-attach in `on_detach` without `vim.schedule` (Neovim loops for ever on `:edit!` or `:bunload!` of a held buffer): killed by the `on_detach` mock above. The `:edit!` cases fail with "on_detach loops". - `M19`, a listener that stays on a.txt after the hold moves to b.txt: declined, Claude holds the same text. `M24` and four others: judged equivalent, no sequence of keys reaches a different result. - `mise run format-check` and `mise run check` pass. My changes add no luacheck warning: `selection.lua` and the integration spec have 0, and `tests/selection_test.lua` has the one that `origin/main` has. `mise run test`: 1341 successes, 0 failures, 0 errors. - `.agents/skills/verify-diff-lifecycle/covered.lock` is re-recorded: only the hash of `selection.lua` changed, and that skill covers no selection code. ## Docs `ARCHITECTURE.md`, `README.md` (global side effects), `lua/claudecode/README.md` (side effects), `CLAUDE.md` and `.agents/skills/verify-claudecode-nvim/features/selection.md` say that a change to the selected text while you are in the Claude terminal sends the cursor of its file, and that the plugin attaches `nvim_buf_attach` listeners to the buffer of a held selection. ## Review record Codex rounds on exact heads: `7033002` clean, `62a11e4` clean, `beb43ee` one P2 (a fallback cursor inside a multibyte character, fixed in `db3b731`), `e97f6f3` clean, `7f48a9d` clean, `117afc4` clean. Six rounds, the limit. The root's verifier ran three times: 1. On `62a11e4`: the `on_reload` leak, the false comments about reloads and the feature doc wording (fixed in `beb43ee`), and an untested `nvim_buf_is_loaded` guard in `on_detach`. 2. On `e97f6f3`: the same untested guard (fixed with its unit and real-Neovim cases in `6eba6a5`), the side-effect lists in `README.md`, `lua/claudecode/README.md` and `CLAUDE.md` (also `6eba6a5`), and N1: a synchronous re-attach in `on_detach` makes Neovim loop for ever, and no test failed on that mutant. The `on_detach` mock now matches Neovim and a case fails on that mutant (`117afc4`). `7f48a9d` added the real-Neovim case for one listener per buffer through reloads. 3. On `7f48a9d`: PASS. It carries to `117afc4`, which changes tests only. Declined with a reason: re-reading the held range on every change (main pays the same cost through `TextChanged` when the buffer is current), and mutants `M19` and `M24`. Left as follow-ups, not fixed here: - A module reload without `disable()`: the old module's listener outlives its next `on_lines` for as long as the old module still holds a selection, and it can send a cursor that replaces the new module's selection. It needs a module reload, which a user does not do. - With `nohidden`, a file that is unloaded while you are in the terminal and then changes on disk is not seen until you return to it, because Neovim does not see that change either. ## Follow-up The verify-selection-tracking model (coder#477) gets a step for an edit of a buffer that is not current once this merges, so `NoDeletedText` covers it. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

… edits another line or writes the file (coder#524) ## Result Claude gets the selection you released, not the cursor, when a plugin edits another line or the file is written while you are in visual mode. This holds for a quick release (within the 100 ms debounce) and for a slow one. Before: `ve`, then a plugin edits line 2, then `Esc` within 100 ms. Claude got the cursor (`a.txt "" 0:4-0:4`). After: Claude holds `alpha`. ## Cause `flush_visual_selection` skips the release on `Esc` when the buffer's changedtick moved since visual mode began (the guard from coder#246). The guard is for an operator (`d`, `c`, `>`, `gU`...) that consumes the selection: the `'<` and `'>` marks then point at text you never selected, so a release would send a phantom selection. Five things move the changedtick: an operator, a plugin's edit, an undo (from a plugin or a `<Cmd>` mapping), a `:write` of a modified buffer (5 -> 6), and a reload (`:checktime`, `:edit!`). An operator and a reload consume the selection. The other three leave it on the screen. ## Fix 1. Neovim ends visual mode before an operator changes any text. A plugin's edit runs while visual mode is on. A `:write` fires no buffer callback at all. 2. `watch_selection_buffer` (the coder#481 listener on the held buffer) now also listens to the buffer you select in. There is still one listener per buffer. It detaches at the first edit after the selection is over, as before, unless the buffer holds a selection. 3. `visual_entry` no longer stores a changedtick. It stores `consumed` and `unchecked_edits`. The flush skips when `consumed` is set or an edit is unchecked. 4. Neovim 0.8 and 0.9 end visual mode for the length of an `nvim_buf_set_lines` or `nvim_buf_set_text` call, and run the callback in that state (0.10 and later run it in visual mode). So the callback only counts the edit, and `vim.schedule` reads the mode after the call. An operator's flush comes before that check, so it finds an unchecked edit and skips. A reload or a detach of the buffer during visual mode counts as an operator. The Claude terminal buffer is not listened to: its output is a stream of edits, and the flush ignores it. ## What does not change 1. A real consuming operator still sends nothing: `d`, `c`, `>`, a linewise `>`, and an operator after a plugin's edit or after a `:write`. 2. In-place operators (`gU`, `~`, `J`) stay skipped, as the old comment says. 3. If a plugin's edit and `Esc` are handled in the same event-loop turn (both are in typeahead), the check has not run, and the flush skips. That is the old behavior, not a regression. 4. A plugin edit of the selected text or of its line keeps the release: Claude gets the text that Neovim highlights after the edit. On Neovim 0.8 to 0.11, an earlier edit on the same line shifts the highlight, and a plugin that inserts lines above the selection leaves the visual anchor on its old line number. The flush sends what the editor highlights. The new spec does not test these cases. ## Tests | Where | What | |---|---| | `tests/integration/selection_visual_edit_spec.lua` (new, real Neovim) | 12 tests. For 20 ms and 300 ms between the steps: plugin edits line 2, plugin appends lines, `:write` of a modified buffer. Guards: `ved`, `vec`, `Vj>`, `d` after a plugin edit, `d` after a `:write`. Next selection does not inherit an operator. | | `tests/selection_test.lua` | 4 operator tests now fire the buffer listener as Neovim does. 8 new tests (plugin edit, `:write`, operator after plugin edit, unchecked edit, reload, next selection, detach, terminal buffer). | Red on main: 6 of the 12 integration tests (the plugin-edit and `:write` cases at both delays). The 6 guards pass on main. Mutants, all killed: 2 integration (the flush never skips, every edit counts as consumed) and 8 unit (flush never skips, unchecked edit ignored, always consumed, never consumed, reload ignored, entry not cleared, terminal watched, no detach). Checked on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3: the new spec passes 12 of 12. Gates: `treefmt --ci` is clean and luacheck shows 0 warnings in 178 files. Busted gives 1663 unit tests passed, 0 failed, 24 pending (no coverage). The integration runner, once normally and once under a `TMPDIR` named `odd tmp 50%`, in a private `HOME`, passes 331 tests per run on 0.12.3 and 244 per run on 0.8.0, with 0 failures. `verify-diff-lifecycle/check.sh` matches after the re-record: only the hash of `selection.lua` changed, which cannot reach diff state, and the model passes (89,205 distinct states). The docs say what the listeners do (`lua/claudecode/README.md` and the Global Side Effects list in `README.md`). ## Follow-up `verify-selection-tracking` (coder#477) models the changedtick. It gets a separate round after this merges. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

The model reads the new visual_entry guard (FlushSkipsOperator, ListenerNotesVisualEdit, VisualCheckSparesPluginEdit) and the old comparison as FlushIgnoresTick. The hashes of the flush, on_mode_changed and watch_selection_buffer blocks changed, and visual_entry_of and note_visual_edit are new blocks. The file hashes of init.lua and server/init.lua changed with main: no block the model reads changed there.

…select, and name the one-typeahead limit Three probes for #524: a plugin edits another line, a plugin appends lines, and :write runs while you are in visual mode, then Esc inside the 100 ms debounce. Claude must get the selection. They print BUG on the code before #524 and OK on main, on Neovim 0.12.3 and 0.8.0. The old limit replay quick_release_after_plugin_edit_in_visual.lua becomes the first one, with the verdict that #524 made true. A mapping that edits and presses Esc in one typeahead still reaches the flush before the check, so that limit gets its own replay.

…ree doc minors in verify-selection-tracking Facts table, the #524 path in Bugs this model found, the new step names, the replays table, the holdLoose exemption (HeldInTerminal too), the 'rows whose rule is none' wording, and the unloaded-buffer return in Not modeled.

…ing replay, and give the reason for the one-bit changedtick

…on-tracking

…ured --mutants time

ThomasK33 · 2026-11-12T03:59:06Z

@codex review

ThomasK33 · 2026-11-12T03:59:08Z

@codex security review

chatgpt-codex-connector · 2026-11-12T04:02:32Z

🛡️ Codex Security Review

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

Reviewed commit: f974ee0698

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

chatgpt-codex-connector · 2026-11-12T04:06:25Z

Codex Review: Didn't find any major issues. Chef's kiss.

Reviewed commit: f974ee0698

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

…ad the old listener in ListensToSelectionBuffer Opus and GPT verified f974ee0 and found one documentation defect: 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, and two more ways to get there are reproduced (a key that arrives during the plugin's callback, an autocmd edit at a mode change). They get replays that print BUG until #540 merges. Also: check.sh prints only the first broken rule, the operator order sentence (on_lines first, ModeChanged after) is fixed, and the ListensToSelectionBuffer regex reads both forms of on_lines (it read FALSE on the code before #524, which listens).

…on-tracking

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

ThomasK33 · 2026-11-12T07:09:43Z

@codex review

ThomasK33 · 2026-11-12T07:09:46Z

@codex security review

chatgpt-codex-connector · 2026-11-12T07:12:14Z

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

Reviewed commit: 0a1d9fd3ee

ℹ️ About Codex in GitHub

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

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

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-11-12T07:12:54Z

🛡️ Codex Security Review

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

Reviewed commit: 0a1d9fd3ee

View security finding report

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

ℹ️ About Codex security reviews in GitHub

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

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

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

…oder#540) ## What a user sees You select text in visual mode, a plugin or a mapping edits another line, and your Esc is read before the plugin has checked that edit. The selection is untouched and its text is still there, but Claude gets the cursor and not the selection. coder#524 fixed the case in which the check ran before the key. Three ways to read the key first also failed on `main`, and this PR fixes all of them: 1. A mapping that edits and presses Esc in one key sequence, for example `<Cmd>lua edit_other_line()<CR><Esc>`. 2. A key that arrives while a callback runs, as a UI sends it (`nvim_input`): during the plugin's own timer callback, or during another one that was queued before the check. 3. An autocmd that edits when visual mode starts (a `ModeChanged` handler for `n:v`) with the Esc already in the typeahead (`ve<Esc>`). The replays of `verify-selection-tracking` print `BUG` on `main` for each of them, 3 of 3 runs on Neovim 0.8.0 and 0.12.3, and `OK` with this change. ## Cause The flush on visual exit skips a selection that has an edit nobody checked yet (`entry.consumed or entry.unchecked_edits > 0`). An operator (`d`, `c`, `>`) edits the text and then ends visual mode, and its flush runs before any check, so that skip is what stops a phantom selection. A plugin's edit leaves visual mode on. The check that tells the two apart (is visual mode still on?) ran only in `vim.schedule`, and a schedule runs after the command or callback that made the edit returns, and after any callback that was queued before it. When a key is read first, the flush takes the plugin's edit for an operator's. ## The fix `lua/claudecode/selection.lua`: - `check_visual_edits(entry)` is the old scheduled check as its own function. It judges every edit that is waiting at once, by the mode that they left (visual mode on: a plugin's edit, benign. Off: an operator consumed the selection). It does nothing for a stale entry or when nothing waits, so running it twice is safe. - `note_visual_edit` still counts the edit and schedules the check, and it now also sets a `vim.on_key` listener (one namespace, made on first use). Neovim calls the listener for the next key before it processes that key, also for a key that comes from a mapping or that a UI sends, so the Esc finds visual mode still on. Whichever of the schedule and the key comes first runs the check, and the check clears the listener. - An operator's flush still comes before both, so `d`, `c`, `>` and the other operators skip as before. A listener of a flushed selection does nothing at the next key and clears itself, so it can live until that key (README says "at the latest until the next key"). I checked the key listener on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3 (a probe script, not the plugin): it fires for the `<Esc>` of a mapping before it is processed with the mode still `v`, a second `vim.on_key(fn, ns)` replaces the first, and `vim.on_key(nil, ns)` is safe inside the callback and for an unregistered namespace. I did not try the range of the edit (`on_lines` receives the changed lines) as the test for whether it touched the selected lines. By my reasoning, which I did not test, a plugin edit inside the selection would then count as an operator's although the selection is still on the screen, and the marks and the edit range can be in different coordinates once lines move. ## Proof - `tests/integration/selection_visual_edit_spec.lua` has eight new real-Neovim cases: a mapping edits another line and presses Esc, appends lines and presses Esc, edits twice and presses Esc, writes the file and presses Esc, edits and then `d` (nothing is sent after it), an operator followed by the next selection in one typeahead, an autocmd edit at a mode change with `ve<Esc>`, and a queued check that runs after visual mode ended and before the flush (a user `ModeChanged` handler for `*:n` that calls `vim.wait(0)`, defined before the plugin starts, and a mapping that edits and presses Esc). On `main`'s `selection.lua` five of them fail on Neovim 0.8.0 and 0.12.3 (the first three, the autocmd case and the new one), and the rest are guards. The spec passes 20 of 20 on 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3. The case for a key that arrives during a callback is a replay only: `vim.wait` gives the callback's key a main-loop turn first, so the check cannot lose the race in that spec. - `tests/selection_test.lua` has eleven new cases (the mock gets `vim.on_key` and one `nvim_create_namespace` id for each name, a new one for the empty name, as Neovim does): the key comes before the schedule, a check that runs after visual mode ended and before the flush judges nothing again, several edits are judged together, the edit of a mapping is not the operator that comes next, a stale check does not clear the listener of the next selection, the schedule clears the listener, several edits keep one listener, a stale listener clears itself, an operator's listener waits for a key, and (the last two) a detached listener counts as an operator on the visual entry and the detach of another buffer does not. I changed `selection.lua` in 14 ways, one at a time, and counted the failures in `tests/selection_test.lua` (158 cases): no key listener (9), a listener that only clears (4), one decrement for each check (1), never consumed (6), always consumed (6), no schedule (6), no `clear_visual_edit_keys()` in the key listener (2), no `clear_visual_edit_keys()` in `check_visual_edits` (1), a `clear_visual_edit_keys` that does nothing, which removes both (4), a namespace for each edit (3), no stale-entry guard (1), no `unchecked_edits == 0` guard (1), and no `entry.consumed = true` in `on_detach` (1). 13 are killed. One survives and I think it is equivalent, but I did not prove it: the key listener checks `M.state.visual_entry` instead of the entry it was set for. The listener always belongs to the last noted entry, and a different current entry has no unchecked edit, so the zero guard returns. The zero guard itself is not equivalent. A `ModeChanged` handler that runs before the plugin's and calls `vim.wait(0)` runs the queued check after visual mode ended and before the flush. Without the guard that check judges the edit a second time, takes it for an operator's, and Claude gets the cursor. The new unit case and the new integration case kill it (the integration case on Neovim 0.8.0 and 0.12.3). - `verify-selection-tracking` (merged in coder#477): `check.sh` passes (129,986 distinct states) and so does `verify-diff-lifecycle` (89,205), with both locks re-recorded: `selection.lua` changed, the selection skill has a new covered block (`check_visual_edits`), and the diff model reads no block or site of that file. All 16 replays print `OK` on Neovim 0.8.0 and 0.12.3 at the default delay and with `DELAY_MS=50`. The three that replay these bugs print `BUG` on `main`. - The skill is updated for this fix: `VisualCheckSparesPluginEdit` now reads `check_visual_edits` and both triggers in `note_visual_edit`, so removing the schedule, the key listener, the mode test or the `consumed` mark reads `FALSE` and nothing else (checked with five mutants of `selection.lua`; the model then breaks `ReleaseSent`). `ListensToSelectionBuffer` reads `check_soon()` in the body of `on_lines` (in the branch that holds the selection) and in the body of `on_reload`, each body on its own. So moving the call into the `elseif not entry` branch, removing it from `on_lines` or `on_reload`, or moving it from `on_reload` into `on_detach` reads `FALSE` and nothing else (five mutants). All 27 facts read `TRUE` on this tree. On the code before coder#524 exactly four facts read `FALSE` (checked at the previous push), and the old form of `on_lines` still reads `TRUE` for `ListensToSelectionBuffer` after this change. The replay header prints the Neovim version as numbers (it printed a table address on 0.8). - Gates on the final head: the full unit suite (`busted --shuffle`, seed 1794484841) 1748 successes, 0 failures, 28 pending. The integration runner (CI style, a private `HOME`, normal and `odd tmp 50%` `TMPDIR`): 535 tests in both runs on 0.12.3 and 398 in both runs on v0.8.0, 0 failures, and the real cache stays untouched. `scripts/tla/test-check-lib.sh` 44 of 44. The spec passes 20 of 20 on all five Neovim versions, `selection_test.lua` 158 of 158, `check.sh` of both skills passes, `luacheck` 0 warnings in 185 files, `treefmt --ci` 0 changes in 427 files, and `--hash-only` matches for all four `verify-*` skills (no re-record was needed after the merge of `main`). - `selection_held_spec.lua` is flaky under load on `main` (here 7 of 72 runs, on `origin/main` 14 of 72). This PR does not touch it. coder#559 fixes it with condition waits and shows the cause with traces. ## Notes for the reviewer - coder#553 is merged. This branch merges `main` and keeps the helpers of that PR at the outer scope of the spec, because the mapping cases use them. coder#559 also edits `selection_visual_edit_spec.lua` (`wait_for_cursor` waits 400 ms, and one new case at the end of the operator block), so whichever of the two lands second needs a small merge in that file. - Neovim 0.8 and 0.9 still need the scheduled check for a plugin edit whose callback ends before any key (their `on_lines` runs with visual mode off during the API call). The key listener adds the keys that come first. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 added 3 commits November 10, 2026 18:16

Merge origin/main into skills/verify-selection-tracking

2d9bf12

ThomasK33 mentioned this pull request Nov 10, 2026

fix(selection): end a held selection when its file changes while you are in the Claude terminal #481

Merged

ThomasK33 added 5 commits November 10, 2026 20:19

Merge origin/main into skills/verify-selection-tracking

e6f985e

Merge origin/main into skills/verify-selection-tracking

6a27d9d

Merge origin/main into skills/verify-selection-tracking

f91391f

chatgpt-codex-connector Bot reviewed Nov 11, 2026

View reviewed changes

Comment thread .agents/skills/verify-selection-tracking/model/SelectionTracking.tla Resolved

Comment thread .agents/skills/verify-selection-tracking/replays/run.sh Resolved

Comment thread .agents/skills/verify-selection-tracking/replays/run.sh Resolved

ThomasK33 added 9 commits November 11, 2026 07:22

Merge origin/main into skills/verify-selection-tracking

47b160d

Merge origin/main into skills/verify-selection-tracking

613432e

chatgpt-codex-connector Bot reviewed Nov 11, 2026

View reviewed changes

Comment thread .agents/skills/verify-selection-tracking/SKILL.md Resolved

Comment thread .agents/skills/verify-selection-tracking/model/SelectionTracking.tla Resolved

ThomasK33 mentioned this pull request Nov 11, 2026

fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #524

Merged

ThomasK33 added 2 commits November 12, 2026 01:50

Merge remote-tracking branch 'origin/main' into skills/verify-selecti…

ea0193b

…on-tracking

ThomasK33 added 4 commits November 12, 2026 02:31

docs(skills): name the same-typeahead edit as a known bug with a fail…

92c7936

…ing replay, and give the reason for the one-bit changedtick

ThomasK33 mentioned this pull request Nov 12, 2026

fix(selection): check a plugin's edit in visual mode at the next key #540

Merged

ThomasK33 added 2 commits November 12, 2026 03:52

Merge remote-tracking branch 'origin/main' into skills/verify-selecti…

bc7654d

…on-tracking

docs(skills): cite the fix PR for the same-typeahead bug and the meas…

f974ee0

…ured --mutants time

ThomasK33 added 3 commits November 12, 2026 07:00

Merge remote-tracking branch 'origin/main' into skills/verify-selecti…

d22515a

…on-tracking

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

Merged via the queue into main with commit bd90803 Nov 12, 2026
8 checks passed

ThomasK33 deleted the skills/verify-selection-tracking branch November 12, 2026 08:37

Conversation

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

Uh oh!

Status

What this adds

The ten rules, as plain sentences

Bugs this model found

What changed from the model that found those bugs

Proof

Run it

Review record

Notes for the reviewer

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

ThomasK33 commented Nov 10, 2026

Uh oh!

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

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 10, 2026

🛡️ Codex Security Review

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 11, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

ThomasK33 commented Nov 11, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ Codex Security Review

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ThomasK33 commented Nov 10, 2026 •

edited

Loading

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

edited

Loading