diff --git a/.agents/skills/verify-selection-tracking/SKILL.md b/.agents/skills/verify-selection-tracking/SKILL.md new file mode 100644 index 000000000..b664c6ee0 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/SKILL.md @@ -0,0 +1,207 @@ +--- +name: verify-selection-tracking +description: Model-check what Claude sees as the user's current selection in claudecode.nvim (TLA+/TLC) against guards read from the current Lua code, and replay paths on headless Neovim. Use after a change to selection tracking (lua/claudecode/selection.lua, its enable/disable calls in lua/claudecode/init.lua, server.broadcast or on_connect in lua/claudecode/server/init.lua, or the getCurrentSelection and getLatestSelection tools), to the debounce or demotion timers, the visual-exit flush, or held-selection behavior (issue #246), and before trusting such a change. +--- + +# Verify selection tracking + +While Claude is connected, `lua/claudecode/selection.lua` pushes the user's selection as a `selection_changed` notification. `getCurrentSelection` and `getLatestSelection` return the same value, `M.state.latest_selection`. Each send sets it first, so this check treats `latest_selection` as what Claude holds. If it is wrong, Claude answers about text the user did not select, about text that is gone, or about the wrong file. When nothing is tracked, `getCurrentSelection` reads the editor itself (#457, #463). The model makes no claim about that answer. + +A selection survives Esc: Claude holds it until the cursor moves or its text changes (issue #246). The plugin keeps that hold in `last_active_visual_selection`, `cursor_at_flush` and `selection_tick`, and ends it from `CursorMoved`, `BufEnter`, `TextChanged`, `ModeChanged`, two one-shot timers, and a listener on the buffer of the held selection (`nvim_buf_attach`: `on_lines`, `on_reload`). + +The check explores every order of keys, mode changes, buffer switches, timer firings and timer callbacks in a small model, with each guard switched on or off to match the code as it is now. The model has no clock, so it covers every `visual_demotion_delay_ms`. + +## Rules + +| Rule | Plain sentence | Harm when broken | +| --------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- | +| `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, and when a plugin edited another line or a `:write` ran while you selected. | A quick selection never reaches Claude (issue #246). | +| `NoPhantomSelection` | Claude only gets text you selected, never the text at the `'<,'>` marks after an operator such as `d` changed it. | Claude gets a selection the user never made. | +| `NoTerminalSelection` | Claude never gets a selection in the Claude terminal buffer. | Claude's own prompt text becomes the context. | +| `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. | The selection the user means to ask about is gone before they type (issue #246). | +| `HeldInTerminal` | Once events settle in the Claude terminal, Claude still holds the selection you released while its text is unchanged. | The selection is gone when the user goes to the terminal to type the question (issue #246). | +| `HeldEndsWhenMoved` | Once events settle in a file, Claude holds a released selection only while the cursor has not moved since you released it. | Claude answers about an old selection after the user moved on. | +| `SameFile` | Once events settle in a file, Claude's selection is in that file. | Claude thinks the user is in another 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. | Claude points at the wrong line or column. | +| `NoDeletedText` | Once events settle, Claude holds no selection text that its buffer no longer has. | Claude answers about text the user deleted. | +| `TimerClosedOnce` | No timer handle is closed twice. | Neovim shows `handle ... is already closing`, a Lua error, while the user moves or types. | + +"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. + +## Run + +```bash +.agents/skills/verify-selection-tracking/check.sh # about 1 min +.agents/skills/verify-selection-tracking/check.sh --keep # same, keeps the TLC configs and output, prints the dir +.agents/skills/verify-selection-tracking/check.sh --mutants # about 1 to 1.5 h (4486 s to 4990 s at a load average of 22 to 31), after you edit the model or a fact +.agents/skills/verify-selection-tracking/check.sh --record # rewrite covered.lock, only after "Update after an intended change" +.agents/skills/verify-selection-tracking/check.sh --hash-only # about 5 s, no TLC: only compares covered.lock with the code +``` + +The shared harness is `scripts/tla/check-lib.sh` (read its header). It pins TLC 1.7.4 by sha256 and downloads it to `~/.cache/claudecode-nvim-tla/` on the first run. It needs bash 4 or newer, Java 11 or newer (`JAVA=/path/to/java` overrides), and `sha256sum` or `shasum`. CI runs every `.agents/skills/verify-*/check.sh`. Run one TLC job at a time on a shared host. + +Exit codes: + +- `0` is PASS. +- `1` means a rule broke. A rule that breaks on a stale tree exits `1`, not `3`. With `--mutants`, `1` also means a guard no rule caught, or a rule that never broke. +- `2` is a tool or script error, or a model whose `TypeOK` breaks. +- `3` is STALE. The covered code changed since the model was last confirmed, so the change is unverified. + +## Does the change touch the verified code? + +Run `check.sh --hash-only`. `covered.lock` records, for each covered file, its hash, the hash of each block the model describes, and each line that reads or writes the selection state, a timer field, or calls a send, with its enclosing top-level statement. Any change to a covered file reads `STALE` (exit 3) and prints `was:`/`now:` lines for the changed file, blocks and sites. + +Covered files and blocks: + +- `lua/claudecode/selection.lua`: `cursor_unmoved_since_flush`, `clear_held_state`, `selection_text_is_there`, `cursor_in_other_buffer`, `demote_if_selection_text_changed`, `holds_selection_of`, `visual_entry_of`, `note_visual_edit`, `watch_selection_buffer`, `record_selection_read`, `reconcile_held_selection`, `M.enable`, `M.disable`, `M._cancel_debounce_timer`, `M._cancel_demotion_timer`, `M._create_autocommands`, `M.on_cursor_moved`, `M.on_mode_changed`, `M.on_text_changed`, `M.debounce_update`, `M.update_selection`, `M.handle_selection_demotion`, `M.get_visual_selection_from_marks`, `M.flush_visual_selection`, `M.has_selection_changed`, `M.send_selection_update`, `M.is_claude_terminal_buffer`, `M.get_latest_selection`. +- `lua/claudecode/init.lua`: `M.start` (calls `selection.enable(M.state.server, visual_demotion_delay_ms)`) and `M.stop` (calls `selection.disable()`, then stops the server). +- `lua/claudecode/server/init.lua`: `M.broadcast` and the `on_connect` callback. +- `lua/claudecode/tools/get_current_selection.lua` and `get_latest_selection.lua`: the `handler`, which starts from `get_latest_selection()`. + +`git log -- .agents/skills/verify-selection-tracking/covered.lock` shows each confirmation. Move it forward, with `--record`, only after you confirm that the model describes the code at the new commit. + +Not covered, so a change there shows nothing: `lua/claudecode/utils.lua` `selection_type` (which modes count as visual, Select mode among them), `valid_utf8` (decides whether the held text is still at its range) and `utf8_sequence_length` (keeps a cursor off the middle of a character), `lua/claudecode/terminal.lua` `get_active_terminal_bufnr` (the second check in `is_claude_terminal_buffer`), and `tools/get_open_editors.lua`, which also reads `get_latest_selection()`. A PASS says the model holds for the guards the facts read, on code that matches the record. It does not review a change. STALE never means "probably fine". + +## Read the result + +`check.sh` prints the code facts first. Each fact is a guard that a regex reads from the source. `TRUE` means the regex found the guard. `FALSE` means the model runs without that guard. + +| Fact | Code it reads (all in `selection.lua`) | +| ----------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `FlushOnVisualExit` | the `ModeChanged` autocmd calls `on_mode_changed`, which calls `M.flush_visual_selection()` when `leaving_visual` | +| `FlushSkipsOperator` | `on_mode_changed` makes `visual_entry` (`bufnr`, `consumed`, `unchecked_edits`) when visual mode starts. The flush returns when `entry.consumed or entry.unchecked_edits > 0` (an operator such as `d` consumed the selection) | +| `FlushSkipsTerminal` | the flush returns when `M.is_claude_terminal_buffer(current_buf)` | +| `FlushRecordsCursor` | the flush sets `M.state.cursor_at_flush` to the buffer and the window cursor | +| `UpdateSkipsTerminal` | `update_selection` cancels the demotion and returns when `M.is_claude_terminal_buffer(current_buf)` | +| `PendingKeepsHeld` | in `update_selection`, while `M.state.demotion_timer` is set: `latest_selection` stays when `cursor_unmoved_since_flush`, else the cursor. That function compares the cursor with `cursor_at_flush` in the same buffer and reads `.left` | +| `ElseClearsHeldState` | `update_selection`'s last branch (no demotion, no held selection here) clears `last_active_visual_selection` and `cursor_at_flush` | +| `DemotionWaitsForMove` | `handle_selection_demotion` returns while `cursor_unmoved_since_flush` (Condition 3) | +| `DemotionClearsHeldState` | `handle_selection_demotion` clears the original buffer's `last_active_visual_selection` and `cursor_at_flush` after it demotes | +| `DebounceIgnoresStale` | the debounce callback returns unless `M.state.debounce_timer` is its own timer | +| `DemotionIgnoresStale` | the demotion callback returns unless `M.state.demotion_timer` is its own timer | +| `ClearsBeforeClose` | both `_cancel_*_timer` functions and both callbacks set the state field to `nil` before `timer:close()` | +| `EntryClearsHeld` | `on_mode_changed` calls `clear_held_state()` when visual mode starts, except in the Claude terminal | +| `FlushSkipReports` | the flush skipped for an operator calls `clear_held_state()`, then `M.update_selection()` when `latest_selection` is not empty | +| `PendingClearsHeld` | the cursor branch of `update_selection`'s pending-demotion case calls `clear_held_state()` when it reports the cursor | +| `ReconcileOnCursorMoved` | `on_cursor_moved` calls `reconcile_held_selection(not entered_buffer)` before the debounce, and the `CursorMoved`, `CursorMovedI` and `BufEnter` autocmd passes `args.event == "BufEnter"` (the window cursor is not restored yet at `BufEnter`) | +| `ReconcileOnTextChanged` | `on_text_changed` calls `reconcile_held_selection(true)` before the debounce, from the `TextChanged`, `TextChangedI` and `TextChangedP` autocmd | +| `TextChangeReports` | `reconcile_held_selection` returns after `demote_if_selection_text_changed()`, which clears the held state and calls `update_selection` when the changedtick of the selection's buffer moved since the selection was read and `selection_text_is_there` says no | +| `MoveReports` | `reconcile_held_selection` clears the held state and calls `update_selection` when `compare_cursor` and the cursor is not `cursor_unmoved_since_flush` | +| `LeaveNoted` | `reconcile_held_selection` notes another buffer in `cursor_at_flush.away`, and sets `cursor_at_flush.left` for one that is not the Claude terminal, once the next event arrives | +| `ReadRecordsTick` | the flush and the in-visual `update_selection` call `record_selection_read`, which records `selection_tick` (the buffer and its changedtick) next to the selection they read | +| `ListensToSelectionBuffer` | `record_selection_read` also calls `watch_selection_buffer`, which attaches an `nvim_buf_attach` listener (`on_lines`, `on_reload`) whose callback schedules `demote_if_selection_text_changed`. `TextChanged` fires only for the current buffer | +| `TerminalReportsHeldBuffer` | `demote_if_selection_text_changed` also runs when the Claude terminal is current and the selection's buffer is another one (`from_terminal`): it clears the held state and sends `cursor_in_other_buffer`, because `update_selection` does nothing in the terminal | +| `UpdateChecksHeldText` | `update_selection` in the Claude terminal calls `demote_if_selection_text_changed()` after it cancels the demotion, because a new terminal is not registered when `BufEnter` fires | +| `ListenerNotesVisualEdit` | `on_mode_changed` calls `watch_selection_buffer(buf)` when visual mode starts in a buffer that is not the Claude terminal. Its `on_lines` finds the buffer's `visual_entry` (`visual_entry_of`) and `note_visual_edit` adds one to `unchecked_edits` | +| `VisualCheckSparesPluginEdit` | `note_visual_edit` schedules a check with `vim.schedule` that takes the edit back and sets `consumed` only when visual mode is over: a plugin's edit leaves the selection on the screen, an operator ends visual mode | +| `FlushIgnoresTick` | neither `on_mode_changed` nor the flush reads a changedtick (comments apart). `FALSE` models the code before #524: the flush returned when the changedtick moved since visual mode started, which took a plugin's edit of another line or a `:write` for an operator | + +Five guards break no rule alone, because another guard covers for them. `--mutants` removes each with the guard that covers for it, and the rule that breaks is the one `EXPECT` in `check.sh` names. `LeaveNoted` breaks `HeldEndsWhenMoved` alone, but only with 2 files, so `--mutants` runs that rule with 2 files. `ReconcileOnTextChanged` breaks `NoDeletedText` alone in the model, because of `YouEditByPlugin`. On real Neovim that guard and `TextChangeReports` are not the only ones that end the hold after an edit of the current buffer: the listener's `on_lines` fires for that edit too and runs the same check, so the running plugin still ends the hold without either guard (`replays/held_after_plugin_edit.lua` prints `OK` with the call removed from `on_text_changed`). The model lets the listener see only an edit of a buffer that is not current (`YouEditOtherBuffer`). A `BROKEN` trace for one of these two guards is a counterexample of the model, not a failure of the running plugin. `--mutants` still requires them, because the model has no other way to end the hold at that edit. + +| Removed together | Rule that breaks | The two guards | +| ------------------------------------------------ | ------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| `DemotionClearsHeldState` and `MoveReports` | `ClaudeSeesCursor` | The demotion forgets the held selection after it reports the cursor. A cursor move reports the cursor and forgets the held selection at once. | +| `PendingClearsHeld` and `ReconcileOnCursorMoved` | `ClaudeSeesCursor` | A pending-demotion update forgets the held selection when it reports the cursor. `CursorMoved` and `BufEnter` reconcile the hold at once. | +| `ElseClearsHeldState` and `LeaveNoted` | `SameFile` | The last branch of `update_selection` forgets the held selection. A buffer entered other than the Claude terminal ends the hold. | +| `EntryClearsHeld` and `FlushSkipReports` | `HeldEndsWhenMoved` | A new visual selection forgets the held one. A flush skipped for an operator forgets it. | + +The model also has three environment switches that are not facts. `check.sh` sets them in `tla_constants`: + +- `DelayBelowDebounce`: `TRUE` restricts the model to the default order (`visual_demotion_delay_ms` 50 < `debounce_ms` 100): a demotion timer fires before any debounce timer started after it. `check.sh` uses `FALSE`, which covers every delay. +- `WithTerminal`: `TRUE` lets the user go to a Claude terminal buffer. `FALSE` models `terminal.provider = "none"` or `"external"`. `check.sh` always uses `TRUE`. +- `MaxEdits`: edits per file, 1. + +On `BROKEN`, the script prints the TLC trace as action names. Each action names the step it models: `YouStartSelecting`, `YouExtendSelection`, `YouReleaseSelection` (Esc), `YouEditSelection` (`d`, `c`), `YouMoveCursor`, `YouEditAtCursor` (`x`), `YouEditByPlugin` (a plugin or reload changes the text: `TextChanged` without `CursorMoved`), `YouEditByPluginInVisual` and `YouWriteInVisual` (a plugin edits another line, or `:write` runs, while you select: only the changedtick moves), `YouEditOtherBuffer` (the same for a file that is not the current buffer: no `TextChanged`, no `BufEnter`), `YouEditElsewhere`, `YouSwitchBuffer`, and for each timer `...TimerFires` (the uv timer fires and queues its callback) and `...CallbackRuns`. `ListenerCheckRuns` is the check that the buffer listener queued with `vim.schedule`. Read the trace with the pstack `/statechart` skill: + +1. Rerun with `--keep`. +2. Copy the broken run's `.cfg` from the kept dir. Shrink it: `Files = {f1}` unless the rule is `SameFile`, `HeldEndsWhenMoved` or `NoDeletedText`, `Ranges = {r1}`, `Pos = {p1}` unless the path moves the cursor, `MaxEdits = 0` unless it edits, `WithTerminal = FALSE` unless it visits the Claude terminal. Stop at the smallest config that still breaks the rule. +3. Give `/statechart` the kept `SelectionTracking.tla`, that cfg, and the view `model/statechart-view.ts`. + +The report tells the path in plain words, for example "you start selecting, you press Esc, you press x on the cursor, 100 ms pass, the plugin updates Claude: Claude holds text you deleted from a.txt". That is the path of the `NoDeletedText` bug below. + +Then decide which kind of failure it is: + +- **Real bug.** A fact went `FALSE` because the change removed or moved a guard, or the facts are `TRUE` and the path is one the code can take. Replay it on headless Neovim with a probe in `replays/` (see below) before you report it. Report it in the code's words. Never weaken a rule or the model to make it pass. +- **Modeling error.** The facts are `TRUE` but the path needs a step the code cannot take, or a fact reads `FALSE` because the guard was reworded and still works. Fix the regex or the model, run `--mutants`, and say what you changed. If a replay does not show the bug, assume the model is wrong until you show it is not. + +## Replays + +Each probe in `replays/` starts the plugin through the real `require("claudecode").start()` with `terminal.provider = "none"`, then types keys through Neovim's main loop with real timers. It replaces only `server.broadcast`, in its own process, to record each `selection_changed`. It prints one line per step, the settled state, `OK` or `BUG`, and a count line, and Neovim exits 0 for `OK` and 1 for `BUG`. Each probe replays a path that once broke a rule (see "Bugs this model found"), or a limit that the model does not cover (the rows whose rule is `none`), so `OK` shows the promise kept or the limit as documented. Three probes replay known bugs and print `BUG` until their fix lands (see "Scope and bounds"). A probe does not prove that one guard is needed on its own: the listener also covers for `ReconcileOnTextChanged` and `TextChangeReports` at runtime (see "Read the result"). + +```bash +NVIM=~/.local/share/mise/installs/neovim/0.12.3/bin/nvim \ + .agents/skills/verify-selection-tracking/replays/run.sh held_after_operator.lua +``` + +`run.sh` puts this checkout first on `runtimepath` and gives each run a fresh `XDG_*_HOME`, `CLAUDE_CONFIG_DIR` and `TMPDIR` under `$XUM_SCRATCH_DIR` (or `/tmp`), removed afterwards. `DELAY_MS=50` reruns the two long-delay probes (`other_file_after_return.lua`, `cursor_after_return.lua`) with the default delay. They use 1000 ms. + +| Probe | Keys | Rule | +| ---------------------------------------------- | -------------------------------------------------------------------------- | ----------------------------------------------------- | +| `held_after_operator.lua` | `vb`, Esc, `gv`, `d` | `HeldEndsWhenMoved`, `NoDeletedText` | +| `held_after_quick_move.lua` | `ve`, Esc, `l`, then `h` 30 ms later | `HeldEndsWhenMoved` | +| `held_after_edit.lua` | `viw`, Esc, `x`, `x` | `NoDeletedText` | +| `held_after_plugin_edit.lua` | `Vj`, Esc, a plugin deletes text of line 1 | `NoDeletedText` | +| `held_after_reload_in_terminal.lua` | `ve`, Esc, the Claude terminal, Neovim reloads the rewritten file | `NoDeletedText` | +| `held_after_edit_in_terminal.lua` | `ve`, Esc, the Claude terminal, a plugin deletes the selected text | `NoDeletedText` | +| `other_file_after_return.lua` | `ve`, Esc, `:b b.txt`, `:b a.txt`, a long delay | `SameFile` | +| `cursor_after_return.lua` | `ve`, Esc, `l`, `h` 250 ms later, a long delay | `ClaudeSeesCursor` | +| `held_after_line_inserted_above.lua` | `ve`, Esc, a plugin inserts a line above the selection | none: a limit that the model skips | +| `release_after_plugin_edit_in_visual.lua` | `ve`, a plugin edits line 2, Esc within 100 ms | `ReleaseSent`, `HeldUntilMoved` | +| `release_after_plugin_append_in_visual.lua` | `ve`, a plugin appends two lines, Esc within 100 ms | `ReleaseSent`, `HeldUntilMoved` | +| `release_after_write_in_visual.lua` | a modified buffer, `ve`, `:write`, Esc within 100 ms | `ReleaseSent`, `HeldUntilMoved` | +| `release_in_same_typeahead_as_plugin_edit.lua` | `ve`, then one mapping edits line 2 and presses Esc | `ReleaseSent`: a known bug, `BUG` until its fix lands | +| `release_with_key_during_plugin_callback.lua` | `ve`, a timer callback edits line 2 and `nvim_input` sends Esc during it | `ReleaseSent`: a known bug, `BUG` until its fix lands | +| `release_after_autocmd_edit_in_visual.lua` | `ve` in one typeahead, a `ModeChanged` autocmd for `n:v` edits line 2 | `ReleaseSent`: a known bug, `BUG` until its fix lands | +| `v_escape_selects_one_character.lua` | `ve`, Esc, then `v` and Esc with no motion | none: shows a bare `v` Esc selects | + +## Bugs this model found + +The first version of the model found four broken rules on the code before #452. Each was replayed on Neovim 0.12.3 with the probe named, and #452 fixed all four: + +1. **`HeldEndsWhenMoved`: Claude kept a released selection after the cursor left it, when the cursor stood where the selection was released again by the time the debounce fired.** You select `alpha` backwards (`vb`), press Esc, press `gv`, press `d` (`held_after_operator.lua`). Or you select `alpha` (`ve`), press Esc, press `l` and then `h` within 100 ms (`held_after_quick_move.lua`). The plugin compared the cursor with `cursor_at_flush` only when a timer fired, and a new selection or an operator did not clear it. +2. **`NoDeletedText`: Claude kept a held selection after you edited its text without moving the cursor.** You select `alpha` (`viw`), press Esc, then `x` twice. Claude still held `alpha` after the line became `alphbeta gamma` (`held_after_edit.lua`). Nothing compared the held text with the buffer. +3. **`SameFile`: with a long `visual_demotion_delay_ms`, Claude held another file's cursor.** With 1000 ms: you select `alpha` in `a.txt`, press Esc, `:b b.txt`, `:b a.txt`. Claude held `b.txt` 0:0 until the cursor moved (`other_file_after_return.lua`). +4. **`ClaudeSeesCursor`: with a long `visual_demotion_delay_ms`, Claude held a cursor position you had left.** With 1000 ms: you select `alpha`, press Esc, press `l`, wait, press `h`. The cursor was at 0:4 and Claude held 0:5 (`cursor_after_return.lua`). + +#452 ends the hold when the cursor leaves, when a new selection starts, when an operator consumes the selection, and when its text changes. The model has each as a guard (`MoveReports`, `EntryClearsHeld`, `FlushSkipReports`, `TextChangeReports`). + +A review of #452 found one more path, and #471 fixed it: Claude holds selection A, you start selection B, an operator consumes B before the 100 ms in-visual debounce, and you enter the Claude terminal inside that 100 ms. Claude kept A for the whole visit. The model has the fixed flush-skip step (`FlushSkipReports`). `tests/integration/selection_held_spec.lua` replays that exact path with a real terminal buffer. See "Scope and bounds" for what the model can and cannot say about it. + +A reviewer of this skill found one more path that no model step could express then, and #481 fixed 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 edits it). `TextChanged` fires only for the current buffer, so Claude kept A's old text until you came back (`replays/held_after_reload_in_terminal.lua`, `replays/held_after_edit_in_terminal.lua`). The model has a step for it (`YouEditOtherBuffer`) and three guards: `ListensToSelectionBuffer`, `TerminalReportsHeldBuffer` and `UpdateChecksHeldText`. The model found the last one in the first version of that fix: a file that changes while you are in another file, just before you open a new Claude terminal, finds the terminal unregistered at `BufEnter`, so only the debounce can send the cursor. + +An advisor of this skill found a last path that the model could not express, and #524 fixed 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. Entering visual mode had recorded the buffer's changedtick, and the flush took a moved changedtick for an operator that consumed the selection, so Claude got the cursor and not the selection, although its text was untouched (`replays/release_after_plugin_edit_in_visual.lua`, `release_after_plugin_append_in_visual.lua`, `release_after_write_in_visual.lua`). #524 replaced the comparison with a `visual_entry` that the buffer listener marks: an operator's edit counts and ends in a skipped flush, a plugin's edit is checked once visual mode is known to be on, and a `:write` fires no callback. The model has two steps that move only the changedtick (`YouEditByPluginInVisual`, `YouWriteInVisual`) and three guards for the new code (`FlushSkipsOperator`, `ListenerNotesVisualEdit`, `VisualCheckSparesPluginEdit`). `FlushIgnoresTick` keeps the old comparison out: put it back into `selection.lua` and `check.sh` exits 1 and prints the first broken rule, `ReleaseSent` (you select, a plugin edits another line, you press Esc). `--mutants` lists the others that break with it: `HeldUntilMoved` and `HeldInTerminal`. Paths of the same kind are still open: any edit whose check has not run when the next key arrives. Three are reproduced (`replays/release_in_same_typeahead_as_plugin_edit.lua`, `release_with_key_during_plugin_callback.lua` and `release_after_autocmd_edit_in_visual.lua` print `BUG`; see "Scope and bounds"). Fix PR #540 fixes all three. + +## Update after an intended change + +1. Read every `was:`/`now:` line of the STALE output and the code behind it. + - If only `file` lines changed, and the change cannot reach the selection state, a timer, a send, or the tools (for example a diff or terminal change in `init.lua`), say so in the PR. Then skip to step 4. +2. If the behavior changed, change the action or operator in `model/SelectionTracking.tla` that cites that code (`Update`, `Demote`, `Flush`, `Reconcile`, `OnModeChanged`, `DebounceUpdate`, the `Cancel*` operators, the listener operators `OnOtherBufferChanged`, `ListenerCheck`, `TerminalChanged` and `ReportHeldBuffer`, the entry operators `TickMoved`, `EntryEdited` and `PluginEditedInVisual`, or a `You*` step). If a guard moved, change its fact regex in `check.sh`. A regex must read its own guard only: remove each guard from `lua/` alone and see that only its own fact reads `FALSE`. If a rule breaks on the new code, that is a finding: replay it, and fix the code, not the rule. +3. Run `check.sh --mutants`. Every fact must be caught by its rule, alone or in a listed pair (`EXPECT`), and every rule must break at least once. +4. Run `check.sh` and read the result. +5. Run `check.sh --record` only once you have confirmed that the model describes the code at this commit. Commit `covered.lock` with the change. + +## Scope and bounds + +- The main run uses 2 files, the Claude terminal, 2 cursor positions, 2 selection ranges and 1 edit per file, any `visual_demotion_delay_ms` (129,986 distinct states). The `--mutants` runs use 1 file, except `SameFile`, `HeldEndsWhenMoved` and `NoDeletedText` with 2. +- One model step is one key or command together with the autocmds it fires (`ModeChanged`, `TextChanged`, `CursorMoved`, `BufEnter`). They run in the same main-loop iteration as the key, before Neovim polls libuv again, so no timer callback runs between them. A window command such as `w` in visual mode fires `ModeChanged` in the old buffer first (checked on Neovim 0.12.3), so the model splits it into Esc and a buffer switch. Each uv timer firing and each scheduled callback is its own step, the listener's queued check included (`ListenerCheckRuns`). The one exception is the check of an edit that you make while you select: the model runs it in the step of the edit, which is true only when it runs before the next key (see the bullet on edits in visual mode). The model can fire a timer between any two keys, which also covers typeahead. Typed one key at a time, each key fires its autocmds before the next. Keys that run with no main-loop turn between them (a mapping, a macro, `:normal!`, typeahead) fire `CursorMoved` and `TextChanged` later or not at all: #471 was such a path. `YouEditSelection` leaves both out, so it is the case in which they have not fired yet. +- An operator in visual mode (`d`, `c`, `>`) sets the mode to normal before it changes the text, and `ModeChanged` (`v` to `n`) fires after the change: the listener's `on_lines` runs first, with the mode already normal, and the flush that `ModeChanged` triggers comes second. That order holds for 8 of 8 operators (`d`, `c`, `>`, `gU`, `~`, `J`, `r` and `x`) on Neovim 0.8.0 and 0.12.3, and the mode in `on_lines` is normal for these operators also on 0.9.5, 0.10.4 and 0.11.4. So the edit is counted before the flush. The cursor lands on any position. A plugin's edit in visual mode runs `on_lines` with the mode `n` on 0.8 and 0.9 (Neovim ends visual mode for the length of `nvim_buf_set_lines` and `nvim_buf_set_text`) and `v` from 0.10, so the code tests the mode in a `vim.schedule` callback, after the call. The model has no mode inside a call and runs that check before the next key. +- At `BufEnter` the window cursor is not restored yet, so the model compares it only at `CursorMoved` and `TextChanged`. A new Claude terminal is not registered when `BufEnter` fires, so the model lets the plugin not know it yet (`termKnown`) and decide at the next event. +- An edit changes the held text (`YouEditSelection`, `YouEditAtCursor`, `YouEditByPlugin`, `YouEditOtherBuffer`) or leaves it alone (`YouEditElsewhere`, and, while you select, `YouEditByPluginInVisual` and `YouWriteInVisual`, which move only the changedtick). 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 #524 only compared it with the value recorded at entry, and a changedtick only grows. Each buffer has one text version, so the model cannot tell the text of the held selection from the text of another selection in the same buffer: the #471 path (an operator consumes a different selection) is checked by `tests/integration/selection_held_spec.lua`, and `FlushSkipReports` breaks no rule alone, because the held text is found at the next check anyway (the debounce in the Claude terminal, `UpdateChecksHeldText`, or the next `CursorMoved`). It is caught together with `EntryClearsHeld`. An edit that moves the held range's lines, such as a line added above, is not modeled. The code reads the range again with `nvim_buf_get_text`, and reports the cursor when the held text is not there. A user sees Claude lose the selection and get the cursor on the shifted line, although the selected text still exists (`replays/held_after_line_inserted_above.lua`). That is a limit, not a rule. +- The listener on the buffer of the held selection (`ListensToSelectionBuffer`) is attached once the selection is read. It only queues the check with `vim.schedule` (`check_soon`), so the model sets a queued-check bit at the edit and runs the check in a separate step (`ListenerCheckRuns`), after any other step: in the Claude terminal it sends the cursor of the selection's buffer, in the buffer of the selection it ends the hold, in another file it does nothing. A scheduled callback runs after the command that made a new Claude terminal returned, so the plugin knows the terminal then. That `:edit`, `:edit!` and `:bunload` detach it (`on_detach`), that the listener attaches itself again (from a `vim.schedule` callback, and only for a loaded buffer, because `nvim_buf_attach` returns `false` for an unloaded buffer and the `watched_buffers` entry would then block the next listener), and that `:checktime` keeps it (`on_reload`) are not modeled: `tests/selection_test.lua` and `tests/integration/selection_held_spec.lua` check them. If one of them went wrong, the listener would be gone (or doubled) after such a command, and a user in the Claude terminal would see Claude keep text that a reload or a plugin deleted until they come back. +- A held selection whose buffer becomes a Claude terminal after the selection was read is not modeled: the buffers of the model are files and the terminal `Term`, and no step turns one into the other. The triggers that were reproduced are `termopen()` in the buffer and a rename to a `term://...claude` name. A reload with a custom `terminal_cmd` did not reproduce it. Before #493, a change of that buffer's text made `update_selection` and `demote_if_selection_text_changed` call each other until Neovim raised `stack overflow` (from `CursorMoved`, `TextChanged` and `vim.schedule` callbacks) on every event, and Claude kept the old text. In another Claude terminal, the check also sent the cursor of that buffer, with a `term://` path. #493 fixed both: the check sends no cursor of a Claude terminal, cancels a pending demotion and forgets the read. `tests/selection_test.lua` and three cases of `tests/integration/selection_held_spec.lua` ("does not overflow the stack when the buffer of the held selection is taken for the Claude terminal", "does not send a cursor of the buffer that became the Claude terminal when a demotion is pending" and "sends nothing when the buffer of the held selection became a Claude terminal and you are in another") cover it. A change that brings the recursion back reads STALE here, and no rule breaks. +- `latest_selection` is what Claude holds: every send sets it first, `M.server` is always set while tracking runs, and both tools return it when it is set. +- `is_claude_terminal_buffer` finds the Claude terminal by a `term://` buffer name whose command contains `claude`, or by `terminal.get_active_terminal_bufnr()`. The model has one terminal buffer, `Term`, and treats both checks as one. `handle_selection_demotion` checks only `terminal.get_active_terminal_bufnr()` (Condition 1). In a terminal that only the name check knows, a demotion does not take Condition 3, which needs the current buffer to be the buffer it was scheduled for. It only clears the held-state records of that buffer and sends nothing. The model does not tell the two apart, so no TLC run tested that difference. I read it from the code and did not replay it. +- "After `:ClaudeCodeStop` nothing is sent" is not a rule, because no `selection.lua` guard can break it alone. `init.lua` `M.stop` calls `selection.disable()`, which clears the autocmds, both timers and `M.server`, and then stops the server, and `server.broadcast` returns `false` without a server. Start, stop and restart are not modeled. +- Not modeled, each with what a user sees when the code goes wrong there (read from the code, not replayed): + - Select mode as distinct from Visual mode: `utils.selection_type` maps both to the same selection type, so Claude would answer about a selection in Select mode as in Visual mode. A wrong mapping makes Claude miss that selection. + - Empty selections (no text): the flush skips them. If the skip went wrong, Claude would hold a selection with no text. A bare `v` and Esc is not empty: it selects the character under the cursor, and Claude gets that character in place of the held selection (`replays/v_escape_selects_one_character.lua`). + - A second Claude terminal: the model has one. `handle_selection_demotion` knows only the active terminal, so a demotion that fires in a terminal that only its name marks does not take Condition 3. It clears the held-state records of the buffer it was scheduled for and sends nothing. If it did take Condition 3, Claude would get the cursor of that terminal. + - `send_current_selection`: no code in `lua/` calls it. A bug there reaches a user only through a mapping the user wrote. + - `:ClaudeCodeSend` at-mentions: they send a file and range mention, not the tracked selection. A bug there makes Claude get the wrong mention. + - Insert mode as distinct from normal mode: `TextChangedI` and `TextChangedP` run the same handler as `TextChanged`. If they stopped doing so, Claude would keep a held selection that you typed over in insert mode. + - A held selection whose buffer is unloaded while you are in the Claude terminal (`:bunload`): `demote_if_selection_text_changed` returns for a buffer that is not loaded, so the selection stays held. The model has no unloaded buffer. A user sees Claude keep the selection of a file that is not loaded until they come back, and then get the cursor (checked on Neovim 0.8.0 and 0.12.3 with `:bunload` in a Claude terminal tab and `:buffer` after it). The text on disk did not change, so Claude holds no text that is gone. Without the return, the check could not find the text in the unloaded buffer, would take it for gone, and would send the cursor of a file that is not loaded (read from the code). The listener is detached by the unload (`on_detach`) and attaches itself again only for a loaded buffer. +- Edits while you are in visual mode that the model leaves out: an edit of the selected text itself (the debounce or the listener's check reads the new text), and any edit whose check has not run when the next key arrives. The model runs the check of a plugin's edit in the step of the edit, which is true only when the check comes before the next key. The code runs it in `vim.schedule`, after the command or callback that made the edit returns. When a key comes first, the flush on Esc finds an edit that nobody checked and takes it for an operator's: a user sees Claude get the cursor and not the selection, although its text is untouched. Three ways to get there are reproduced on Neovim 0.8.0 and 0.12.3, and each is a known bug, not a limit by design: a mapping that edits and presses Esc in one typeahead (`replays/release_in_same_typeahead_as_plugin_edit.lua`), a key that arrives while the plugin's timer callback still runs (`replays/release_with_key_during_plugin_callback.lua`, with `nvim_input`, the way a UI sends a key), and an autocmd that edits when visual mode starts with the Esc already in the typeahead (`replays/release_after_autocmd_edit_in_visual.lua`, a `ModeChanged` handler for `n:v`). The three print `BUG` until fix PR #540 merges, and `OK` in a tree with #540. The model does not show them, so a PASS says nothing about them. A plugin edit whose callback ends before the next key is not like this (`replays/release_after_plugin_edit_in_visual.lua`). +- A reload or `:edit` while you select (`on_reload` and `on_detach` set `consumed`) counts as an operator, because it replaces the text under the selection. It is not modeled: a user sees Claude get the cursor and not the selection after the file was reloaded under it. +- Coming back from the Claude terminal to the file of a held selection with the cursor where it was, the model allows Claude to hold either the selection or the cursor (`holdLoose`), and `HeldUntilMoved`, `HeldInTerminal` and `HeldEndsWhenMoved` make no claim there. A user sees Claude hold either the selection or only the cursor there, and the model allows both. +- A Claude that connects after the last change gets no `selection_changed` until the selection changes: `on_connect` sends none, and `has_selection_changed` stops a resend of an unchanged selection. PROTOCOL.md promises a notification only when the selection changes, and the tools answer on request, so this is not a rule. +- A pass covers this model at these bounds, for the facts `check.sh` reads, on the covered files exactly as recorded in `covered.lock`. Any other tree reads STALE. diff --git a/.agents/skills/verify-selection-tracking/check.sh b/.agents/skills/verify-selection-tracking/check.sh new file mode 100755 index 000000000..6d9458d23 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/check.sh @@ -0,0 +1,297 @@ +#!/usr/bin/env bash +# shellcheck disable=SC2034,SC2154,SC2329 # check-lib.sh reads these; covered_block sets the block variables +# Model-check what Claude sees as the current selection (lua/claudecode/selection.lua) against facts read +# from the code. +# Usage: check.sh [--mutants] [--keep] [--record] | check.sh --hash-only +# exit 0 pass, 1 rule broken, 2 tool or script error (or TypeOK broken), 3 stale +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +SKILL=verify-selection-tracking MODEL=SelectionTracking +source "$here/../../../scripts/tla/check-lib.sh" +tla_init "$@" + +SEL=lua/claudecode/selection.lua +MAIN=lua/claudecode/init.lua +SERVER=lua/claudecode/server/init.lua +CURRENT_TOOL=lua/claudecode/tools/get_current_selection.lua +LATEST_TOOL=lua/claudecode/tools/get_latest_selection.lua +COVERED=("$SEL" "$MAIN" "$SERVER" "$CURRENT_TOOL" "$LATEST_TOOL") +SITE_RE='(latest_selection|last_active_visual_selection|cursor_at_flush|visual_entry|debounce_timer|demotion_timer|send_selection_update|flush_visual_selection|update_selection|handle_selection_demotion|selection_tick|watched_buffers|watch_selection_buffer|record_selection_read|reconcile_held_selection|clear_held_state|selection_changed|selection\.(enable|disable))' + +covered_block unmoved "$SEL" '^local function cursor_unmoved_since_flush\(' +covered_block clear_held "$SEL" '^local function clear_held_state\(' +covered_block text_there "$SEL" '^local function selection_text_is_there\(' +covered_block cursor_other "$SEL" '^local function cursor_in_other_buffer\(' +covered_block demote_text "$SEL" '^local function demote_if_selection_text_changed\(' +covered_block holds_selection "$SEL" '^local function holds_selection_of\(' +covered_block entry_of "$SEL" '^local function visual_entry_of\(' +covered_block note_edit "$SEL" '^local function note_visual_edit\(' +covered_block watch_buffer "$SEL" '^local function watch_selection_buffer\(' +covered_block record_read "$SEL" '^local function record_selection_read\(' +covered_block reconcile "$SEL" '^local function reconcile_held_selection\(' +covered_block enable "$SEL" '^function M\.enable\(' +covered_block disable "$SEL" '^function M\.disable\(' +covered_block cancel_debounce "$SEL" '^function M\._cancel_debounce_timer\(' +covered_block cancel_demotion "$SEL" '^function M\._cancel_demotion_timer\(' +covered_block autocmds "$SEL" '^function M\._create_autocommands\(' +covered_block on_cursor_moved "$SEL" '^function M\.on_cursor_moved\(' +covered_block on_mode_changed "$SEL" '^function M\.on_mode_changed\(' +covered_block on_text_changed "$SEL" '^function M\.on_text_changed\(' +covered_block debounce_update "$SEL" '^function M\.debounce_update\(' +covered_block update_selection "$SEL" '^function M\.update_selection\(' +covered_block demotion "$SEL" '^function M\.handle_selection_demotion\(' +covered_block from_marks "$SEL" '^function M\.get_visual_selection_from_marks\(' +covered_block flush "$SEL" '^function M\.flush_visual_selection\(' +covered_block changed "$SEL" '^function M\.has_selection_changed\(' +covered_block send_update "$SEL" '^function M\.send_selection_update\(' +covered_block get_latest "$SEL" '^function M\.get_latest_selection\(' +covered_block is_terminal "$SEL" '^function M\.is_claude_terminal_buffer\(' +covered_block start "$MAIN" '^function M\.start\(' +covered_block stop "$MAIN" '^function M\.stop\(' +covered_block broadcast "$SERVER" '^function M\.broadcast\(' +covered_block on_connect "$SERVER" '^ *on_connect = function\(client\)' +covered_block current_tool "$CURRENT_TOOL" '^local function handler\(' +covered_block latest_tool "$LATEST_TOOL" '^local function handler\(' + +FACTS=(FlushOnVisualExit FlushSkipsOperator FlushSkipsTerminal FlushRecordsCursor UpdateSkipsTerminal + PendingKeepsHeld ElseClearsHeldState DemotionWaitsForMove DemotionClearsHeldState DebounceIgnoresStale + DemotionIgnoresStale ClearsBeforeClose EntryClearsHeld FlushSkipReports PendingClearsHeld ReconcileOnCursorMoved + ReconcileOnTextChanged TextChangeReports MoveReports LeaveNoted ReadRecordsTick ListensToSelectionBuffer + TerminalReportsHeldBuffer UpdateChecksHeldText ListenerNotesVisualEdit VisualCheckSparesPluginEdit FlushIgnoresTick) + +# ModeChanged runs on_mode_changed, which flushes when visual mode ends. +flush_on_visual_exit() { + in_order '^ vim\.api\.nvim_create_autocmd\("ModeChanged", \{$' '^ M\.on_mode_changed\(\)$' <<<"$autocmds" && + in_order 'local leaving_visual = is_visual_mode\(event\.old_mode\) and not is_visual_mode\(event\.new_mode\)$' \ + '^ elseif leaving_visual then$' '^ M\.flush_visual_selection\(\)$' <<<"$on_mode_changed" +} +fact[FlushOnVisualExit]=$(as_bool flush_on_visual_exit) +# Entering visual mode makes a visual_entry. The flush returns when the entry is consumed or has an edit that the listener +# counted and no check has cleared yet (an operator such as d: its edit comes before the ModeChanged that flushes). +flush_skips_operator() { + in_order '^ if entering_visual then$' \ + '^ M\.state\.visual_entry = \{ bufnr = buf, consumed = false, unchecked_edits = 0 \}$' \ + <<<"$on_mode_changed" && + in_order '^ local entry = M\.state\.visual_entry$' \ + '^ if entry and entry\.bufnr == current_buf and \(entry\.consumed or entry\.unchecked_edits > 0\) then$' \ + '^ return$' 'M\.get_visual_selection_from_marks\(\)' <<<"$flush" +} +fact[FlushSkipsOperator]=$(as_bool flush_skips_operator) +# Each terminal guard compares the current buffer with the active Claude terminal buffer and returns. The flush's next +# statement after its guard is `local entry`: a later `return` (the operator skip) must not stand in for the guard's. +fact[FlushSkipsTerminal]=$(as_bool in_order 'if M\.is_claude_terminal_buffer\(current_buf\) then' '^ *return$' \ + '^ local entry = M\.state\.visual_entry$' <<<"$flush") +fact[UpdateSkipsTerminal]=$(as_bool in_order 'if M\.is_claude_terminal_buffer\(current_buf\) then' 'M\._cancel_demotion_timer\(\)' '^ *return$' \ + '^ local current_mode_info = vim\.api\.nvim_get_mode\(\)$' <<<"$update_selection") +fact[FlushRecordsCursor]=$(as_bool in_order 'M\.get_visual_selection_from_marks\(\)' \ + '^ M\.state\.cursor_at_flush = \{ bufnr = current_buf, pos = vim\.api\.nvim_win_get_cursor\(0\) \}$' \ + 'M\.send_selection_update\(selection\)' <<<"$flush") +# cursor_unmoved_since_flush compares the window cursor with cursor_at_flush in the same buffer. +unmoved_reads_flush() { + in_order '^ local caf = M\.state\.cursor_at_flush$' '^ if not caf or caf\.bufnr ~= bufnr or caf\.left then$' \ + '^ return false$' '^ local pos = vim\.api\.nvim_win_get_cursor\(0\)$' \ + '^ return pos\[1\] == caf\.pos\[1\] and pos\[2\] == caf\.pos\[2\]$' <<<"$unmoved" +} +pending_keeps_held() { + unmoved_reads_flush && + in_order '^ if M\.state\.demotion_timer then$' '^ if cursor_unmoved_since_flush\(current_buf\) then$' \ + '^ current_selection = M\.state\.latest_selection$' '^ else$' \ + '^ current_selection = M\.get_cursor_position\(\)$' <<<"$update_selection" +} +fact[PendingKeepsHeld]=$(as_bool pending_keeps_held) +fact[ElseClearsHeldState]=$(as_bool in_order 'M\.handle_selection_demotion\(current_buf\)' '^ else$' \ + '^ current_selection = M\.get_cursor_position\(\)$' '^ M\.state\.last_active_visual_selection = nil$' \ + '^ M\.state\.cursor_at_flush = nil$' '^ end$' <<<"$update_selection") +demotion_waits_for_move() { + unmoved_reads_flush && + in_order '^ if current_buf == original_bufnr_when_scheduled then$' \ + '^ if cursor_unmoved_since_flush\(current_buf\) then$' '^ return$' \ + '^ local new_sel_for_demotion = M\.get_cursor_position\(\)$' <<<"$demotion" +} +fact[DemotionWaitsForMove]=$(as_bool demotion_waits_for_move) +fact[DemotionClearsHeldState]=$(as_bool in_order 'M\.send_selection_update\(M\.state\.latest_selection\)' \ + 'M\.state\.last_active_visual_selection\.bufnr == original_bufnr_when_scheduled' \ + '^ M\.state\.last_active_visual_selection = nil$' \ + '^ if M\.state\.cursor_at_flush and M\.state\.cursor_at_flush\.bufnr == original_bufnr_when_scheduled then$' \ + '^ M\.state\.cursor_at_flush = nil$' <<<"$demotion") +# Each timer callback returns unless its timer is still the one in M.state. +fact[DebounceIgnoresStale]=$(as_bool in_order 'vim\.schedule_wrap\(function\(\)' \ + '^ if M\.state\.debounce_timer ~= timer then$' '^ return$' 'timer:close\(\)' \ + 'M\.update_selection\(\)' <<<"$debounce_update") +fact[DemotionIgnoresStale]=$(as_bool in_order 'vim\.schedule_wrap\(function\(\)' \ + '^ if M\.state\.demotion_timer ~= timer then$' '^ return$' 'timer:close\(\)' \ + 'M\.handle_selection_demotion\(current_buf\)' <<<"$update_selection") +# Both cancel functions and both callbacks clear the state field before timer:close(). +clears_before_close() { + in_order '^ M\.state\.debounce_timer = nil$' '^ timer:close\(\)$' <<<"$cancel_debounce" && + in_order '^ M\.state\.demotion_timer = nil$' '^ timer:close\(\)$' <<<"$cancel_demotion" && + in_order 'vim\.schedule_wrap\(function\(\)' '^ M\.state\.debounce_timer = nil$' \ + '^ timer:close\(\)$' <<<"$debounce_update" && + in_order 'vim\.schedule_wrap\(function\(\)' '^ M\.state\.demotion_timer = nil$' \ + '^ timer:close\(\)$' <<<"$update_selection" +} +fact[ClearsBeforeClose]=$(as_bool clears_before_close) + +# clear_held_state() forgets both records of a held selection. +clear_held_clears_both() { + in_order '^ M\.state\.last_active_visual_selection = nil$' '^ M\.state\.cursor_at_flush = nil$' <<<"$clear_held" +} +# A new visual selection replaces the held one, except in the Claude terminal. +entry_clears_held() { + clear_held_clears_both && + in_order '^ if entering_visual then$' '^ if not M\.is_claude_terminal_buffer\(buf\) then$' '^ clear_held_state\(\)$' \ + '^ elseif leaving_visual then$' <<<"$on_mode_changed" +} +fact[EntryClearsHeld]=$(as_bool entry_clears_held) +# A flush skipped for an operator forgets the held selection and reports the cursor when Claude holds a selection. +flush_skip_reports() { + clear_held_clears_both && + in_order '^ local entry = M\.state\.visual_entry$' '^ clear_held_state\(\)$' \ + '^ local held = M\.state\.latest_selection$' '^ if held and not held\.selection\.isEmpty then$' '^ M\.update_selection\(\)$' \ + '^ return$' 'M\.get_visual_selection_from_marks\(\)' <<<"$flush" +} +fact[FlushSkipReports]=$(as_bool flush_skip_reports) +# The pending-demotion branch ends the hold when it reports the cursor. +pending_clears_held() { + clear_held_clears_both && + in_order '^ if M\.state\.demotion_timer then$' '^ else$' \ + '^ current_selection = M\.get_cursor_position\(\)$' '^ clear_held_state\(\)$' <<<"$update_selection" +} +fact[PendingClearsHeld]=$(as_bool pending_clears_held) +# The two autocmd handlers call reconcile_held_selection. The BufEnter autocmd says so, because the window cursor is +# not restored yet then. +reconcile_on_cursor_moved() { + in_order '^ reconcile_held_selection\(not entered_buffer\)$' '^ M\.debounce_update\(\)$' <<<"$on_cursor_moved" && + in_order '^ vim\.api\.nvim_create_autocmd\(\{ "CursorMoved", "CursorMovedI", "BufEnter" \}, \{$' \ + '^ M\.on_cursor_moved\(args\.event == "BufEnter"\)$' <<<"$autocmds" +} +fact[ReconcileOnCursorMoved]=$(as_bool reconcile_on_cursor_moved) +reconcile_on_text_changed() { + in_order '^ reconcile_held_selection\(true\)$' '^ M\.debounce_update\(\)$' <<<"$on_text_changed" && + in_order '^ vim\.api\.nvim_create_autocmd\(\{ "TextChanged", "TextChangedI", "TextChangedP" \}, \{$' '^ M\.on_text_changed\(\)$' <<<"$autocmds" +} +fact[ReconcileOnTextChanged]=$(as_bool reconcile_on_text_changed) +# reconcile_held_selection first reports the cursor when the changedtick moved since the selection was read and its +# text is no longer at its range. +text_change_reports() { + clear_held_clears_both && + in_order '^ if demote_if_selection_text_changed\(\) then$' '^ return$' <<<"$reconcile" && + in_order '^ if vim\.api\.nvim_buf_get_changedtick\(read\.bufnr\) == read\.tick or selection_text_is_there\(held, read\.bufnr\) then$' \ + '^ return false$' '^ clear_held_state\(\)$' '^ M\.update_selection\(\)$' '^ return true$' <<<"$demote_text" +} +fact[TextChangeReports]=$(as_bool text_change_reports) +# A cursor that left the flushed position is reported at once. +move_reports() { + clear_held_clears_both && + in_order '^ elseif compare_cursor and not cursor_unmoved_since_flush\(current_buf\) then$' '^ clear_held_state\(\)$' \ + '^ M\.update_selection\(\)$' <<<"$reconcile" +} +fact[MoveReports]=$(as_bool move_reports) +# Another buffer entered is noted in cursor_at_flush.away and decided at the next event: the Claude terminal keeps the +# hold, any other buffer sets cursor_at_flush.left, which cursor_unmoved_since_flush reads. +leave_noted() { + unmoved_reads_flush && + in_order '^ if caf\.away and caf\.away ~= current_buf then$' '^ if not M\.is_claude_terminal_buffer\(caf\.away\) then$' \ + '^ caf\.left = true$' '^ elseif caf\.bufnr ~= current_buf then$' '^ caf\.away = current_buf$' <<<"$reconcile" +} +fact[LeaveNoted]=$(as_bool leave_noted) +# The flush and the in-visual update call record_selection_read, which records the buffer and changedtick of the +# selection they read. +read_records_tick() { + in_order 'M\.get_visual_selection_from_marks\(\)' '^ record_selection_read\(current_buf\)$' \ + 'M\.send_selection_update\(selection\)' <<<"$flush" && + in_order 'M\.state\.last_active_visual_selection = \{' '^ record_selection_read\(current_buf\)$' \ + '^ else$' <<<"$update_selection" && + in_order '^ M\.state\.selection_tick = \{ bufnr = bufnr, tick = vim\.api\.nvim_buf_get_changedtick\(bufnr\) \}$' <<<"$record_read" +} +fact[ReadRecordsTick]=$(as_bool read_records_tick) +# record_selection_read listens to the buffer it records, and the listener schedules the check when the buffer changes +# (a reload or a plugin's edit: TextChanged fires only for the current buffer). +# on_lines and on_reload each call check_soon, at any indentation: the code before #524 called it straight from on_lines, and +# since then both calls sit inside `if holds_selection_of(buf) then`. +listens_to_selection_buffer() { + in_order '^ watch_selection_buffer\(bufnr\)$' <<<"$record_read" && + in_order '^ local function check_soon\(\)$' 'vim\.schedule\(function\(\)' '^ demote_if_selection_text_changed\(\)$' \ + '^ vim\.api\.nvim_buf_attach\(bufnr, false, \{$' '^ on_lines = function\(_, buf\)$' '^ *check_soon\(\)$' \ + '^ on_reload = function\(_, buf\)$' '^ *check_soon\(\)$' <<<"$watch_buffer" +} +fact[ListensToSelectionBuffer]=$(as_bool listens_to_selection_buffer) +# The check runs in the Claude terminal for a selection of another buffer that is not a Claude terminal, clears the held +# state and sends the cursor of that buffer: update_selection does nothing in the terminal. +terminal_reports_held_buffer() { + clear_held_clears_both && + in_order '^ local in_terminal = M\.is_claude_terminal_buffer\(current_buf\)$' \ + '^ if read\.bufnr ~= current_buf and not in_terminal then$' '^ return false$' \ + '^ local from_terminal = read\.bufnr ~= current_buf and not M\.is_claude_terminal_buffer\(read\.bufnr\)$' \ + '^ local cursor = from_terminal and cursor_in_other_buffer\(read\.bufnr\)$' '^ clear_held_state\(\)$' '^ if cursor then$' \ + '^ M\.state\.latest_selection = cursor$' '^ M\.send_selection_update\(cursor\)$' <<<"$demote_text" +} +fact[TerminalReportsHeldBuffer]=$(as_bool terminal_reports_held_buffer) +# update_selection in the Claude terminal also runs that check: a new terminal is not registered when BufEnter fires. +update_checks_held_text() { + in_order '^ M\._cancel_demotion_timer\(\)$' '^ demote_if_selection_text_changed\(\)$' <<<"$update_selection" +} +fact[UpdateChecksHeldText]=$(as_bool update_checks_held_text) +# Entering visual mode in a buffer that is not the Claude terminal listens to it, and the listener's on_lines counts an edit +# on the visual_entry of that buffer: visual_entry_of finds it, note_visual_edit adds one to unchecked_edits. +listener_notes_visual_edit() { + in_order '^ if entering_visual then$' '^ if not M\.is_claude_terminal_buffer\(buf\) then$' '^ watch_selection_buffer\(buf\)$' \ + '^ elseif leaving_visual then$' <<<"$on_mode_changed" && + in_order '^ local entry = M\.state\.visual_entry$' '^ return entry and entry\.bufnr == bufnr and entry or nil$' <<<"$entry_of" && + in_order '^ on_lines = function\(_, buf\)$' '^ local entry = visual_entry_of\(buf\)$' '^ if entry then$' \ + '^ note_visual_edit\(entry\)$' '^ on_reload = function\(_, buf\)$' <<<"$watch_buffer" && + in_order '^ entry\.unchecked_edits = entry\.unchecked_edits \+ 1$' <<<"$note_edit" +} +fact[ListenerNotesVisualEdit]=$(as_bool listener_notes_visual_edit) +# note_visual_edit schedules a check that takes the edit back and marks the entry consumed only when visual mode is over: +# a plugin's edit leaves the selection on the screen and does not consume it. +visual_check_spares_plugin_edit() { + in_order '^ vim\.schedule\(function\(\)$' '^ entry\.unchecked_edits = entry\.unchecked_edits - 1$' \ + '^ if not is_visual_mode\(vim\.api\.nvim_get_mode\(\)\.mode\) then$' '^ entry\.consumed = true$' <<<"$note_edit" +} +fact[VisualCheckSparesPluginEdit]=$(as_bool visual_check_spares_plugin_edit) +# Neither on_mode_changed nor the flush reads a changedtick (comments apart). The code before #524 compared the changedtick +# with the one it recorded at visual entry, which took a plugin's edit or a :write for an operator. +flush_ignores_tick() { + ! awk '!/^ *--/ && /changedtick/ { found = 1 } END { exit !found }' <<<"$on_mode_changed"$'\n'"$flush" +} +fact[FlushIgnoresTick]=$(as_bool flush_ignores_tick) + +RULES=(ReleaseSent NoPhantomSelection NoTerminalSelection HeldUntilMoved HeldInTerminal HeldEndsWhenMoved SameFile ClaudeSeesCursor + NoDeletedText TimerClosedOnce) +LIVE=() +# Five guards break no rule alone, because another guard in the code covers for them. EXPECT lists each with a guard +# that covers for it (a "+" key sets both FALSE) and the rule that breaks when both go. +EXPECT=( + [FlushOnVisualExit]=ReleaseSent [FlushSkipsOperator]=NoPhantomSelection + [FlushSkipsTerminal]=NoTerminalSelection [UpdateSkipsTerminal]=NoTerminalSelection + [FlushRecordsCursor]=HeldUntilMoved [PendingKeepsHeld]=HeldUntilMoved [DemotionWaitsForMove]=HeldUntilMoved + [DebounceIgnoresStale]=TimerClosedOnce [DemotionIgnoresStale]=TimerClosedOnce [ClearsBeforeClose]=TimerClosedOnce + [ReadRecordsTick]=NoDeletedText [TextChangeReports]=NoDeletedText + [ListensToSelectionBuffer]=NoDeletedText [TerminalReportsHeldBuffer]=NoDeletedText + [UpdateChecksHeldText]=NoDeletedText + [ListenerNotesVisualEdit]=NoPhantomSelection [VisualCheckSparesPluginEdit]=ReleaseSent [FlushIgnoresTick]=ReleaseSent + [ReconcileOnTextChanged]=NoDeletedText [ReconcileOnCursorMoved]=HeldEndsWhenMoved [MoveReports]=HeldEndsWhenMoved + [LeaveNoted]=HeldEndsWhenMoved + ["DemotionClearsHeldState+MoveReports"]=ClaudeSeesCursor + ["PendingClearsHeld+ReconcileOnCursorMoved"]=ClaudeSeesCursor + ["ElseClearsHeldState+LeaveNoted"]=SameFile + ["EntryClearsHeld+FlushSkipReports"]=HeldEndsWhenMoved +) + +# The main run explores any visual_demotion_delay_ms with two files. Three rules need a second file in their mutant runs: +# SameFile, HeldEndsWhenMoved (LeaveNoted breaks it only when the user can visit another file), and NoDeletedText +# (UpdateChecksHeldText breaks it only when a file changes while the user is in another file). +# DelayBelowDebounce stays FALSE: TRUE would drop every order in which a demotion timer fires after a later debounce. +tla_constants() { + local rule=${1##*-} files="f1" + [[ $1 != main && $rule != SameFile && $rule != HeldEndsWhenMoved && $rule != NoDeletedText ]] || files="f1, f2" + echo " Files = {$files}" + echo " Term = term" + echo " Pos = {p1, p2}" + echo " Ranges = {r1, r2}" + echo " None = none" + echo " MaxEdits = 1" + echo " DelayBelowDebounce = FALSE" + echo " WithTerminal = TRUE" +} +tla_main diff --git a/.agents/skills/verify-selection-tracking/covered.lock b/.agents/skills/verify-selection-tracking/covered.lock new file mode 100644 index 000000000..29c192c7b --- /dev/null +++ b/.agents/skills/verify-selection-tracking/covered.lock @@ -0,0 +1,175 @@ +== lua/claudecode/init.lua +file lua/claudecode/init.lua fc28de832b4056df +block start 7bf331d94d09a034 +block stop d754def6d5865650 +site lua/claudecode/init.lua: selection.disable() @ function M.stop() +site lua/claudecode/init.lua: selection.enable(M.state.server, M.state.config.visual_demotion_delay_ms) @ function M.start(show_startup_notification) +== lua/claudecode/selection.lua +file lua/claudecode/selection.lua 349b9bb73c6f64c5 +block unmoved f1a214d2c667190d +block clear_held d64cb396d2cab01b +block text_there 1b8ae5bb0f3cf2bc +block cursor_other a3f70cc27b68d423 +block demote_text 0668ccc9dd4a9b5f +block holds_selection edc9a9c85c5d4ba0 +block entry_of 0753ce446f57ebfd +block note_edit 4fdbc33b47229b1d +block watch_buffer b2d4b61899558e19 +block record_read b0556eae55637f45 +block reconcile bc1c8b3e222be191 +block enable 4493c0b8788e2324 +block disable 83c1fbe87e1dca74 +block cancel_debounce 592a0a27d18d8087 +block cancel_demotion a9ce6b7f0a3f9fa4 +block autocmds 4590b41712d7f2c6 +block on_cursor_moved 1d59e87e56f0e0de +block on_mode_changed 57750d820b55e948 +block on_text_changed 3cb267a861b8736a +block debounce_update 7749d9d18b3de96c +block update_selection 534fe77bf7eaafab +block demotion 9688100d85cb04c4 +block from_marks 0a6ab596f29cc854 +block flush 38f80398900e8afd +block changed c5a25cb2e7e9c27f +block send_update d001653f2e4d8c80 +block get_latest 786c00231c530411 +block is_terminal 4e2b519f765955d2 +site lua/claudecode/selection.lua: M._cancel_debounce_timer() @ function M.debounce_update() +site lua/claudecode/selection.lua: M._cancel_debounce_timer() @ function M.disable() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ function M.disable() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ function M.update_selection() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ function M.update_selection() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: M._cancel_demotion_timer() @ local function reconcile_held_selection(compare_cursor) +site lua/claudecode/selection.lua: M.flush_visual_selection() @ function M.on_mode_changed() +site lua/claudecode/selection.lua: M.handle_selection_demotion(current_buf) -- Pass buffer at time of scheduling @ function M.update_selection() +site lua/claudecode/selection.lua: M.send_selection_update(M.state.latest_selection) @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.send_selection_update(current_selection) @ function M.update_selection() +site lua/claudecode/selection.lua: M.send_selection_update(cursor) @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: M.send_selection_update(selection) @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M.send_selection_update(selection) @ function M.send_current_selection() +site lua/claudecode/selection.lua: M.server.broadcast("selection_changed", selection) @ function M.send_selection_update(selection) +site lua/claudecode/selection.lua: M.state.cursor_at_flush = nil @ function M.disable() +site lua/claudecode/selection.lua: M.state.cursor_at_flush = nil @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.cursor_at_flush = nil @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.cursor_at_flush = nil @ local function clear_held_state() +site lua/claudecode/selection.lua: M.state.cursor_at_flush = { bufnr = current_buf, pos = vim.api.nvim_win_get_cursor(0) } @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M.state.debounce_timer = nil @ function M._cancel_debounce_timer() +site lua/claudecode/selection.lua: M.state.debounce_timer = nil @ function M.debounce_update() +site lua/claudecode/selection.lua: M.state.debounce_timer = timer @ function M.debounce_update() +site lua/claudecode/selection.lua: M.state.demotion_timer = nil @ function M._cancel_demotion_timer() +site lua/claudecode/selection.lua: M.state.demotion_timer = nil @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.demotion_timer = timer @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.disable() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = nil @ local function clear_held_state() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = { @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection = { @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.last_active_visual_selection @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.last_active_visual_selection @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.last_active_visual_selection @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.latest_selection = current_selection @ function M.update_selection() +site lua/claudecode/selection.lua: M.state.latest_selection = cursor @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: M.state.latest_selection = new_sel_for_demotion @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: M.state.latest_selection = nil @ function M.disable() +site lua/claudecode/selection.lua: M.state.latest_selection = selection @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M.state.selection_tick = nil @ function M.disable() +site lua/claudecode/selection.lua: M.state.selection_tick = nil @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: M.state.selection_tick = { bufnr = bufnr, tick = vim.api.nvim_buf_get_changedtick(bufnr) } @ local function record_selection_read(bufnr) +site lua/claudecode/selection.lua: M.state.visual_entry = nil @ function M.disable() +site lua/claudecode/selection.lua: M.state.visual_entry = nil @ function M.on_mode_changed() +site lua/claudecode/selection.lua: M.state.visual_entry = { bufnr = buf, consumed = false, unchecked_edits = 0 } @ function M.on_mode_changed() +site lua/claudecode/selection.lua: M.state.watched_buffers[buf] = nil @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: M.state.watched_buffers[buf] = nil @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: M.state.watched_buffers[bufnr] = true @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: M.update_selection() @ function M.debounce_update() +site lua/claudecode/selection.lua: M.update_selection() @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: M.update_selection() @ function M.send_current_selection() +site lua/claudecode/selection.lua: M.update_selection() @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: M.update_selection() @ local function reconcile_held_selection(compare_cursor) +site lua/claudecode/selection.lua: and M.state.last_active_visual_selection.bufnr == original_bufnr_when_scheduled @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: and M.state.last_active_visual_selection.bufnr == original_bufnr_when_scheduled @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: and M.state.last_active_visual_selection.bufnr == original_bufnr_when_scheduled @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: clear_held_state() @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: clear_held_state() @ function M.on_mode_changed() +site lua/claudecode/selection.lua: clear_held_state() @ function M.update_selection() +site lua/claudecode/selection.lua: clear_held_state() @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: clear_held_state() @ local function reconcile_held_selection(compare_cursor) +site lua/claudecode/selection.lua: current_selection = M.state.latest_selection @ function M.update_selection() +site lua/claudecode/selection.lua: current_selection = M.state.latest_selection @ function M.update_selection() +site lua/claudecode/selection.lua: cursor_at_flush = nil, @ M.state = { +site lua/claudecode/selection.lua: debounce_timer = nil, @ M.state = { +site lua/claudecode/selection.lua: demotion_timer = nil, @ M.state = { +site lua/claudecode/selection.lua: function M._cancel_debounce_timer() @ function M._cancel_debounce_timer() +site lua/claudecode/selection.lua: function M._cancel_demotion_timer() @ function M._cancel_demotion_timer() +site lua/claudecode/selection.lua: function M.flush_visual_selection() @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: function M.get_latest_selection() @ function M.get_latest_selection() +site lua/claudecode/selection.lua: function M.handle_selection_demotion(original_bufnr_when_scheduled) @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: function M.has_selection_changed(new_selection) @ function M.has_selection_changed(new_selection) +site lua/claudecode/selection.lua: function M.send_selection_update(selection) @ function M.send_selection_update(selection) +site lua/claudecode/selection.lua: function M.update_selection() @ function M.update_selection() +site lua/claudecode/selection.lua: if M.has_selection_changed(cursor) then @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: if M.has_selection_changed(new_sel_for_demotion) then @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: if M.has_selection_changed(selection) then @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: if M.state.cursor_at_flush and M.state.cursor_at_flush.bufnr == original_bufnr_when_scheduled then @ function M.handle_selection_demotion(original_bufnr_when_scheduled) +site lua/claudecode/selection.lua: if M.state.debounce_timer ~= timer then @ function M.debounce_update() +site lua/claudecode/selection.lua: if M.state.demotion_timer then @ function M.update_selection() +site lua/claudecode/selection.lua: if M.state.demotion_timer ~= timer then @ function M.update_selection() +site lua/claudecode/selection.lua: if M.state.last_active_visual_selection and M.state.last_active_visual_selection.bufnr == current_buf then @ function M.update_selection() +site lua/claudecode/selection.lua: if M.state.visual_entry ~= entry then @ local function note_visual_edit(entry) +site lua/claudecode/selection.lua: if M.state.watched_buffers[bufnr] then @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: last_active_visual_selection = nil, @ M.state = { +site lua/claudecode/selection.lua: latest_selection = nil, @ M.state = { +site lua/claudecode/selection.lua: local caf = M.state.cursor_at_flush @ local function cursor_in_other_buffer(bufnr) +site lua/claudecode/selection.lua: local caf = M.state.cursor_at_flush @ local function cursor_unmoved_since_flush(bufnr) +site lua/claudecode/selection.lua: local caf = M.state.cursor_at_flush @ local function reconcile_held_selection(compare_cursor) +site lua/claudecode/selection.lua: local changed = M.has_selection_changed(current_selection) @ function M.update_selection() +site lua/claudecode/selection.lua: local entry = M.state.visual_entry @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: local entry = M.state.visual_entry @ local function visual_entry_of(bufnr) +site lua/claudecode/selection.lua: local entry = visual_entry_of(buf) @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: local entry = visual_entry_of(buf) @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: local entry = visual_entry_of(buf) @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: local function clear_held_state() @ local function clear_held_state() +site lua/claudecode/selection.lua: local function reconcile_held_selection(compare_cursor) @ local function reconcile_held_selection(compare_cursor) +site lua/claudecode/selection.lua: local function record_selection_read(bufnr) @ local function record_selection_read(bufnr) +site lua/claudecode/selection.lua: local function visual_entry_of(bufnr) @ local function visual_entry_of(bufnr) +site lua/claudecode/selection.lua: local function watch_selection_buffer(bufnr) @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: local held = M.state.latest_selection @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: local held = M.state.latest_selection @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: local held = M.state.latest_selection @ local function holds_selection_of(bufnr) +site lua/claudecode/selection.lua: local last_visual = M.state.last_active_visual_selection @ function M.update_selection() +site lua/claudecode/selection.lua: local old_selection = M.state.latest_selection @ function M.has_selection_changed(new_selection) +site lua/claudecode/selection.lua: local read = M.state.selection_tick @ local function demote_if_selection_text_changed() +site lua/claudecode/selection.lua: local read = M.state.selection_tick @ local function holds_selection_of(bufnr) +site lua/claudecode/selection.lua: local selection = M.state.latest_selection @ function M.send_current_selection() +site lua/claudecode/selection.lua: local timer = M.state.debounce_timer @ function M._cancel_debounce_timer() +site lua/claudecode/selection.lua: local timer = M.state.demotion_timer @ function M._cancel_demotion_timer() +site lua/claudecode/selection.lua: reconcile_held_selection(not entered_buffer) @ function M.on_cursor_moved(entered_buffer) +site lua/claudecode/selection.lua: reconcile_held_selection(true) @ function M.on_text_changed() +site lua/claudecode/selection.lua: record_selection_read(current_buf) @ function M.flush_visual_selection() +site lua/claudecode/selection.lua: record_selection_read(current_buf) @ function M.update_selection() +site lua/claudecode/selection.lua: return M.state.latest_selection @ function M.get_latest_selection() +site lua/claudecode/selection.lua: sel_to_send = M.state.latest_selection @ function M.send_at_mention_for_visual_selection(line1, line2) +site lua/claudecode/selection.lua: selection_tick = nil, @ M.state = { +site lua/claudecode/selection.lua: visual_entry = nil, @ M.state = { +site lua/claudecode/selection.lua: watch_selection_buffer(buf) @ function M.on_mode_changed() +site lua/claudecode/selection.lua: watch_selection_buffer(buf) @ local function watch_selection_buffer(bufnr) +site lua/claudecode/selection.lua: watch_selection_buffer(bufnr) @ local function record_selection_read(bufnr) +site lua/claudecode/selection.lua: watched_buffers = {}, @ M.state = { +== lua/claudecode/server/init.lua +file lua/claudecode/server/init.lua 8da8851fff781946 +block broadcast fc69234ae8ed7cf0 +block on_connect daf282e2fe8f3c9a +== lua/claudecode/tools/get_current_selection.lua +file lua/claudecode/tools/get_current_selection.lua 5fb9ade5d26239ae +block current_tool 7d8f6acd15d97423 +site lua/claudecode/tools/get_current_selection.lua: local selection = selection_module.get_latest_selection() @ local function handler(params) +== lua/claudecode/tools/get_latest_selection.lua +file lua/claudecode/tools/get_latest_selection.lua ca8dfa01572dc62b +block latest_tool 5f86f1f5efadf5e6 +site lua/claudecode/tools/get_latest_selection.lua: local selection = selection_module.get_latest_selection() @ local function handler(params) diff --git a/.agents/skills/verify-selection-tracking/model/SelectionTracking.tla b/.agents/skills/verify-selection-tracking/model/SelectionTracking.tla new file mode 100644 index 000000000..73fcbb2b0 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/model/SelectionTracking.tla @@ -0,0 +1,652 @@ +------------------------- MODULE SelectionTracking ------------------------- +(***************************************************************************) +(* What Claude sees as the user's current selection in claudecode.nvim. *) +(* *) +(* lua/claudecode/selection.lua pushes the selection to Claude as a *) +(* selection_changed notification, and getCurrentSelection and *) +(* getLatestSelection return the same value, M.state.latest_selection. *) +(* Each send sets latest_selection first, so in this model `latest` is what *) +(* a connected Claude holds. *) +(* *) +(* The user moves, selects, edits and switches buffers. Autocmds run a *) +(* synchronous flush on visual exit and restart a 100 ms debounce timer; *) +(* the debounced update can start a demotion timer. Both are one-shot uv *) +(* timers whose callback goes through vim.schedule, so a timer can fire, *) +(* queue its callback, and be cancelled before the callback runs. The *) +(* listener on the buffer of a held selection queues its check the same way.*) +(* *) +(* One user step is one key (or command) with the autocmds it fires: *) +(* ModeChanged, TextChanged, CursorMoved and BufEnter run in the same main- *) +(* loop iteration as the key, before Neovim polls libuv again, so no timer *) +(* or scheduled callback can run between them. Each uv timer firing and *) +(* each scheduled callback is its own step. The model has no clock: a timer *) +(* can fire after any number of user steps, which covers every value of *) +(* visual_demotion_delay_ms (DelayBelowDebounce = TRUE adds the default *) +(* 50 ms < 100 ms order). *) +(* *) +(* Code facts (BOOLEAN constants) are read from the source by check.sh: *) +(* TRUE means the guard is in the code, FALSE models the code without it. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Files, \* file buffers (model values) + Term, \* the Claude terminal buffer (terminal.get_active_terminal_bufnr) + Pos, \* cursor positions + Ranges, \* visual selection ranges + None, \* nil (model value) + MaxEdits, \* edits per file buffer that change the text a selection can hold (YouEditSelection, YouEditAtCursor, + \* YouEditByPlugin, YouEditOtherBuffer). Each one also moves the buffer's changedtick + DelayBelowDebounce, \* environment: visual_demotion_delay_ms < debounce_ms, so a + \* demotion timer always fires before a later debounce timer + WithTerminal, \* environment: a Claude terminal buffer exists in Neovim (FALSE: terminal.provider + \* "none" or "external", Claude runs elsewhere) + + \* Code facts, see check.sh for the source lines each one reads. + FlushOnVisualExit, \* on_mode_changed calls flush_visual_selection when visual mode ends + FlushSkipsOperator, \* on_mode_changed records visual_entry; the flush returns when the entry has an edit that the + \* listener counted (an operator such as d consumed the selection) + FlushSkipsTerminal, \* flush_visual_selection returns in the Claude terminal buffer + FlushRecordsCursor, \* flush_visual_selection sets cursor_at_flush + UpdateSkipsTerminal, \* update_selection returns in the Claude terminal buffer + PendingKeepsHeld, \* update_selection keeps latest_selection while a demotion is + \* pending and the cursor stands where the flush left it + ElseClearsHeldState, \* update_selection's cursor branch clears last_active_visual_selection + \* and cursor_at_flush + DemotionWaitsForMove, \* handle_selection_demotion returns while the cursor is unmoved + DemotionClearsHeldState, \* handle_selection_demotion clears the original buffer's + \* last_active_visual_selection and cursor_at_flush + DebounceIgnoresStale, \* the debounce callback returns unless it is M.state.debounce_timer + DemotionIgnoresStale, \* the demotion callback returns unless it is M.state.demotion_timer + ClearsBeforeClose, \* both cancel functions and both callbacks set the state field to + \* nil before timer:close() + EntryClearsHeld, \* on_mode_changed clears the held state when visual mode starts, except in the + \* Claude terminal + FlushSkipReports, \* a flush skipped for an operator clears the held state and, when Claude holds a + \* selection, reports the cursor at once + PendingClearsHeld, \* update_selection's pending-demotion branch clears the held state when it + \* reports the cursor + ReconcileOnCursorMoved, \* on_cursor_moved calls reconcile_held_selection, and the BufEnter autocmd tells + \* it that the window cursor is not restored yet + ReconcileOnTextChanged, \* on_text_changed calls reconcile_held_selection + TextChangeReports, \* reconcile reports the cursor when the text of the held selection changed + MoveReports, \* reconcile reports the cursor when it left the flushed position + LeaveNoted, \* reconcile notes another buffer entered (away) and ends the hold for one that is + \* not the Claude terminal (left) + ReadRecordsTick, \* the flush and the in-visual update record selection_tick + ListensToSelectionBuffer, \* record_selection_read listens to the buffer of the selection it read, and a change of + \* that buffer schedules the check + TerminalReportsHeldBuffer, \* the check, in the Claude terminal, sends the cursor of the selection's buffer when the + \* held text changed + UpdateChecksHeldText, \* update_selection runs that check in the Claude terminal too + ListenerNotesVisualEdit, \* entering visual mode listens to the buffer, and an edit of it counts on the visual_entry + \* (note_visual_edit) + VisualCheckSparesPluginEdit, \* the check that note_visual_edit schedules marks the entry consumed only when visual mode + \* has ended, so a plugin's edit that leaves the selection on the screen does not + FlushIgnoresTick \* neither on_mode_changed nor the flush reads a changedtick. FALSE models the code before #524, whose + \* flush returned when the changedtick moved since visual mode started + +Bufs == Files \cup {Term} +Modes == {"n", "v"} \* "n" is every mode without a selection (normal, insert, terminal) + +\* A selection value as has_selection_changed compares it: buffer (filePath), range or cursor +\* (start/end), and text. A visual selection's text is the text of its range at buffer version ver. +Vis(b, r, k) == [kind |-> "vis", buf |-> b, at |-> r, ver |-> k] +Cur(b, p) == [kind |-> "cur", buf |-> b, at |-> p, ver |-> 0] +VisValues == {Vis(b, r, k) : b \in Bufs, r \in Ranges, k \in 0..MaxEdits} +CurValues == {Cur(b, p) : b \in Bufs, p \in Pos} +Values == VisValues \cup CurValues + +\* A timer field of M.state: nil, a running uv timer, a timer that fired and whose +\* vim.schedule'd callback waits, or (only without ClearsBeforeClose) a closed handle that +\* the field still holds, with or without a queued callback. +TStates == {"nil", "armed", "queued", "closed", "closedQueued"} +Alive == {"armed", "queued"} + +P0 == CHOOSE p \in Pos : TRUE + +VARIABLES + \* Neovim + buf, \* the current buffer + mode, \* "v" in Visual or Select mode + cur, \* the window cursor + vsel, \* the live visual range, None outside visual mode + ver, \* per buffer: the version of the text that a selection can hold. An edit of the selected text advances it, + \* a :write or an edit of another line does not (both move the changedtick all the same) + \* selection.lua M.state + latest, \* latest_selection: what Claude holds + lastVis, \* last_active_visual_selection.bufnr, or None + cafBuf, \* cursor_at_flush.bufnr, or None + cafPos, \* cursor_at_flush.pos + cafLeft, \* cursor_at_flush.left: the cursor left the flushed position or buffer, noted when it happened + cafAway, \* cursor_at_flush.away: a buffer entered since, not yet known to be the Claude terminal, or None + rdBuf, \* selection_tick.bufnr, or None + rdVer, \* selection_tick.tick (as a text version) + entryBuf, \* visual_entry.bufnr, or None + entryDirty, \* visual_entry.consumed or visual_entry.unchecked_edits > 0: the listener counted an edit since visual mode started + entryMoved, \* the changedtick of that buffer moved since visual mode started: any edit, or a :write. The code before #524 + \* compared the tick with the one recorded then. A tick only grows, so this bit is all the comparison reads + db, \* debounce_timer + dbStale, \* a callback of a cancelled debounce timer waits in the schedule queue + dbLoose, \* (only without DebounceIgnoresStale) a live debounce timer that the state lost + dm, \* demotion_timer + dmBuf, \* the buffer the demotion callback was scheduled for (current_buf) + dmStale, \* a callback of a cancelled demotion timer waits in the schedule queue + dmLoose, \* (only without DemotionIgnoresStale) buffers of live demotion timers the state lost + chk, \* check_soon of the listener on the buffer of the held selection: its callback waits in the schedule queue + \* ghosts + phantom, \* Claude was sent text at the '<,'> marks that an edit changed after the selection + closedTwice,\* timer:close() ran on a closed handle: Lua error "handle ... is already closing" + hold, \* the selection the user released with Esc, until the cursor moves; or None + holdPos, \* the cursor when it was released + holdLoose, \* the user came back from the Claude terminal to it: either outcome is allowed + released \* the last step was the release itself + +nvim == <> +plugin == <> +spec == <> +vars == <> + +TypeOK == + /\ buf \in Bufs /\ mode \in Modes /\ cur \in Pos + /\ vsel \in Ranges \cup {None} /\ (mode = "v") = (vsel # None) + /\ ver \in [Bufs -> 0..MaxEdits] /\ ver[Term] = 0 + /\ latest \in Values \cup {None} + /\ lastVis \in Bufs \cup {None} + /\ cafBuf \in Bufs \cup {None} /\ cafPos \in Pos /\ cafLeft \in BOOLEAN /\ cafAway \in Bufs \cup {None} + /\ rdBuf \in Bufs \cup {None} /\ rdVer \in 0..MaxEdits + /\ entryBuf \in Bufs \cup {None} /\ entryDirty \in BOOLEAN /\ entryMoved \in BOOLEAN + /\ db \in TStates /\ dbStale \in BOOLEAN /\ dbLoose \in BOOLEAN + /\ dm \in TStates /\ dmBuf \in Bufs \cup {None} /\ (dm = "nil") = (dmBuf = None) + /\ dmStale \in BOOLEAN /\ dmLoose \subseteq Bufs /\ chk \in BOOLEAN + /\ phantom \in BOOLEAN /\ closedTwice \in BOOLEAN + /\ hold \in VisValues \cup {None} /\ holdPos \in Pos /\ holdLoose \in BOOLEAN /\ released \in BOOLEAN + +Init == + /\ buf = CHOOSE f \in Files : TRUE + /\ mode = "n" /\ cur = P0 /\ vsel = None + /\ ver = [b \in Bufs |-> 0] + /\ latest = None /\ lastVis = None /\ cafBuf = None /\ cafPos = P0 /\ cafLeft = FALSE /\ cafAway = None /\ rdBuf = None /\ rdVer = 0 /\ entryBuf = None /\ entryDirty = FALSE /\ entryMoved = FALSE + /\ db = "nil" /\ dbStale = FALSE /\ dbLoose = FALSE + /\ dm = "nil" /\ dmBuf = None /\ dmStale = FALSE /\ dmLoose = {} /\ chk = FALSE + /\ phantom = FALSE /\ closedTwice = FALSE + /\ hold = None /\ holdPos = P0 /\ holdLoose = FALSE /\ released = FALSE + +----------------------------------------------------------------------------- +(* The plugin's state as a record, so that the code's functions chain as *) +(* operators over it. E is the Neovim state the code reads (after the key). *) + +S == [latest |-> latest, lastVis |-> lastVis, cafBuf |-> cafBuf, cafPos |-> cafPos, cafLeft |-> cafLeft, cafAway |-> cafAway, rdBuf |-> rdBuf, rdVer |-> rdVer, entryBuf |-> entryBuf, + entryDirty |-> entryDirty, entryMoved |-> entryMoved, db |-> db, dbStale |-> dbStale, dbLoose |-> dbLoose, dm |-> dm, dmBuf |-> dmBuf, + dmStale |-> dmStale, dmLoose |-> dmLoose, chk |-> chk, phantom |-> phantom, closedTwice |-> closedTwice] + +SetS(s) == + /\ latest' = s.latest /\ lastVis' = s.lastVis /\ cafBuf' = s.cafBuf + /\ cafPos' = IF s.cafBuf = None THEN P0 ELSE s.cafPos + /\ cafLeft' = IF s.cafBuf = None THEN FALSE ELSE s.cafLeft + /\ cafAway' = IF s.cafBuf = None THEN None ELSE s.cafAway + /\ rdBuf' = s.rdBuf /\ rdVer' = IF s.rdBuf = None THEN 0 ELSE s.rdVer + /\ entryBuf' = s.entryBuf + /\ entryDirty' = (s.entryBuf # None /\ FlushSkipsOperator /\ s.entryDirty) \* kept only while a guard reads it + /\ entryMoved' = (s.entryBuf # None /\ ~FlushIgnoresTick /\ s.entryMoved) + /\ db' = s.db /\ dbStale' = s.dbStale /\ dbLoose' = s.dbLoose + /\ dm' = s.dm /\ dmBuf' = IF s.dm = "nil" THEN None ELSE s.dmBuf + /\ dmStale' = s.dmStale /\ dmLoose' = s.dmLoose /\ chk' = s.chk + /\ phantom' = s.phantom /\ closedTwice' = s.closedTwice + +\* marks: the '<,'> marks that ending visual mode just set: the range and the buffer +\* version it was selected at. The flush reads them in the same step, so no state keeps them. +E == [buf |-> buf, mode |-> mode, cur |-> cur, vsel |-> vsel, marks |-> None, ver |-> ver] + +\* has_selection_changed, then the send: latest_selection = sel; M.server.broadcast(...). +Publish(s, sel) == IF sel = s.latest THEN s ELSE [s EXCEPT !.latest = sel] + +\* cursor_unmoved_since_flush(bufnr) +Unmoved(s, e) == s.cafBuf = e.buf /\ s.cafPos = e.cur /\ ~s.cafLeft + +\* clear_held_state() +ClearHeld(s) == [s EXCEPT !.lastVis = None, !.cafBuf = None] + +\* demote_if_selection_text_changed: the visual text in latest_selection was read in a buffer at another text version +\* than it has now. TextChanged is the check for the buffer you are in, HeldTextGone the check for the buffer of the +\* selection, whichever it is. +HeldTextGone(s, e) == s.rdBuf \in Bufs /\ s.latest \in VisValues /\ s.rdVer # e.ver[s.rdBuf] +TextChanged(s, e) == s.rdBuf = e.buf /\ HeldTextGone(s, e) + +\* In the Claude terminal, which keeps a held selection of another buffer and does not update it, the check sends the +\* cursor of the selection's buffer: where its window has the cursor, else where the selection was released. +TerminalChanged(s, e) == e.buf = Term /\ s.rdBuf \in Files /\ HeldTextGone(s, e) +ReportHeldBuffer(s) == Publish(ClearHeld(s), Cur(s.rdBuf, IF s.cafBuf = s.rdBuf THEN s.cafPos ELSE P0)) + +\* timer:stop(); timer:close() on the handle in state t. Closing a closed handle is an error. +CloseErr(t) == t \in {"closed", "closedQueued"} + +\* _cancel_debounce_timer / _cancel_demotion_timer. Clearing the field first turns a queued +\* callback into a stale one. Without it the field keeps the closed handle. +Cancelled(t) == + CASE t = "nil" -> "nil" + [] ClearsBeforeClose -> "nil" + [] t \in {"armed", "closed"} -> "closed" + [] OTHER -> "closedQueued" +NowStale(t) == ClearsBeforeClose /\ t \in {"queued", "closedQueued"} + +CancelDebounce(s) == + [s EXCEPT !.db = Cancelled(s.db), !.dbStale = @ \/ NowStale(s.db), !.closedTwice = @ \/ CloseErr(s.db)] + +CancelDemotion(s) == + [s EXCEPT !.dm = Cancelled(s.dm), !.dmStale = @ \/ NowStale(s.dm), !.closedTwice = @ \/ CloseErr(s.dm), + !.dmBuf = IF Cancelled(s.dm) = "nil" THEN None ELSE @] + +(* selection.lua debounce_update: cancel, then a new timer. A queued callback of the old *) +(* handle no longer matches M.state.debounce_timer, so it is stale. *) +DebounceUpdate(s) == + LET c == CancelDebounce(s) + IN [c EXCEPT !.db = "armed", !.dbStale = @ \/ c.db = "closedQueued"] + +(* selection.lua update_selection. *) +Update(s, e) == + LET here == e.buf + orCursor(sel) == IF sel = None THEN Cur(here, e.cur) ELSE sel + IN + CASE here = Term /\ UpdateSkipsTerminal -> + IF UpdateChecksHeldText /\ TerminalReportsHeldBuffer /\ TerminalChanged(s, e) + THEN ReportHeldBuffer(CancelDemotion(s)) + ELSE CancelDemotion(s) + [] e.mode = "v" -> + Publish([CancelDemotion(s) EXCEPT !.lastVis = here, !.rdBuf = IF ReadRecordsTick THEN here ELSE @, + !.rdVer = IF ReadRecordsTick THEN e.ver[here] ELSE @], + Vis(here, e.vsel, e.ver[here])) + [] s.dm # "nil" -> \* `if M.state.demotion_timer then`: a pending demotion + IF PendingKeepsHeld /\ Unmoved(s, e) + THEN Publish(s, orCursor(s.latest)) + ELSE Publish(IF PendingClearsHeld THEN ClearHeld(s) ELSE s, orCursor(Cur(here, e.cur))) + [] s.lastVis = here -> \* just left visual mode here: keep it, start the demotion timer + Publish([s EXCEPT !.dm = "armed", !.dmBuf = here], orCursor(s.latest)) + [] OTHER -> + Publish([s EXCEPT !.lastVis = IF ElseClearsHeldState THEN None ELSE @, + !.cafBuf = IF ElseClearsHeldState THEN None ELSE @], Cur(here, e.cur)) + +(* selection.lua handle_selection_demotion(original_bufnr_when_scheduled). *) +Demote(s, e, b) == + LET clearVis(x) == [x EXCEPT !.lastVis = IF @ = b THEN None ELSE @] + resolved(x) == IF DemotionClearsHeldState + THEN [clearVis(x) EXCEPT !.cafBuf = IF @ = b THEN None ELSE @] + ELSE x + IN + CASE e.buf = Term -> clearVis(s) \* Condition 1 + [] e.buf = b /\ e.mode = "v" -> clearVis(s) \* Condition 2 + [] e.buf = b /\ DemotionWaitsForMove /\ Unmoved(s, e) -> s \* Condition 3, cursor unmoved + [] e.buf = b -> resolved(Publish(s, Cur(b, e.cur))) \* Condition 3, demote + [] OTHER -> resolved(s) \* another buffer + +(* selection.lua flush_visual_selection, right after visual mode ended. *) +Flush(s, e) == + LET here == e.buf + sel == Vis(here, e.marks.at, e.ver[here]) \* get_visual_selection_from_marks: the text there now + rec == [s EXCEPT !.cafBuf = IF FlushRecordsCursor THEN here ELSE @, + !.cafPos = IF FlushRecordsCursor THEN e.cur ELSE @, + !.cafLeft = FALSE, !.cafAway = None, + !.rdBuf = IF ReadRecordsTick THEN here ELSE @, + !.rdVer = IF ReadRecordsTick THEN e.ver[here] ELSE @, + !.lastVis = here, + !.phantom = @ \/ (sel # s.latest /\ e.marks.ver # e.ver[here])] + IN + CASE here = Term /\ FlushSkipsTerminal -> s + [] s.entryBuf = here /\ ((FlushSkipsOperator /\ s.entryDirty) \/ (~FlushIgnoresTick /\ s.entryMoved)) -> + IF ~FlushSkipReports THEN s + ELSE IF s.latest \in VisValues THEN Update(ClearHeld(s), e) + ELSE ClearHeld(s) + [] OTHER -> Publish(CancelDemotion(rec), sel) + +(* selection.lua on_mode_changed, then the debounce. Entering visual mode makes the visual_entry, leaving it flushes and *) +(* then forgets the entry. *) +OnModeChanged(s, e, entering, leaving) == + LET entered == [s EXCEPT !.entryBuf = e.buf, !.entryDirty = FALSE, !.entryMoved = FALSE] + left == IF FlushOnVisualExit THEN Flush(s, e) ELSE s + s1 == CASE entering -> IF e.buf = Term \/ ~EntryClearsHeld THEN entered ELSE ClearHeld(entered) + [] leaving -> [left EXCEPT !.entryBuf = None] + [] OTHER -> s + IN DebounceUpdate(s1) + +E2(b, m, c, v, mk, vr) == [buf |-> b, mode |-> m, cur |-> c, vsel |-> v, marks |-> mk, ver |-> vr] + +\* The changedtick of buffer b moved: an edit, or a :write. The visual_entry of b notes that it moved. +TickMoved(s, b) == IF s.entryBuf = b THEN [s EXCEPT !.entryMoved = TRUE] ELSE s + +\* An edit of buffer b reaches the listener (on_lines): note_visual_edit counts it on the visual_entry of b. +EntryEdited(s, b) == IF s.entryBuf = b /\ ListenerNotesVisualEdit THEN [s EXCEPT !.entryDirty = TRUE] ELSE s + +\* A plugin's edit in visual mode: the listener counts it, and the model runs the check that the code schedules in the same +\* step, which is true when the check comes before the next key. Visual mode is still on then, so the entry is not consumed, +\* unless the code takes every counted edit for an operator's. A key that comes first is not modeled (a known bug): a +\* mapping that edits and presses Esc in one typeahead, a key that arrives during the plugin's callback, an autocmd edit at +\* a mode change. See SKILL.md, "Scope and bounds". +PluginEditedInVisual(s, b) == + TickMoved(IF VisualCheckSparesPluginEdit THEN s ELSE EntryEdited(s, b), b) + +\* reconcile_held_selection (on_cursor_moved, on_text_changed): changed text makes the plugin report the cursor at +\* once. A cursor that left the flushed position is reported at once (it is final at CursorMoved), another buffer is noted. At CursorMoved and TextChanged the +\* cursor is compared, at BufEnter it is not (Neovim restores it after the event). Entering the Claude terminal +\* keeps the hold and cancels the pending demotion. +\* termKnown: is_claude_terminal_buffer(current buffer) at this event. A new Claude terminal is not registered when +\* BufEnter fires, so then it may be FALSE: the buffer is noted in cafAway and decided at the next event. +Reconcile(s, e, compareCursor, termKnown) == + IF TextChangeReports /\ TextChanged(s, e) THEN Update(ClearHeld(s), e) + ELSE IF TerminalReportsHeldBuffer /\ termKnown /\ TerminalChanged(s, e) THEN ReportHeldBuffer(s) + ELSE IF s.cafBuf = None \/ s.cafLeft THEN s + ELSE LET awayGone == LeaveNoted /\ s.cafAway # None /\ s.cafAway # e.buf + IN IF awayGone /\ s.cafAway # Term THEN [s EXCEPT !.cafLeft = TRUE] + ELSE LET s1 == IF awayGone THEN [s EXCEPT !.cafAway = None] ELSE s + IN IF e.buf = Term /\ termKnown THEN CancelDemotion([s1 EXCEPT !.cafAway = None]) + ELSE IF LeaveNoted /\ s1.cafBuf # e.buf THEN [s1 EXCEPT !.cafAway = e.buf] + ELSE IF MoveReports /\ compareCursor /\ ~Unmoved(s1, e) THEN Update(ClearHeld(s1), e) + ELSE s1 + +\* The listener on the buffer b of the selection Claude holds (watch_selection_buffer): on_lines runs while b changes, +\* and only queues the check with vim.schedule (check_soon), which does not touch the buffer in the callback. It +\* queues nothing when b does not hold the selection. +OnOtherBufferChanged(s, b) == + IF ListensToSelectionBuffer /\ s.rdBuf = b /\ s.latest \in VisValues THEN [s EXCEPT !.chk = TRUE] ELSE s + +\* The queued callback: demote_if_selection_text_changed in whatever state the user is in when it runs. For the buffer +\* you are in it ends the hold, as TextChanged does. In the Claude terminal, which does not update the selection, it +\* sends the cursor of the selection's buffer: where its window has the cursor, else where the selection was released. +\* In another file it does nothing: the debounce replaces the selection there. +\* A scheduled callback runs after the command that made a new Claude terminal returned, so the plugin knows the +\* terminal then, unlike at the BufEnter that the command fires. +ListenerCheck(s, e) == + IF TextChanged(s, e) THEN Update(ClearHeld(s), e) + ELSE IF TerminalReportsHeldBuffer /\ TerminalChanged(s, e) THEN ReportHeldBuffer(s) + ELSE s + +\* The two handlers that call it. A key that edits the cursor line (x) fires CursorMoved, then TextChanged. +OnCursor(s, e, compareCursor, termKnown) == IF ReconcileOnCursorMoved THEN Reconcile(s, e, compareCursor, termKnown) ELSE s +OnText(s, e) == IF ReconcileOnTextChanged THEN Reconcile(s, e, TRUE, TRUE) ELSE s + +NoSpecChange == UNCHANGED <> /\ released' = FALSE +DropHold == hold' = None /\ holdPos' = P0 /\ holdLoose' = FALSE /\ released' = FALSE + +----------------------------------------------------------------------------- +(* The user. Each step is one key or command with the autocmds it fires. *) + +(* v, V, CTRL-V or gv: ModeChanged (entering visual). *) +YouStartSelecting(r) == + /\ mode = "n" + /\ mode' = "v" /\ vsel' = r + /\ SetS(OnModeChanged(S, E2(buf, "v", cur, r, None, ver), TRUE, FALSE)) + /\ UNCHANGED <> + /\ IF buf \in Files THEN DropHold ELSE NoSpecChange + +(* A motion in visual mode: CursorMoved. *) +YouExtendSelection(r, p) == + /\ mode = "v" /\ <> # <> + /\ vsel' = r /\ cur' = p + /\ SetS(DebounceUpdate(OnCursor(S, E2(buf, "v", p, r, None, ver), TRUE, TRUE))) + /\ UNCHANGED <> + /\ NoSpecChange + +(* Esc (or a window command) ends visual mode: Neovim sets '<,'>, then ModeChanged. *) +YouReleaseSelection == + /\ mode = "v" + /\ SetS(OnModeChanged(S, E2(buf, "n", cur, None, [at |-> vsel, ver |-> ver[buf]], ver), FALSE, TRUE)) + /\ mode' = "n" /\ vsel' = None + /\ UNCHANGED <> + /\ IF buf \in Files + THEN hold' = Vis(buf, vsel, ver[buf]) /\ holdPos' = cur /\ holdLoose' = FALSE /\ released' = TRUE + ELSE NoSpecChange + +(* d, c, x, > or another operator on the selection: the text changes (the listener sees *) +(* the edit with the mode already normal, then ModeChanged fires) and the cursor lands *) +(* on p. CursorMoved and TextChanged fire when Neovim waits for the next key, so a *) +(* mapping, a macro or typeahead runs the next key first. The step leaves them out: it *) +(* is the case in which they have not fired yet. *) +YouEditSelection(p) == + /\ buf \in Files /\ mode = "v" /\ ver[buf] < MaxEdits + /\ LET vr == [ver EXCEPT ![buf] = @ + 1] + IN /\ ver' = vr + /\ SetS(DebounceUpdate(OnModeChanged(TickMoved(EntryEdited(S, buf), buf), + E2(buf, "n", p, None, [at |-> vsel, ver |-> ver[buf]], vr), FALSE, TRUE))) + /\ mode' = "n" /\ vsel' = None /\ cur' = p + /\ UNCHANGED buf + /\ DropHold + +(* A motion in a file: CursorMoved. *) +YouMoveCursor(p) == + /\ buf \in Files /\ mode = "n" /\ p # cur + /\ cur' = p + /\ SetS(DebounceUpdate(OnCursor(S, E2(buf, "n", p, None, None, ver), TRUE, TRUE))) + /\ UNCHANGED <> + /\ DropHold + +(* x or r at the cursor: the text under the cursor changes, the cursor stays. TextChanged. *) +YouEditAtCursor == + /\ buf \in Files /\ mode = "n" /\ ver[buf] < MaxEdits + /\ ver' = [ver EXCEPT ![buf] = @ + 1] + /\ SetS(DebounceUpdate(OnText(OnCursor(S, E2(buf, "n", cur, None, None, ver'), TRUE, TRUE), E2(buf, "n", cur, None, None, ver')))) + /\ UNCHANGED <> + /\ NoSpecChange + +(* A plugin, a reload or a command changes text away from the cursor, and the held text *) +(* with it: TextChanged fires, CursorMoved does not. *) +YouEditByPlugin == + /\ buf \in Files /\ mode = "n" /\ ver[buf] < MaxEdits + /\ ver' = [ver EXCEPT ![buf] = @ + 1] + /\ SetS(DebounceUpdate(OnText(S, E2(buf, "n", cur, None, None, ver')))) + /\ UNCHANGED <> + /\ NoSpecChange + +(* A plugin edits another line while you select, and the selection stays on the screen with the *) +(* text it had: the changedtick moves, and the listener counts the edit. No TextChanged and no *) +(* CursorMoved fire in visual mode. An edit whose check has not run when the next key arrives *) +(* would reach the flush unchecked: not modeled (a known bug, see SKILL.md). *) +YouEditByPluginInVisual == + /\ buf \in Files /\ mode = "v" + /\ SetS(PluginEditedInVisual(S, buf)) + /\ UNCHANGED nvim + /\ NoSpecChange + +(* :write in visual mode: it moves the changedtick of a modified buffer and fires no on_lines. *) +YouWriteInVisual == + /\ buf \in Files /\ mode = "v" + /\ SetS(TickMoved(S, buf)) + /\ UNCHANGED nvim + /\ NoSpecChange + +(* A plugin edits, or Neovim reloads, a file that is not the current buffer, and the held *) +(* text with it: no TextChanged and no BufEnter fire. The listener on that buffer queues a *) +(* check (ListenerCheckRuns), which runs later, after any other step. *) +YouEditOtherBuffer(b) == + /\ mode = "n" /\ b \in Files /\ b # buf /\ ver[b] < MaxEdits + /\ ver' = [ver EXCEPT ![b] = @ + 1] + /\ SetS(OnOtherBufferChanged(S, b)) + /\ UNCHANGED <> + /\ NoSpecChange + +(* A change that leaves the cursor and any held selection alone (a line below it, or a *) +(* reload): TextChanged. *) +YouEditElsewhere == + /\ buf \in Files /\ mode = "n" + /\ SetS(DebounceUpdate(OnText(S, E))) + /\ UNCHANGED nvim + /\ NoSpecChange + +(* :b, a window command or a click into buffer b with the cursor at p: BufEnter. *) +(* In the Claude terminal the held selection stays. Back in its file with the *) +(* cursor where it was, Claude may keep it or get the cursor. *) +YouSwitchBuffer(b, p) == + /\ mode = "n" /\ b # buf + /\ b = Term => WithTerminal /\ p = P0 + /\ buf' = b /\ cur' = p + /\ \E cursorMoved, termKnown \in BOOLEAN : + \* Without CursorMoved the cursor lands where the window had it, and a :b lands on the buffer's remembered + \* position, which is the one the plugin recorded: every later move would have set left. + /\ ~cursorMoved => (p = cur /\ (cafBuf = b /\ ~cafLeft => p = cafPos)) + /\ LET e2 == E2(b, "n", p, None, None, ver) + entered == OnCursor(S, e2, FALSE, termKnown) + IN SetS(DebounceUpdate(IF cursorMoved THEN OnCursor(entered, e2, TRUE, TRUE) ELSE entered)) + /\ UNCHANGED <> + /\ IF b = Term + THEN NoSpecChange + ELSE IF buf = Term /\ hold # None /\ hold.buf = b /\ p = holdPos + THEN holdLoose' = TRUE /\ UNCHANGED <> /\ released' = FALSE + ELSE DropHold + +----------------------------------------------------------------------------- +(* The timers. uv fires a timer; schedule_wrap queues its callback; the *) +(* callback runs later on the main loop. *) + +(* The debounce uv timer fires. With the default delays, a pending demotion fires first. *) +DebounceTimerFires == + /\ db = "armed" + /\ DelayBelowDebounce => dm \notin Alive + /\ db' = "queued" + /\ UNCHANGED <> + /\ NoSpecChange + +(* debounce_update's callback for the current timer: clear the field, close, update_selection. *) +DebounceCallbackRuns == + /\ db \in {"queued", "closedQueued"} + /\ LET s1 == [S EXCEPT !.db = IF ClearsBeforeClose THEN "nil" ELSE "closed", !.closedTwice = @ \/ CloseErr(db)] + IN SetS(IF CloseErr(db) THEN s1 ELSE Update(s1, E)) \* the close error aborts the callback + /\ UNCHANGED nvim + /\ NoSpecChange + +(* A callback of a cancelled debounce timer. With the identity check it returns. *) +(* Without it, it clears the field (losing the live timer), and its close errors. *) +StaleDebounceCallbackRuns == + /\ dbStale + /\ dbStale' \in BOOLEAN \* other stale callbacks can wait behind it + /\ IF DebounceIgnoresStale + THEN UNCHANGED <> + ELSE /\ db' = IF ClearsBeforeClose THEN "nil" ELSE db + /\ dbLoose' = (dbLoose \/ (ClearsBeforeClose /\ db \in Alive)) + /\ closedTwice' = TRUE + /\ UNCHANGED <> + /\ NoSpecChange + +(* Without the identity check: a live debounce timer the field lost fires and runs in full. *) +LooseDebounceCallbackRuns == + /\ dbLoose + /\ \E keep \in BOOLEAN : \* other lost timers can still be live + SetS(Update([S EXCEPT !.db = "nil", !.dbLoose = keep \/ db \in Alive], E)) + /\ UNCHANGED nvim + /\ NoSpecChange + +(* check_soon's callback of the listener runs: the check, then nothing is queued. *) +ListenerCheckRuns == + /\ chk + /\ SetS(ListenerCheck([S EXCEPT !.chk = FALSE], E)) + /\ UNCHANGED nvim + /\ NoSpecChange + +DemotionTimerFires == + /\ dm = "armed" + /\ dm' = "queued" + /\ UNCHANGED <> + /\ NoSpecChange + +(* update_selection's demotion callback: clear the field, close, handle_selection_demotion. *) +DemotionCallbackRuns == + /\ dm \in {"queued", "closedQueued"} + /\ LET s1 == [S EXCEPT !.dm = IF ClearsBeforeClose THEN "nil" ELSE "closed", !.closedTwice = @ \/ CloseErr(dm)] + IN SetS(IF CloseErr(dm) THEN s1 ELSE Demote(s1, E, dmBuf)) + /\ UNCHANGED nvim + /\ NoSpecChange + +StaleDemotionCallbackRuns == + /\ dmStale + /\ dmStale' \in BOOLEAN + /\ IF DemotionIgnoresStale + THEN UNCHANGED <> + ELSE /\ dm' = IF ClearsBeforeClose THEN "nil" ELSE dm + /\ dmBuf' = IF ClearsBeforeClose THEN None ELSE dmBuf + /\ dmLoose' = IF ClearsBeforeClose /\ dm \in Alive THEN dmLoose \cup {dmBuf} ELSE dmLoose + /\ closedTwice' = TRUE + /\ UNCHANGED <> + /\ NoSpecChange + +LooseDemotionCallbackRuns(b) == + /\ b \in dmLoose + /\ \E keep \in BOOLEAN : + LET s1 == [S EXCEPT !.dm = "nil", !.dmBuf = None, + !.dmLoose = (IF keep THEN @ ELSE @ \ {b}) \cup (IF dm \in Alive THEN {dmBuf} ELSE {})] + IN SetS(Demote(s1, E, b)) + /\ UNCHANGED nvim + /\ NoSpecChange + +Next == + \/ \E r \in Ranges : YouStartSelecting(r) + \/ \E r \in Ranges, p \in Pos : YouExtendSelection(r, p) + \/ YouReleaseSelection + \/ \E p \in Pos : YouEditSelection(p) + \/ \E p \in Pos : YouMoveCursor(p) + \/ YouEditAtCursor + \/ YouEditByPlugin + \/ YouEditByPluginInVisual + \/ YouWriteInVisual + \/ \E b \in Files : YouEditOtherBuffer(b) + \/ YouEditElsewhere + \/ \E b \in Bufs, p \in Pos : YouSwitchBuffer(b, p) + \/ DebounceTimerFires + \/ DebounceCallbackRuns + \/ StaleDebounceCallbackRuns + \/ LooseDebounceCallbackRuns + \/ DemotionTimerFires + \/ DemotionCallbackRuns + \/ StaleDemotionCallbackRuns + \/ \E b \in Bufs : LooseDemotionCallbackRuns(b) + \/ ListenerCheckRuns + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Rules *) + +\* No timer is running and no timer callback waits: the events have settled. +Settled == db = "nil" /\ dm = "nil" /\ ~dbStale /\ ~dmStale /\ ~dbLoose /\ dmLoose = {} /\ ~chk +InFile == buf \in Files + +(* Right after you release a selection in a file, Claude holds it, also when you made it *) +(* faster than the 100 ms debounce (issue #246). *) +ReleaseSent == released => latest = hold + +(* Claude only gets text you selected: never the text at the '<,'> marks after an *) +(* operator changed it. *) +NoPhantomSelection == ~phantom + +(* Claude never gets a selection in the Claude terminal buffer. *) +NoTerminalSelection == latest = None \/ latest.buf # Term + +(* Once events settle in a file, a selection you released stays with Claude while the *) +(* cursor has not moved and its text is unchanged. *) +HeldUntilMoved == + (Settled /\ InFile /\ mode = "n" /\ hold # None /\ ~holdLoose /\ hold.ver = ver[hold.buf]) => latest = hold + +(* Once events settle in the Claude terminal, Claude still holds the selection you released *) +(* while its text is unchanged: going there to type the question must not lose it (#246). *) +HeldInTerminal == + (Settled /\ buf = Term /\ hold # None /\ ~holdLoose /\ hold.ver = ver[hold.buf]) => latest = hold + +(* Once events settle in a file, Claude holds a released selection only while the cursor *) +(* has not moved since you released it. *) +HeldEndsWhenMoved == (Settled /\ InFile /\ mode = "n" /\ hold = None) => latest \notin VisValues + +(* Once events settle in a file, Claude's selection is in that file. *) +SameFile == (Settled /\ InFile /\ latest # None) => latest.buf = buf + +(* 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. *) +ClaudeSeesCursor == + Settled /\ InFile => + /\ mode = "v" => latest = Vis(buf, vsel, ver[buf]) + /\ (mode = "n" /\ latest \in CurValues /\ latest.buf = buf) => latest.at = cur + +(* Once events settle, Claude holds no text that its buffer no longer has. *) +NoDeletedText == Settled => ~(latest \in VisValues /\ latest.ver # ver[latest.buf]) + +(* No timer handle is closed twice. *) +TimerClosedOnce == ~closedTwice +============================================================================= diff --git a/.agents/skills/verify-selection-tracking/model/statechart-view.ts b/.agents/skills/verify-selection-tracking/model/statechart-view.ts new file mode 100644 index 000000000..3b57b98b5 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/model/statechart-view.ts @@ -0,0 +1,96 @@ +// /statechart view for SelectionTracking.tla: what you do, what Claude holds, and whether a timer still waits. +const file = (b: string) => + ({ f1: "a.txt", f2: "b.txt" })[b] ?? "the Claude terminal"; + +const waiting = (v: any) => + v.db !== "nil" || + v.dbStale || + v.dbLoose || + v.dm !== "nil" || + v.dmStale || + v.chk || + (v.dmLoose && v.dmLoose.length > 0); + +// What Claude holds. While a timer waits, a cursor that is behind is normal, so only a settled state says so. +const what = (v: any) => { + const sel = v.latest; + if (!sel || sel.kind === undefined) return "nothing"; + if (sel.kind === "cur") { + const behind = !waiting(v) && sel.buf === v.buf && sel.at !== v.cur; + return `the cursor in ${file(sel.buf)}${behind ? ", where it was" : ""}`; + } + if (sel.ver !== v.ver[sel.buf]) + return `text you deleted from ${file(sel.buf)}`; + const live = v.mode === "v" && sel.buf === v.buf && sel.at === v.vsel; + const held = + v.hold && + v.hold.kind === "vis" && + v.hold.at === sel.at && + v.hold.buf === sel.buf; + return live || held + ? `your selection in ${file(sel.buf)}` + : `an old selection in ${file(sel.buf)}`; +}; + +const you = (v: any) => { + if (v.buf === "term") + return v.mode === "v" + ? "you select in the Claude terminal" + : "you are in the Claude terminal"; + if (v.mode === "v") return `you select in ${file(v.buf)}`; + if (v.hold && v.hold.kind === "vis") { + const changed = v.hold.ver !== v.ver[v.hold.buf] ? " and edited it" : ""; + return `you released a selection in ${file(v.buf)}${changed}`; + } + return `your cursor is in ${file(v.buf)}`; +}; + +export const title = "What Claude sees as your selection (claudecode.nvim)"; + +export const state = (v: any) => { + if (v.mode === "v" && waiting(v)) return `${you(v)}; a timer waits`; + return `${you(v)}; Claude holds ${what(v)}${waiting(v) ? "; a timer waits" : ""}`; +}; + +export const group = (v: any) => { + if (waiting(v)) return "waiting"; + const sel = v.latest; + const otherFile = + sel && sel.kind !== undefined && v.buf !== "term" && sel.buf !== v.buf; + return otherFile || /deleted|old|where it was/.test(what(v)) + ? "stale" + : "current"; +}; +export const colors = { stale: "pink", current: "teal", waiting: "blue" }; + +const labels: Record = { + YouStartSelecting: "you start selecting (v, V, gv)", + YouExtendSelection: "you extend the selection", + YouReleaseSelection: "you press Esc", + YouEditSelection: "you delete or change the selection (d, c)", + YouMoveCursor: "you move the cursor", + YouEditAtCursor: "you press x on the cursor", + YouEditElsewhere: "you edit another line", + YouEditByPlugin: "a plugin or a reload changes the text away from the cursor", + YouEditOtherBuffer: "a plugin or a reload changes a file that you are not in", + YouEditByPluginInVisual: "a plugin edits another line while you select", + YouWriteInVisual: "you save the file while you select (:write)", + ListenerCheckRuns: "the plugin's listener checks the held text", + DebounceTimerFires: "100 ms pass", + DebounceCallbackRuns: "the plugin updates Claude", + LooseDebounceCallbackRuns: "a lost debounce timer runs", + DemotionTimerFires: "the demotion delay passes", + DemotionCallbackRuns: "the plugin checks whether you moved", + LooseDemotionCallbackRuns: "a lost demotion timer runs", +}; + +// A callback of a cancelled timer returns at once in the code as written, so the chart hides it. +export const step = (action: string, _from: any, to: any) => { + if ( + action === "StaleDebounceCallbackRuns" || + action === "StaleDemotionCallbackRuns" + ) + return null; + if (action === "YouSwitchBuffer") return `you go to ${file(to.buf)}`; + return labels[action] ?? action; +}; diff --git a/.agents/skills/verify-selection-tracking/replays/cursor_after_return.lua b/.agents/skills/verify-selection-tracking/replays/cursor_after_return.lua new file mode 100644 index 000000000..2586ca790 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/cursor_after_return.lua @@ -0,0 +1,23 @@ +-- ClaudeSeesCursor: with visual_demotion_delay_ms longer than two debounces (here 1000 ms), release a selection, +-- move right, wait, move back. Claude must not keep the cursor position you left. Before #452 it did. +-- DELAY_MS=50 (the default delay) reruns the same keys. +local driver = require("driver") +local delay = tonumber(os.getenv("DELAY_MS") or "1000") +driver.run({ + setup = { visual_demotion_delay_ms = delay }, + prepare = function() + driver.files({ { "a.txt", { "alpha beta" } } }) + end, +}, { + { 50, "ve", "ve (select alpha)" }, + { 300, "", " (release it)" }, + { 250, "l", "l (move right)" }, + { 250, "h", "h (move back)" }, +}, function(_, sel) + local cursor = vim.api.nvim_win_get_cursor(0) + if not sel or not sel.selection.isEmpty or sel.selection.start.character == cursor[2] then + return true, "Claude holds the cursor where it is, or the held selection" + end + return false, + string.format("the cursor is at 0:%d, Claude holds the cursor at 0:%d", cursor[2], sel.selection.start.character) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/driver.lua b/.agents/skills/verify-selection-tracking/replays/driver.lua new file mode 100644 index 000000000..5a6869c57 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/driver.lua @@ -0,0 +1,128 @@ +-- Replay driver for the verify-selection-tracking probes. Starts the real plugin (the real start path, the real +-- selection.lua with real uv timers), records every selection_changed the server would broadcast, and types keys +-- through the main loop one step at a time. Only server.broadcast is replaced, and only in this process. +-- A probe calls run(opts, steps, verdict): each step is { wait_ms, keys or function, label }; verdict(log, sel) +-- returns ok (boolean) and a one-line description. Neovim exits 0 for OK and 1 for BUG. +local M = {} + +local function show(sel) + if not sel then + return "nil" + end + local s, e = sel.selection.start, sel.selection["end"] + return string.format( + "%s %q %d:%d-%d:%d%s", + vim.fn.fnamemodify(sel.filePath, ":t"), + sel.text, + s.line, + s.character, + e.line, + e.character, + sel.selection.isEmpty and " (cursor)" or "" + ) +end +M.show = show + +-- Writes each { name, lines } to a fresh temp dir and opens them, the first one last (so it is current). +-- Returns the paths in order. +function M.files(list) + local dir = vim.fn.tempname() + vim.fn.mkdir(dir, "p") + local paths = {} + for i = #list, 1, -1 do + local path = dir .. "/" .. list[i][1] + vim.fn.writefile(list[i][2], path) + vim.cmd.edit(vim.fn.fnameescape(path)) + paths[i] = path + end + return paths +end + +function M.run(opts, steps, verdict) + local out = {} + local function say(line) + table.insert(out, line) + end + vim.o.showmode = false + local claudecode = require("claudecode") + claudecode.setup(vim.tbl_deep_extend("force", { + auto_start = false, + terminal = { provider = "none" }, + log_level = "error", + }, opts.setup or {})) + local ok = claudecode.start(false) + assert(ok, "claudecode.start failed") + local sent = {} + require("claudecode.server.init").broadcast = function(method, params) + if method == "selection_changed" then + table.insert(sent, vim.deepcopy(params)) + say(string.format(" sent selection_changed: %s", show(params))) + end + return true + end + local selection = require("claudecode.selection") + say( + string.format( + "nvim %s, debounce_ms=%d, visual_demotion_delay_ms=%d", + tostring(vim.version()), + selection.state.debounce_ms, + selection.state.visual_demotion_delay_ms + ) + ) + if opts.prepare then + opts.prepare() + end + local i = 0 + local function finish() + local sel = selection.get_latest_selection() + local cursor = vim.api.nvim_win_get_cursor(0) + say( + string.format( + "settled: buffer %s, cursor %d:%d, line %q", + vim.fn.expand("%:t"), + cursor[1] - 1, + cursor[2], + vim.api.nvim_get_current_line() + ) + ) + say(string.format("Claude holds (getLatestSelection): %s", show(sel))) + local good, why = verdict(sent, sel) + say((good and "OK " or "BUG ") .. why) + say(string.format("%d selection_changed sent, result: %s", #sent, good and "rule holds" or "rule broken")) + io.stdout:write(table.concat(out, "\n") .. "\n") + vim.cmd(good and "qa!" or "cquit 1") + end + local function step() + i = i + 1 + local s = steps[i] + if not s then + -- Let every timer settle: well past the debounce and the demotion delay. + vim.defer_fn(finish, 300 + 2 * selection.state.visual_demotion_delay_ms) + return + end + vim.defer_fn(function() + local cursor = vim.api.nvim_win_get_cursor(0) + say( + string.format( + " now: mode=%s buf=%s cursor=%d:%d line=%q", + vim.api.nvim_get_mode().mode, + vim.fn.expand("%:t"), + cursor[1] - 1, + cursor[2], + vim.api.nvim_get_current_line() + ) + ) + local keys = s[2] + say(string.format("+%4dms %s", s[1], s[3] or keys)) + if type(keys) == "function" then + keys() + else + vim.api.nvim_feedkeys(vim.api.nvim_replace_termcodes(keys, true, false, true), "t", false) + end + step() + end, s[1]) + end + step() +end + +return M diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_edit.lua b/.agents/skills/verify-selection-tracking/replays/held_after_edit.lua new file mode 100644 index 000000000..dd2aa3330 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_edit.lua @@ -0,0 +1,23 @@ +-- NoDeletedText: release a selection, then press x on its last character without moving the cursor. Claude must +-- not keep text the buffer no longer has: the plugin reports the cursor once the held text changed. Default delays. +-- Before #452 the held selection survived until the cursor moved. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + end, +}, { + { 50, "viw", "viw (select alpha)" }, + { 300, "", " (release it)" }, + { 300, "x", "x (delete the a under the cursor)" }, + { 300, "x", "x (and the space)" }, +}, function(_, sel) + local line = vim.api.nvim_get_current_line() + if not sel or sel.selection.isEmpty then + return true, "Claude holds the cursor" + end + local s, e = sel.selection.start.character, sel.selection["end"].character + local there = line:sub(s + 1, e) + return there == sel.text, + string.format("Claude holds %q at %d-%d, the buffer has %q there (line %q)", sel.text, s, e, there, line) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_edit_in_terminal.lua b/.agents/skills/verify-selection-tracking/replays/held_after_edit_in_terminal.lua new file mode 100644 index 000000000..4473b2dde --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_edit_in_terminal.lua @@ -0,0 +1,42 @@ +-- NoDeletedText: Claude holds a selection of a.txt, you are in the Claude terminal in the same window (a.txt is in no +-- window), and a plugin deletes the selected text with nvim_buf_set_text. Neovim reports it to the buffer's listeners +-- only. Claude must not keep text that is gone until you come back. Default delays. +local driver = require("driver") +local file_buf +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + file_buf = vim.api.nvim_get_current_buf() + end, +}, { + { 50, "ve", "ve (select alpha)" }, + { 300, "", " (release it)" }, + { + 300, + function() + vim.cmd("terminal sh -c 'sleep 20' claude") + end, + ":terminal ... claude (the Claude terminal, in a.txt's window)", + }, + { + 300, + function() + vim.cmd("stopinsert") + end, + "stopinsert", + }, + { + 300, + function() + vim.api.nvim_buf_set_text(file_buf, 0, 0, 0, 6, {}) + end, + "a plugin deletes 'alpha ' in a.txt", + }, + { 300, function() end, "wait" }, +}, function(_, sel) + if not sel or sel.selection.isEmpty then + return true, "Claude holds the cursor" + end + local lines = vim.api.nvim_buf_get_lines(file_buf, 0, -1, false) + return false, string.format("Claude holds %q, but a.txt is %q", sel.text, table.concat(lines, "|")) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_line_inserted_above.lua b/.agents/skills/verify-selection-tracking/replays/held_after_line_inserted_above.lua new file mode 100644 index 000000000..693d57caf --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_line_inserted_above.lua @@ -0,0 +1,22 @@ +-- A limit that the model does not cover, not a rule: a plugin inserts a line above a held selection. The held range now +-- names other text, so the check that reads the range again finds that the selected text is not there and reports the +-- cursor. Claude loses the selection, although its text still exists one line lower. OK means the plugin does that. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + end, +}, { + { 100, "ve", "select alpha" }, + { 200, "", "release alpha" }, + { + 300, + function() + vim.api.nvim_buf_set_lines(0, 0, 0, false, { "inserted line" }) + end, + "a plugin inserts a line above the held range", + }, +}, function(_, sel) + return sel and sel.selection.isEmpty and sel.selection.start.line == 1, + "Claude holds the cursor on the shifted line, not the selection" +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_operator.lua b/.agents/skills/verify-selection-tracking/replays/held_after_operator.lua new file mode 100644 index 000000000..9bf9d252b --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_operator.lua @@ -0,0 +1,22 @@ +-- HeldEndsWhenMoved / NoDeletedText: a selection made backwards (cursor at its start), released with Esc, then +-- reselected with gv and deleted with d. The cursor ends where the first flush left it. Claude must hold the +-- cursor, not the deleted selection. Default delays. Before #452 the plugin took the deleted selection for a held one. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + vim.api.nvim_win_set_cursor(0, { 1, 4 }) + end, +}, { + { 50, "vb", "vb (select alpha backwards)" }, + { 300, "", " (release it)" }, + { 400, "gv", "gv (select it again)" }, + { 300, "d", "d (delete it)" }, +}, function(_, sel) + local line = vim.api.nvim_get_current_line() + local cursor = vim.api.nvim_win_get_cursor(0) + if sel and sel.selection.isEmpty and sel.selection.start.character == cursor[2] then + return true, "Claude holds the cursor" + end + return false, string.format("Claude holds %q, but the line is now %q", sel and sel.text or "nil", line) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_plugin_edit.lua b/.agents/skills/verify-selection-tracking/replays/held_after_plugin_edit.lua new file mode 100644 index 000000000..01fb3366f --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_plugin_edit.lua @@ -0,0 +1,27 @@ +-- NoDeletedText: a plugin (or a reload, or a command) changes the held text away from the cursor. TextChanged fires, +-- CursorMoved does not. The TextChanged handler ends the hold, and so does the buffer listener (on_lines fires for an +-- edit of the current buffer too), so this probe also passes with the TextChanged call removed: it does not prove +-- that guard on its own (see SKILL.md, "Read the result"). Claude must not keep text the buffer no longer has. +-- Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta", "gamma delta" } } }) + end, +}, { + { 50, "Vj", "Vj (select both lines)" }, + { 300, "", " (release it)" }, + { + 300, + function() + vim.api.nvim_buf_set_text(0, 0, 0, 0, 6, {}) + end, + "a plugin deletes 'alpha ' on line 1 (cursor stays on line 2)", + }, +}, function(_, sel) + if not sel or sel.selection.isEmpty then + return true, "Claude holds the cursor" + end + local lines = vim.api.nvim_buf_get_lines(0, 0, -1, false) + return false, string.format("Claude holds %q, but the buffer is %q", sel.text, table.concat(lines, "\n")) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_quick_move.lua b/.agents/skills/verify-selection-tracking/replays/held_after_quick_move.lua new file mode 100644 index 000000000..d38c81490 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_quick_move.lua @@ -0,0 +1,21 @@ +-- HeldEndsWhenMoved: release a selection, then move away and back faster than the 100 ms debounce. Claude must +-- hold the cursor, not the selection: the plugin notes the move when CursorMoved fires, not when the debounce +-- fires. Default delays. Before #452 it compared the cursor only at the debounce and kept the selection. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + end, +}, { + { 50, "ve", "ve (select alpha)" }, + { 300, "", " (release it)" }, + { 300, "l", "l (move right)" }, + { 30, "h", "h (back, 30 ms later)" }, +}, function(_, sel) + local cursor = vim.api.nvim_win_get_cursor(0) + if sel and sel.selection.isEmpty and sel.selection.start.character == cursor[2] then + return true, "Claude holds the cursor" + end + return false, + string.format("the cursor moved after the release, but Claude still holds %q", sel and sel.text or "nil") +end) diff --git a/.agents/skills/verify-selection-tracking/replays/held_after_reload_in_terminal.lua b/.agents/skills/verify-selection-tracking/replays/held_after_reload_in_terminal.lua new file mode 100644 index 000000000..56e1ef4d1 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/held_after_reload_in_terminal.lua @@ -0,0 +1,46 @@ +-- NoDeletedText: Claude holds a selection of a.txt, you are in the Claude terminal, and Claude rewrites a.txt on disk +-- without the selected text. Neovim reloads the file (autoread, here `:checktime`), and TextChanged does not fire +-- for a buffer that is not current. Claude must not keep text that is gone until you come back. Default delays. +local driver = require("driver") +local file_buf, path +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + file_buf = vim.api.nvim_get_current_buf() + path = vim.api.nvim_buf_get_name(file_buf) + end, +}, { + { 50, "ve", "ve (select alpha)" }, + { 300, "", " (release it)" }, + { + 300, + function() + vim.cmd("vsplit | terminal sh -c 'sleep 20' claude") + end, + ":vsplit | :terminal ... claude (a.txt stays in its window)", + }, + { + 300, + function() + vim.cmd("stopinsert") + end, + "stopinsert", + }, + { + 300, + function() + vim.fn.writefile({ "beta gamma" }, path) + local later = os.time() + 10 + (vim.uv or vim.loop).fs_utime(path, later, later) -- a modification time that Neovim sees as new + vim.cmd("checktime " .. file_buf) + end, + "Claude rewrites a.txt without 'alpha ', :checktime reloads it", + }, + { 300, function() end, "wait" }, +}, function(_, sel) + if not sel or sel.selection.isEmpty then + return true, "Claude holds the cursor" + end + local lines = vim.api.nvim_buf_get_lines(file_buf, 0, -1, false) + return false, string.format("Claude holds %q, but a.txt is %q", sel.text, table.concat(lines, "|")) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/other_file_after_return.lua b/.agents/skills/verify-selection-tracking/replays/other_file_after_return.lua new file mode 100644 index 000000000..d368fb38a --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/other_file_after_return.lua @@ -0,0 +1,22 @@ +-- SameFile: with visual_demotion_delay_ms longer than two debounces (here 1000 ms), release a selection in a.txt, +-- go to b.txt and back while the demotion is still pending. Claude must not end up holding b.txt's cursor while +-- you are in a.txt. Before #452 it did. DELAY_MS=50 (the default delay) reruns the same keys. +local driver = require("driver") +local delay = tonumber(os.getenv("DELAY_MS") or "1000") +driver.run({ + setup = { visual_demotion_delay_ms = delay }, + prepare = function() + driver.files({ { "a.txt", { "alpha beta" } }, { "b.txt", { "one two" } } }) + end, +}, { + { 50, "ve", "ve (select alpha in a.txt)" }, + { 300, "", " (release it)" }, + { 250, ":b b.txt", ":b b.txt" }, + { 250, ":b a.txt", ":b a.txt (cursor back where it was)" }, +}, function(_, sel) + local here = vim.api.nvim_buf_get_name(0) + if sel and sel.filePath == here then + return true, "Claude's selection is in a.txt" + end + return false, string.format("you are in a.txt, Claude holds %s", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_after_autocmd_edit_in_visual.lua b/.agents/skills/verify-selection-tracking/replays/release_after_autocmd_edit_in_visual.lua new file mode 100644 index 000000000..a43089dde --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_after_autocmd_edit_in_visual.lua @@ -0,0 +1,25 @@ +-- A known bug that the model does not cover (fix PR #540): an autocmd edits another line when visual mode starts (a +-- `ModeChanged` handler for `n:v`), and the Esc is already in the typeahead (`ve`). The listener counts the edit and +-- schedules the check that would show that visual mode is still on, but no main-loop turn runs before the flush on Esc, +-- so the flush takes the edit for an operator's. Claude gets the cursor, not the selection, although its text is +-- untouched. BUG means the plugin still does that; the probe prints OK once the fix lands. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + vim.api.nvim_create_autocmd("ModeChanged", { + pattern = "n:v", + once = true, + callback = function() + vim.api.nvim_buf_set_text(0, 1, 0, 1, 6, { "SECOND" }) + end, + }) + end, +}, { + { 20, "ve", "select and release in one typeahead, a ModeChanged autocmd edits line 2" }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_after_plugin_append_in_visual.lua b/.agents/skills/verify-selection-tracking/replays/release_after_plugin_append_in_visual.lua new file mode 100644 index 000000000..83e428875 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_after_plugin_append_in_visual.lua @@ -0,0 +1,24 @@ +-- ReleaseSent / HeldUntilMoved: a plugin appends lines to the end of the buffer while you are in visual mode, and you +-- press Esc inside the 100 ms debounce. The selection is untouched and still on the screen, so the flush on Esc must +-- send it, although the changedtick moved. Before #524 Claude got the cursor. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + end, +}, { + { 20, "ve", "select alpha" }, + { + 10, + function() + vim.api.nvim_buf_set_lines(0, -1, -1, false, { "appended one", "appended two" }) + end, + "a plugin appends two lines while you are in visual mode", + }, + { 10, "", "release inside the debounce" }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_after_plugin_edit_in_visual.lua b/.agents/skills/verify-selection-tracking/replays/release_after_plugin_edit_in_visual.lua new file mode 100644 index 000000000..f0985bf26 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_after_plugin_edit_in_visual.lua @@ -0,0 +1,25 @@ +-- ReleaseSent / HeldUntilMoved: a plugin edits another line while you are in visual mode, and you press Esc inside the +-- 100 ms debounce, so nothing was sent in visual mode. The edit moves the buffer's changedtick but leaves the selection +-- on the screen, so the flush on Esc must send it. Before #524 the flush took a moved changedtick for an operator that +-- consumed the selection, and Claude got the cursor. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + end, +}, { + { 20, "ve", "select alpha" }, + { + 10, + function() + vim.api.nvim_buf_set_text(0, 1, 0, 1, 6, { "SECOND" }) + end, + "a plugin edits line 2 while you are in visual mode", + }, + { 10, "", "release inside the debounce" }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_after_write_in_visual.lua b/.agents/skills/verify-selection-tracking/replays/release_after_write_in_visual.lua new file mode 100644 index 000000000..0866a5d95 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_after_write_in_visual.lua @@ -0,0 +1,26 @@ +-- ReleaseSent / HeldUntilMoved: you change line 2 (the buffer is modified), select `alpha` on line 1, a :write saves the +-- file while you are in visual mode, and you press Esc inside the 100 ms debounce. The write moves the buffer's +-- changedtick and fires no on_lines, and the selection is untouched, so the flush on Esc must send it. Before #524 the +-- flush took the moved changedtick for an operator and Claude got the cursor. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + vim.api.nvim_buf_set_lines(0, 1, 2, false, { "changed line" }) + end, +}, { + { 20, "ve", "select alpha" }, + { + 10, + function() + vim.cmd("silent write") + end, + ":write while you are in visual mode", + }, + { 10, "", "release inside the debounce" }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_in_same_typeahead_as_plugin_edit.lua b/.agents/skills/verify-selection-tracking/replays/release_in_same_typeahead_as_plugin_edit.lua new file mode 100644 index 000000000..0b20643c8 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_in_same_typeahead_as_plugin_edit.lua @@ -0,0 +1,26 @@ +-- A known bug that the model does not cover (fix PR #540): a mapping edits another line while you are in visual +-- mode and presses Esc in the same typeahead (`lua ...`). The listener counts the edit and schedules the +-- check that would show that visual mode is still on, but no main-loop turn runs between the edit and the Esc, so the +-- flush on Esc finds an edit that nobody checked and takes it for an operator's. Claude gets the cursor, not the +-- selection, although its text is untouched. A plugin edit whose check runs before the next key is not like this +-- (`release_after_plugin_edit_in_visual.lua`). Two other ways to reach the same flush are +-- `release_with_key_during_plugin_callback.lua` and `release_after_autocmd_edit_in_visual.lua`. BUG means the plugin +-- still does that; the probe prints OK once the fix lands. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + end, +}, { + { 20, "ve", "select alpha" }, + { + 10, + "lua vim.api.nvim_buf_set_text(0, 1, 0, 1, 6, { 'SECOND' })", + "a mapping edits line 2 and releases in the same typeahead", + }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/release_with_key_during_plugin_callback.lua b/.agents/skills/verify-selection-tracking/replays/release_with_key_during_plugin_callback.lua new file mode 100644 index 000000000..6afe839f6 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/release_with_key_during_plugin_callback.lua @@ -0,0 +1,27 @@ +-- A known bug that the model does not cover (fix PR #540): a plugin edits another line from a timer callback while you +-- are in visual mode, and your Esc arrives while that callback still runs (`nvim_input`, the way a UI sends a key). The +-- schedule that would check the edit runs after the callback, and the key was read first, so the flush on Esc takes the +-- edit for an operator's. Claude gets the cursor, not the selection, although its text is untouched. A plugin edit +-- whose callback ends before the next key is not like this (`release_after_plugin_edit_in_visual.lua`). BUG means the +-- plugin still does that; the probe prints OK once the fix lands. Default delays. +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma", "second line" } } }) + end, +}, { + { 20, "ve", "select alpha" }, + { + 10, + function() + vim.api.nvim_buf_set_text(0, 1, 0, 1, 6, { "SECOND" }) + vim.api.nvim_input("") -- your key arrives while the plugin's callback runs + end, + "a plugin edits line 2 from a timer callback, and Esc arrives during that callback", + }, +}, function(_, sel) + if sel and not sel.selection.isEmpty and sel.text == "alpha" then + return true, "Claude holds the selection" + end + return false, string.format("Claude holds %s, not the selection that you released", driver.show(sel)) +end) diff --git a/.agents/skills/verify-selection-tracking/replays/run.sh b/.agents/skills/verify-selection-tracking/replays/run.sh new file mode 100755 index 000000000..1c6d521be --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/run.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +# Run one replay probe on headless Neovim with this checkout first on 'runtimepath'. +# Usage: .agents/skills/verify-selection-tracking/replays/run.sh .lua (NVIM=/path/to/nvim to pick a binary) +# Each run gets a fresh XDG and CLAUDE_CONFIG_DIR under $XUM_SCRATCH_DIR (or /tmp), removed afterwards. +# Exit 0 when the probe prints OK, 1 when it prints BUG. +set -euo pipefail +[[ $# -eq 1 ]] || { + echo "usage: run.sh .lua (NVIM=/path/to/nvim picks the binary, DELAY_MS= sets the demotion delay of the two long-delay probes)" >&2 + exit 2 +} +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +repo=$(git -C "$here" rev-parse --show-toplevel) +probe=$here/$(basename "$1") +[[ -f $probe ]] || { + echo "no probe $1 in $here" >&2 + exit 2 +} +tmp=$(mktemp -d "${XUM_SCRATCH_DIR:-/tmp}/selection-replay.XXXXXX") +trap 'rm -rf "$tmp"' EXIT +mkdir -p "$tmp/config" "$tmp/data" "$tmp/state" "$tmp/cache" "$tmp/claude" "$tmp/tmp" +# The paths go through the environment and are escaped by Neovim's own Lua API (a comma in 'runtimepath' is not enough +# for require, so the lua directory is on package.path too), so a checkout path with a space, a comma or a quote works. The watchdog is plain bash: macOS has no GNU timeout. +export REPLAY_REPO=$repo REPLAY_HERE=$here REPLAY_PROBE=$probe +XDG_CONFIG_HOME=$tmp/config XDG_DATA_HOME=$tmp/data XDG_STATE_HOME=$tmp/state XDG_CACHE_HOME=$tmp/cache \ + CLAUDE_CONFIG_DIR=$tmp/claude TMPDIR=$tmp/tmp "${NVIM:-nvim}" --headless -u NONE -i NONE \ + --cmd "lua local repo = os.getenv('REPLAY_REPO'); vim.opt.rtp:prepend(repo); package.path = os.getenv('REPLAY_HERE') .. '/?.lua;' .. repo .. '/lua/?.lua;' .. repo .. '/lua/?/init.lua;' .. package.path" \ + -c "lua dofile(os.getenv('REPLAY_PROBE'))" & +nvim_pid=$! +( + sleep 30 + kill -KILL "$nvim_pid" 2>/dev/null +) >/dev/null 2>&1 & +watchdog_pid=$! +status=0 +wait "$nvim_pid" || status=$? +kill "$watchdog_pid" 2>/dev/null || true +wait "$watchdog_pid" 2>/dev/null || true +exit "$status" diff --git a/.agents/skills/verify-selection-tracking/replays/v_escape_selects_one_character.lua b/.agents/skills/verify-selection-tracking/replays/v_escape_selects_one_character.lua new file mode 100644 index 000000000..c36488b61 --- /dev/null +++ b/.agents/skills/verify-selection-tracking/replays/v_escape_selects_one_character.lua @@ -0,0 +1,16 @@ +-- Not a rule, a fact about what a bare `v` and Esc does: with no motion, `v` selects the character under the cursor, so +-- Esc releases a selection of one character, and the plugin sends it. It replaces the selection Claude held before. +-- OK means Claude holds that one character ("a", where the cursor stood after "alpha" was released). +local driver = require("driver") +driver.run({ + prepare = function() + driver.files({ { "a.txt", { "alpha beta gamma" } } }) + end, +}, { + { 50, "ve", "select alpha" }, + { 150, "", "release alpha" }, + { 300, "v", "v without any motion" }, + { 20, "", "Esc without any motion" }, +}, function(_, sel) + return sel and sel.text == "a" and not sel.selection.isEmpty, "Claude holds the one character under the cursor" +end)