fix(selection): check a plugin's edit in visual mode at the next key by ThomasK33 · Pull Request #540 · coder/claudecode.nvim

ThomasK33 · 2026-11-12T03:52:15Z

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

A mapping that edits and presses Esc in one key sequence, for example <Cmd>lua edit_other_line()<CR><Esc>.
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.
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 feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking #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 fix(selection): keep the release of a visual selection after a plugin edits another line or writes the file #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. test(selection): wait for the plugin to settle in selection_held_spec #559 fixes it with condition waits and shows the cause with traces.

Notes for the reviewer

test(selection): count only what is sent after the operator in two visual-edit tests #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. test(selection): wait for the plugin to settle in selection_held_spec #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 • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh

… not only after the schedule The flush on Esc skips a selection that has an edit nobody checked (an operator's edit comes before the flush that it triggers). note_visual_edit checked it in vim.schedule, which runs after the command that made the edit returns. A mapping such as <Cmd>lua edit()<CR><Esc> runs the Esc before that, so the flush took a plugin's edit of another line for an operator's and Claude got the cursor, not the selection. vim.on_key sees the Esc while visual mode is still on (checked on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3), so the same check runs there too. Whichever comes first judges every edit that is waiting, and the second finds nothing.

… visual mode

…ual-edit key check Only the file hash of selection.lua changed. The model reads no block or site of that file.

…peahead-edit

ThomasK33 · 2026-11-12T03:52:22Z

@codex review

ThomasK33 · 2026-11-12T03:52:24Z

@codex security review

chatgpt-codex-connector · 2026-11-12T03:52:43Z

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-12T12:18:02.363396Z	`d7d94d7`	Manual request
🔒 Security Review	✅ Completed 2026-11-12T12:19:30.349419Z	`d7d94d7`	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-12T03:55:07Z

🛡️ Codex Security Review

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

Reviewed commit: 0341a9e000

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-12T03:55:23Z

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

Reviewed commit: 0341a9e000

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

…at edits share one listener Removing clear_visual_edit_keys() from check_visual_edits passed every test: the listener then lives until the next key, where it finds nothing to check. The unit mock now returns one namespace id for each name and a new one for the empty name, as Neovim does, so a namespace for each edit (a listener that nothing clears) fails too. README and the comment say that the listener can live until the next key.

…f the next selection

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

…o timing-exposed visual-edit tests Both tests press ve, wait 20 ms, edit another line or :write, wait 20 ms, and press d. When anything delays that past the 100 ms debounce (a slow :write on a busy host, a stalled loop), the debounce sends the selection that you are still making, with the mode still visual. That send is right, and the plugin sends the cursor as soon as d runs. sent_no_selection counted every message, so the test failed with {false, 'alpha'} on CI. It now looks at the messages after the operator, and checks that a selection sent before it is the selection you made.

… range of an early selection After an operator the plugin sends the cursor once its flush or the debounce has run, and get_latest_selection() is nil until then. A host that stalls the loop past the fixed 400 ms wait made the five operator tests fail with 'attempt to index a nil value' (the stall repro fails them all on main). They wait until the plugin holds a cursor now, then give the debounce and the demotion time to run. The selection that the debounce may send before the operator is checked for its range too, not only its text.

…-edit-flake

…rator is a cursor When a slow write or plugin edit lets the debounce send the selection before the operator, the tests passed even if the plugin only forgot the selection in its own state and never told Claude. The five operator tests now also assert that the last message sent is a cursor.

…n the visual entry Removing entry.consumed = true from on_detach turned no test red.

…peahead-edit

…ener in VisualCheckSparesPluginEdit, tighten ListensToSelectionBuffer The three replays for an edit whose check had not run when the next key arrived print OK now. VisualCheckSparesPluginEdit reads check_visual_edits and both triggers in note_visual_edit (vim.schedule and vim.on_key), so removing either shows. ListensToSelectionBuffer needs check_soon() in the holding branch of on_lines (or after the old detach), so moving it into the elseif branch reads FALSE. The replay header prints the Neovim version as a number string (it printed a table address on 0.8).

selection.lua changed: note_visual_edit now sets the vim.on_key listener, and check_visual_edits is new. The selection skill has a new covered block (check_visual_edits) that VisualCheckSparesPluginEdit reads. The diff model reads no block or site of selection.lua.

…peahead-edit

…' into fix/selection-same-typeahead-edit #553 fixes two timing bugs of the operator tests of this spec. Its helpers move to the outer scope of the spec, where the cases of this branch use them, and the new mapping case waits for the cursor and checks the selections sent before the operator, as #553 does. The spec has one more case: an autocmd that edits as visual mode starts.

ThomasK33 · 2026-11-12T09:46:39Z

@codex review

ThomasK33 · 2026-11-12T09:46:41Z

@codex security review

chatgpt-codex-connector · 2026-11-12T09:50:29Z

🛡️ Codex Security Review

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

Reviewed commit: 24cce3d878

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-12T09:53:31Z

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

Reviewed commit: 24cce3d878

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

…peahead-edit # Conflicts: # tests/integration/selection_visual_edit_spec.lua

A ModeChanged handler that runs before the plugin's and turns the main loop (vim.wait) runs the queued check after visual mode ended and before the flush. The key listener has already checked the edit, so that check must find nothing to judge: without the guard it takes the plugin's edit for an operator's and the flush reports the cursor. A unit test and an integration case cover it.

… which check runs after the flush check.sh read check_soon after on_reload anywhere in watch_selection_buffer, so a check_soon that moved into on_detach still read TRUE. It now reads the bodies of on_lines and on_reload. SKILL.md said the flush on Esc comes after both checks. It comes after the first one: when the key comes first, the schedule runs after the flush and finds nothing to do.

ThomasK33 · 2026-11-12T12:15:44Z

@codex review

ThomasK33 · 2026-11-12T12:15:47Z

@codex security review

chatgpt-codex-connector · 2026-11-12T12:18:00Z

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: d7d94d799f

ℹ️ 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-12T12:19:29Z

🛡️ Codex Security Review

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

Reviewed commit: d7d94d799f

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.

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

…sual-edit tests (coder#553) ## What failed CI run 43167645889 (job `integration-tests (stable)`, PR coder#523, head `3ceb6ecc`) failed `tests/integration/selection_visual_edit_spec.lua:230`, "sends no selection for d after a :write in visual mode", with `{false, 'alpha'}`. ## Cause: a timing bug in the test, not in the plugin The test presses `ve`, waits 20 ms, runs `:write`, waits 20 ms and presses `d`. It then asserts that Claude was never sent a non-empty selection. That holds only while `d` comes within the 100 ms debounce of `ve`. When anything delays the keys past it (a slow `:write` on a busy host, a stalled loop), the debounce sends the selection that you are still making, with the mode still visual. That send is right: you did select `alpha`. The plugin then sends the cursor (an empty selection) the moment `d` runs. `sent_no_selection` counted every message, so it also counted the right one. I traced it with time stamps, on Neovim 0.12.3 and 0.8.0. In every failing run the sequence is the same: ``` 0 ms press ve 20 ms write start 167 ms write end 167 ms SENT text="alpha" empty=false mode=v <- the debounce, before d 247 ms press d 297 ms SENT text="" empty=true mode=n <- the cursor, right after d ``` A phantom after `d` would carry ` beta` (the text at the old marks) and a mode other than `v`. None of the 30 traces has one. A deterministic repro makes `:write` block for 150 ms with a `BufWritePost` autocmd: the same sequence, the same failure, and the plugin ends with the cursor held and ` beta gamma` on line 1. The sibling test "sends no selection for d after a plugin edited another line in visual mode" has the same shape and failed too (`wait(20)` stalled). The `ved`, `vec` and `Vj>` tests press all their keys in one `press`, so no timer can fire between them. ## The fix Round 1 (`43a12838`): `sent_no_selection(from)` looks only at the messages after number `from`. The two tests record `#sent` before they press `d`, and assert that a selection sent before the operator is the one the user made. With the flush made to never skip (`if false and entry ...`), the five operator tests fail on both versions, these two included. Round 2 (the Opus verifier's two findings): - **F1, a second flake in the same tests (also on `main`).** After an operator the plugin sends the cursor when its flush or the debounce has run, and `get_latest_selection()` is `nil` until then. A host that stalls the loop past the fixed `wait(400)` made the test fail with `attempt to index a nil value`. The five operator tests (`ved`, `vec`, `Vj>`, and the plugin-edit and `:write` tests) now call `wait_for_cursor()`: `vim.wait` with a condition (the plugin holds an empty selection) and a 5 s limit, then `wait(200)` so that a selection sent late by the debounce would still show. The release tests keep `wait(400)`: the flush on Esc sends the selection before `press` returns, so `get_latest_selection()` is never `nil` there. - **F2, the early-selection check compared only the text.** `assert_is_the_selection` checks the text and the range (`0:0` to `0:5`) of every selection sent before the operator. Round 3 (Codex P2): when the debounce sends `alpha` before `d`, the tests passed even if the plugin only forgot the selection locally and never sent the cursor. Each of the five operator tests now also asserts that the last `selection_changed` sent is a cursor. A mutant whose flush sets `latest_selection` to the cursor without sending it passes the round-2 spec 12 of 12, and fails this spec's plugin-edit and `:write` tests under the 150 ms stall on both versions (a verifier reran it: 2 of 12 fail, those two). Without a stall, `tests/selection_test.lua` already catches that mutant. ## Proof Deterministic stalls, on Neovim 0.12.3 and 0.8.0 (generated copies of the spec, not part of the PR): | Stall | Old spec (`main`) | Round-1 spec | This spec | | --- | --- | --- | --- | | 150 ms between the selection and `d` (`:write` and plugin-edit tests) | 2 of 12 fail (`{false,'alpha'}`) | passes | 12 of 12 pass | | loop blocked 450 ms right after the operator (the five operator tests) | 5 of 12 fail (`attempt to index a nil value`) | 5 of 12 fail | 12 of 12 pass | | no stall | 12 of 12 | 12 of 12 | 12 of 12 | Wrong range, right text (the in-visual selection sent with its end line moved by 5), with the 150 ms stall: the round-1 spec passes 12 of 12 on both versions, and this spec fails the plugin-edit and `:write` tests (both on 0.8.0 and in 3 of 4 runs on 0.12.3, one run failed only the `:write` test). Same-window load (24 runners in parallel and 8 `dd conv=fsync` loops, or 40 runners with 12 disk loops and 16 CPU burners): | Window | Old or round-1 spec: runs that failed | This spec | | --- | --- | --- | | round 1, 0.12.3, old spec | 25 of 72 (`{false,'alpha'}`) | 0 of 72 (round-1 spec) | | round 1, 0.8.0, old spec | 4 of 72 | 0 of 72 (round-1 spec) | | round 2, 0.12.3, 40 runners, round-1 spec | 24 of 80 (all 24 `attempt to index a nil value`: `Vj>` 15, `vec` 7, `:write` 1, `ved` 1) | 0 of 80 (round-2 spec) | | this head (verifier rerun, load up to about 114) | not reproduced: the round-1 spec also passed 0 of 80 | 0 of 80 on 0.12.3, 0 of 40 on 0.8.0 | A window with lower load had no failure for either spec (0 of 72 each), so the deterministic stalls above are the proof and the load windows the check. Other gates: the spec passes 12 of 12 on both versions on an idle host. The CI-style integration runner (private `HOME`, normal and `odd tmp 50%` `TMPDIR`) passes with 417 tests per run on 0.12.3 and 309 per run on v0.8.0, and leaves the real cache untouched. `luacheck` shows 0 warnings in 181 files and `treefmt --ci` 0 changes. ## Notes for the reviewer coder#540 moves `sent_no_selection` to the outer scope of this spec and adds cases that use it. It resolves the conflict when it merges `main`. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…coder#559) ## Result `selection_held_spec.lua` failed in 24 of 144 runs under load. With this change it failed in 0 of 144 runs, on the same tree, in the same load windows. The load was 16 spec runs at the same time, 8 disk writers (`dd conv=fsync` loops), Neovim 0.12.3, three rounds that alternate the old and the new spec (round 1: 18 of 48 against 0 of 48, round 2: 1 against 0, round 3: 5 against 0). Without load the spec takes 9 s instead of 23 s, because it no longer sleeps. This PR is only test code (two spec files). It does not change the plugin. ## Cause Every wait in the spec was a fixed `vim.wait(N)`. A wait ends at its deadline. When the main loop stalls for 230 to 390 ms (a loaded disk or CPU), the wait can end in the loop iteration that fires the timers. The `vim.schedule_wrap` callbacks of those timers have not run yet. And a late debounce arms the demotion timer too late for the deadline. The next step then reads a plugin that is not done. I traced this with a copy of the spec that logs the plugin's calls, adds a 5 ms heartbeat timer (it reports every stall of the loop), and dumps the log when a test fails. Each failure below comes from a wait that ended too early. The last row also exposes a plugin gap (see "Found while tracing"). The traces are in the details below. | Old test | What failed | What the trace shows | |---|---|---| | keeps one listener on the file through reloads (after `enew`) | `selection.isEmpty` was `false` | the loop stalled 334 ms, the wait ended in the iteration that fired the debounce, and `update_selection` sent the empty cursor 0 ms after the assertion | | ends the selection without an error when the buffer you visited is wiped (both kinds) | `selection.isEmpty` was `false` | a 270 ms or 389 ms stall, the debounce ran late and armed the 50 ms demotion, and the wait ended before it fired | | does not overflow the stack when the buffer of the held selection is taken for the Claude terminal | a `selection_changed` for `term://x//1:claude` was sent | the demotion timer fired in the stall, and its callback ran after the test had renamed the buffer and edited it (I reproduced this with an injected stall) | | keeps the selection when the Claude terminal first opens (delay 50) | held text was `""`, not `"alpha"` | the stall ended the wait with the demotion pending, the terminal opened (2.7 s on the loaded disk), and the demotion fired while the terminal was the current buffer | The old spec failed these in 24 of 144 runs: 18 times the overflow test, 7 times the first-opens test, 2 times a wiped-buffer test (27 failed tests in 24 runs). The listener test failed in other runs: 12 of 60, 5 of 60 and 15 of 48 traced runs, and 2 of 36 untraced runs. <details> <summary>Traces (times in ms, from a traced copy of the old spec)</summary> Listener test, a stall straddles the end of `wait(300)`: ``` 28502 on_cursor_moved(buf=24) :enew arms the 100 ms debounce 28853 STALL: loop did not run for 334 ms (28519..28853) 28853 shadow fast timer (100 ms from 28502) fired 28853 wait(300) took 349 ms 28853 cycle 1: isEmpty after wait(300) = false <- the assertion point 28853 shadow scheduled timer (100 ms from 28502) ran 28853 update_selection(buf=24) 28853 send_selection_update text= file= <- the cursor of the new buffer 28853 isEmpty became true 0 ms after the assertion point ``` Wiped-buffer test (`nvim_buf_delete`), the debounce runs late and its demotion misses the deadline: ``` 32138 on_cursor_moved(buf=35) the file buffer is current again, debounce armed 32488 STALL: loop did not run for 270 ms (32218..32488) 32493 update_selection(buf=35) arms the 50 ms demotion 32542 wait(400) took 404 ms the demotion would fire at about 32543 ``` Overflow test. I reproduced it by putting a 220 ms sleep between two loop iterations of the wait after Esc (the natural failure has the same assertion message: `selection_changed`, `filePath = 'term://x//1:claude'`, `text = ''`): ``` 12210 update_selection the debounce read the release, arms the demotion 12226 STALL injected between two loop iterations: the process sleeps 220 ms 12452 STALL: loop did not run for 226 ms (12226..12452) 12452 wait(300) took 347 ms 12452 handle_selection_demotion(buf=16) runs in the NEXT wait, after rename + edit 12452 send_selection_update text= file=term://x//1:claude stack: selection.lua:1170 send_selection_update < :711 handle_selection_demotion < :622 timer callback ``` First-opens test (delay 50): ``` 296 update_selection arms the 50 ms demotion 547 STALL: loop did not run for 231 ms (316..547) 547 wait(300) took 351 ms the wait ends with the demotion pending 748 on_cursor_moved(demotion_timer=true, buf=2) the terminal opens 3306 STALL: loop did not run for 2759 ms (547..3306) 3306 handle_selection_demotion(buf=2) fires while the terminal is the current buffer 3721 send_selection_update(buf=1) text= after you return: the cursor replaces the selection ``` </details> ## What changed `tests/integration/selection_held_spec.lua`: - `settle(keep_demotion)` waits until the plugin has no debounce timer and no demotion timer pending, and until every `vim.schedule` callback queued before the call has run (it queues a flag and waits for the flag, and the queue is first in, first out). Every `wait(N)` that waited for the plugin is now `settle()`. - `select_and_release(keep_demotion)` settles after `ve` (the debounce reads the selection) and after Esc (the debounce reads the release, and the demotion runs). The two specs that need a long demotion still pending (`visual_demotion_delay_ms` of 1000) pass `keep_demotion`, and the helper asserts that the demotion is pending, so a stall cannot silently end that premise. - The one `wait(20)` stays, with its comment: the popup is closed inside the debounce on purpose. `tests/integration/selection_visual_edit_spec.lua` (two follow-ups to coder#553, F1 and F2): - F1: `wait_for_cursor` waits 400 ms after the cursor (it was 200) and then drains the queued callbacks, so a phantom selection sent up to 400 ms after the operator shows again. - F2: a new case, "sends a cursor for d after the debounce sent the selection in visual mode". It waits until the debounce has sent the selection, before `d`. The two cases above it press `d` within the debounce, so their early-selection checks usually have nothing to look at. This one checks the text and the range of the early selection and that the last message is a cursor, on every run. ## The tests still test the same things One thing was lost in the first version and is back in round 2. The three tests that expect nothing to be sent (overflow, pending demotion, sends nothing in another terminal) lost the late-send window of their old fixed waits, because `settle()` returns as soon as no timer is pending. The verifier's mutant sends the cursor of the terminal buffer 200 ms late with `vim.defer_fn`. It failed 3 tests of the old spec and none of the first version of the new spec. Each of the three tests now calls `wait_for_late_send()`: it waits 300 ms after `settle()` and then settles again, because a timer that fires in the last iteration of that wait has not run its callback yet (Codex found this in round 2). The mutant fails the same 3 tests again, and the unchanged plugin passes all 14. I changed `selection.lua` ten ways (one at a time, in a scratch copy) and ran the old and the new spec. None of these ten is a late send. The set of failing tests is the same for nine of them, and the new spec also kills one that the old spec did not: | Mutant of `selection.lua` | Old spec fails | New spec fails | |---|---|---| | overflow: the terminal branch calls `update_selection` | 3 | 3 (same tests) | | no demotion cancel in the terminal branch | 1 | 1 | | `from_terminal` ignores the terminal name | 1 | 1 | | no `check_soon` in `on_reload` | 1 | 1 | | no `check_soon` in `on_lines` | 6 | 6 | | the listener forgets its buffer on reload | 1 | 1 | | the demotion ignores an unmoved cursor | 13 | 13 | | no `caf.left` mark | 2 | 2 | | the terminal update keeps the pending demotion | 0 | 1 (first opens, delay 1000) | | no re-watch in `on_detach` | 0 | 0 (survives both, as before) | For the coder#553 follow-ups, on coder#553's tree: removing the flush guard fails 5 tests of the old spec and 6 of the new one. A range off by one at the selection end (the text stays right) survives the old spec and fails the new F2 case. A phantom selection sent 350 ms after the operator fails 4 of the 12 tests of coder#553's spec with `wait(200)` in every run of the independent verifier (I saw 0 failures in one run, so the old margin depends on timing), and 6 tests with `wait(400)`. ## Found while tracing: a plugin bug that this PR does not fix At the default `visual_demotion_delay_ms` of 50, Claude loses a held selection when you enter the Claude terminal 100 to 150 ms after Esc and then come back. The demotion timer fires while the terminal is the current buffer, and Condition 1 of `handle_selection_demotion` sets `last_active_visual_selection = nil`. When you return, `update_selection` finds no recent visual exit and sends the cursor. A probe with no stall shows it: release `alpha`, wait until the debounce arms the demotion, open the terminal at once, wait for the demotion, `wincmd p`. At delay 50 the held text after the return is `""`. At delay 200 it is `"alpha"` (the terminal's own debounce cancels the demotion). Removing the `last_active_visual_selection = nil` block in Condition 1 keeps `"alpha"` at both delays, and this spec stays 14 of 14. That change touches a file that `verify-selection-tracking` covers, so it is its own PR: coder#562. The old test only failed because a stall moved the demotion into that window. ## Gates - `selection_held_spec.lua` 14 of 14 and `selection_visual_edit_spec.lua` 13 of 13 on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3 before the coder#540 merge, and 21 of 21 on 0.8.0 and 0.12.3 after it (a verifier rerun). Under the load of the first table (16 runs at once, 8 disk writers) the spec with the added waits failed 0 of 48 runs. - The integration runner as CI runs it (a private `HOME`, normal and `odd tmp 50%` `TMPDIR`): 0.12.3 528 of 528 in both runs, v0.8.0 391 of 391 in both runs, 0 failures. - coder#553's spec under the same load, with F1 and F2: 0 of 96 runs failed, and 0 of 96 for coder#553's spec alone. - `luacheck` 0 warnings, `treefmt --ci` 0 changes. No unit test changes, so I did not run the unit suite. - I did not run the load comparison on Neovim 0.8.0. The comparison above is 0.12.3 only. ## Notes for the reviewer - coder#540 is merged. This branch merged `main` without a conflict, and F1 and F2 sit on the helpers that coder#540 moved to the outer scope of `selection_visual_edit_spec.lua`. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…he flush (coder#565) ## What changes One sentence of `.agents/skills/verify-selection-tracking/SKILL.md` (the bullet about edits in visual mode that the model leaves out). It said that when the key comes first, the schedule that checks the edit "runs later, after the flush". That is the usual order, but not the only one. A `ModeChanged` handler that runs before the plugin's and turns the main loop (`vim.wait(0)`, for example) runs the queued check earlier: after Neovim ended visual mode and before the flush. The key listener has already checked the edit at the key, so `check_visual_edits` finds nothing to judge. That is the `unchecked_edits == 0` guard, which coder#540 pins with a unit test and an integration case. The second check finds nothing to do in both orders. The sentence now says both orders and why the result is the same. ## Evidence The independent verifier of coder#540 found the gap (round c, evidence `trail/evidence/540c`). Its probe `k_probe.lua` runs a handler that calls `vim.wait` in `ModeChanged` (`*:n`, and `v:*`): with the guard (the head and mutant K), Claude holds `alpha` in 28 of 28 runs; without it (mutant H) in 10 of 14, and with main's code in 8 of 14.8.0 and 0.12.3. Without the guard it holds the cursor. I read the other places that describe the order (the replay headers, `lua/claudecode/README.md`, the comment in `note_visual_edit`). The comment in `note_visual_edit` (`selection.lua:215`) says the mapping "reaches the flush before the schedule", which is the same claim; the guard keeps the result right, and a later PR corrects that comment. ## Gates - Docs only: no `lua/` file and no covered block changes, so no lock needs a re-record. `--hash-only` matches for all four `verify-*` skills. - `treefmt --ci`: 427 files, 0 changes. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

…e terminal (coder#562) ## What a user sees You select text and press Esc. Within the next 100 to 150 ms you enter the Claude terminal (a toggle mapping, or `:ClaudeCode` that opens it). You come back to the file and the cursor has not moved. Claude holds the cursor and not your selection. A slower switch, or a terminal that Neovim already knows, keeps the selection. With this change Claude keeps it in both cases. I found this while tracing the `selection_held_spec` flake (coder#559): a stall of the main loop moved the demotion into that window, and the plugin did what a person can also trigger. ## Cause At the default `visual_demotion_delay_ms` of 50, the debounce (100 ms) reads the release and arms the demotion timer, and the timer fires 50 ms later. When you enter a terminal that the plugin already knows, `reconcile_held_selection` cancels the demotion at `BufEnter`. A new terminal has no name and is not registered at `BufEnter`, so nothing cancels it, and the demotion fires while the terminal is the current buffer, before the debounce of that `BufEnter` can cancel it. Condition 1 of `handle_selection_demotion` handled that case. It returned, but first it set `last_active_visual_selection = nil`. When you came back, `update_selection` found no recent visual exit, took the "genuinely in normal mode" branch and sent the cursor. Why Condition 1 cleared it: `git log -L` on the block shows one commit, f1cad48 (May 2025, the commit that added `visual_demotion_delay_ms`). Its comment says the selection is preserved and the "pending" status of `last_active_visual_selection` is resolved. That was written before coder#246. At that commit Condition 3 demoted without the cursor-unmoved test, and a return to the file reported the cursor. coder#246 (coder#267, `0b245051`) added the test and made Condition 3 leave the record intact, so that a later cursor move re-arms the demotion. Condition 1 was the one branch that still cleared it. ARCHITECTURE.md already said the timer "does nothing in the Claude terminal", and the model had a step for Condition 1 and a `holdLoose` flag that allowed either outcome on the return (SKILL.md lists it as a case where the model allows both). ## The fix `lua/claudecode/selection.lua`: Condition 1 is now `if M.is_claude_terminal_buffer(current_buf) then return end`. The demotion does nothing in a Claude terminal and leaves the records alone, so the return keeps the selection while the cursor stands where you released it, as it does when you never left. It uses `is_claude_terminal_buffer`, the check that `update_selection` and the flush already use. Before, Condition 1 asked only for the registered terminal. For a terminal that only its name marks (`terminal.provider = "none"` with a `:terminal ... claude` buffer), the demotion fell through to the last block of the function, which cleared the same records, so that user lost the selection the same way. SKILL.md described that as "clears the held-state records and sends nothing". The narrow change (only the registered terminal) leaves that case broken, and the new name-only cases fail with it. ## Each case that Condition 1 served still behaves | Case | Result | Evidence | |---|---|---| | The demotion fires in the registered terminal: it sends nothing and Claude still holds the selection there | same as before | unit tests assert `last_broadcast == nil`, the integration spec asserts `alpha` in the terminal | | The "pending" status stays: the return arms a new demotion, which returns at Condition 3 while the cursor is unmoved | no loop, no cursor sent | unit tests call `settle()` after the return | | You come back and the cursor has not moved | Claude keeps the selection (was: the cursor) | new unit tests, new spec (delay 50) | | You come back and move the cursor | Claude gets the cursor at `CursorMoved` | new unit test (it fails on `main` earlier, at the assertion that the selection was kept) | | The terminal was known at `BufEnter`: the demotion is cancelled there | same as before | existing unit test "keeps the selection when its demotion is armed just before you enter the Claude terminal" | | Delay 200: the terminal's own debounce cancels the demotion first | keeps the selection | new spec (delay 200) | | A terminal that only its name marks (no provider) | keeps the selection (was: the cursor) | new unit test, new spec | | The text of the held selection changes while you are in the terminal | the cursor is reported, as before | the existing unit tests of `demote_if_selection_text_changed` pass | | You go to another file buffer, not a terminal | unchanged (Condition 3 or the last block, which still clears) | existing unit tests pass | ## Proof, test first - `tests/integration/selection_demotion_in_terminal_spec.lua` (new, 3 cases): release `alpha`, arm the demotion, open a terminal, let the demotion fire there, come back, and check that Claude holds `alpha`. It fails on `main`'s `selection.lua` for delay 50 with a registered terminal and for the name-only terminal (2 of 3, on Neovim 0.8.0 and 0.12.3). Delay 200 passes on both, because the debounce cancels the demotion. With the fix it passes 3 of 3 on 0.8.0, 0.9.5, 0.10.4, 0.11.4 and 0.12.3. It arms the demotion by calling what the debounce timer calls (`update_selection`), so that the demotion is pending when the terminal opens and a stall cannot end it first. - `tests/selection_test.lua` (3 new cases, 161 in the file on the final head): the new terminal, the name-only terminal, and the cursor move after the return. All 3 fail on `main`'s `selection.lua`. With only the registered terminal in Condition 1 (the narrow change), the name-only case fails and nothing else does. - Model: `holdLoose` is gone from `SelectionTracking.tla`, so `HeldUntilMoved` now applies to the return from the terminal. A new fact, `DemotionIgnoresTerminal`, reads the whole body of Condition 1 (the `if` and one `return`, nothing else), and `Demote` uses `clearVis` when it is `FALSE`. On this tree `check.sh` passes (95,938 distinct states, 129,986 before: the either-outcome branch is gone). With the old clear put back, `DemotionIgnoresTerminal` reads `FALSE` and `check.sh` fails with `main: BROKEN: HeldUntilMoved`. - `check.sh --mutants` on the merged tree (head `7ba852fa5e`): exit 0 in 3,774 s, 27 rows (26 before, one for the new fact), "every guard is caught". The new fact's row reads `DemotionIgnoresTerminal=FALSE caught by: HeldUntilMoved HeldInTerminal`. - Both locks are re-recorded (`verify-selection-tracking`, and `verify-diff-lifecycle` for the file hash of `selection.lua`: the diff model reads no block or site of it). `--hash-only` matches for all four `verify-*` skills. ## Gates - Full unit suite (`busted --shuffle`, seed 1794487328, before the last test was added): 1739 successes, 0 failures, 29 pending. `selection_test.lua` alone 161 of 161 on the final head. A verifier reran the full suite on the head (same seed): 1770 successes, 0 failures, 29 pending. - The integration runner (CI style, a private `HOME`, normal and `odd tmp 50%` `TMPDIR`): 530 tests in both runs on 0.12.3 and 393 in both runs on v0.8.0, 0 failures. - `selection_held_spec.lua` 14 of 14 and the new spec 3 of 3 on all five Neovim versions, on the final head. - `luacheck` 0 warnings in 186 files, `treefmt --ci` 0 changes, `shfmt` and `shellcheck` clean on `check.sh`. ## Notes for the reviewer - coder#540 is merged. This branch merged `main` after it. Only the two `covered.lock` files conflicted, and I re-recorded both (`--hash-only` matches for all four `verify-*` skills). The skill checks pass on the merged tree: `check.sh` 95,938 states for the selection skill, 89,205 (and 5,269 live) for the diff skill, 16 of 16 replays on Neovim 0.8.0 and 0.12.3, `selection_test.lua` 161 of 161. - The test-only PR coder#559 fixes the flaky waits in `selection_held_spec.lua`. This PR does not touch that file, so the two do not conflict. - A demotion in a terminal still lets the debounce of the terminal run later: `update_selection` returns in the terminal and only checks the held text, as before. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_

ThomasK33 added 4 commits November 12, 2026 02:45

docs(selection): say that the next key also checks a plugin's edit in…

4bb67f9

… visual mode

chore(skills): re-record the verify-diff-lifecycle lock after the vis…

621374a

…ual-edit key check Only the file hash of selection.lua changed. The model reads no block or site of that file.

Merge remote-tracking branch 'origin/main' into fix/selection-same-ty…

0341a9e

…peahead-edit

ThomasK33 mentioned this pull request Nov 12, 2026

feat(skills): add verify-selection-tracking, a TLA+ model of selection tracking #477

Merged

ThomasK33 added 2 commits November 12, 2026 05:18

test(selection): pin that a stale check does not clear the listener o…

6286f57

…f the next selection

ThomasK33 mentioned this pull request Nov 12, 2026

test(selection): count only what is sent after the operator in two visual-edit tests #553

Merged

ThomasK33 added 10 commits November 12, 2026 08:09

Merge remote-tracking branch 'origin/main' into test/selection-visual…

b398e1e

…-edit-flake

test(selection): pin that a detached listener counts as an operator o…

b9c0833

…n the visual entry Removing entry.consumed = true from on_detach turned no test red.

Merge remote-tracking branch 'origin/main' into fix/selection-same-ty…

574fa16

…peahead-edit

wip: facts

00bc7b4

Merge remote-tracking branch 'origin/main' into fix/selection-same-ty…

d3e913d

…peahead-edit

Merge remote-tracking branch 'origin/main' into fix/selection-same-ty…

803b24a

…peahead-edit # Conflicts: # tests/integration/selection_visual_edit_spec.lua

ThomasK33 added 2 commits November 12, 2026 11:51

ThomasK33 mentioned this pull request Nov 12, 2026

test(selection): wait for the plugin to settle in selection_held_spec #559

Merged

ThomasK33 mentioned this pull request Nov 12, 2026

fix(selection): keep the selection when the demotion fires in a Claude terminal #562

Merged

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

Merged via the queue into main with commit d123707 Nov 12, 2026
7 checks passed

ThomasK33 deleted the fix/selection-same-typeahead-edit branch November 12, 2026 13:40

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

chore(release): 0.5.0 #444

Open

Conversation

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

Uh oh!

What a user sees

Cause

The fix

Proof

Notes for the reviewer

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

ThomasK33 commented Nov 12, 2026

Uh oh!

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

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Nov 12, 2026

🛡️ 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

🛡️ 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 12, 2026 •

edited

Loading

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

edited

Loading