Repository navigation
test(terminal): test the snacks guards that no test reached, and drop four dead window option assignments - #526
Conversation
… a dead bo assignment Six guards of the snacks wrapper survived a mutant on all 372 terminal tests: the type guard of register_window_events, the z-index and filetype checks of find_backdrop, and the bo removal of the stored window options. A seventh, the bo removal in wrapper_options, changes nothing: wrap_terminal and upgrade_wrapper reset opts.bo after the constructor, and Snacks.win reads it only when it shows a window. Each guard has a test that fails without it now, and the dead assignment is gone.
|
@codex review |
|
@codex security review |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Codex Review: Didn't find any major issues. Breezy! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
…d pin what stays Review of the first commit found three more assignments that change nothing: plain() already drops on_buf and on_win, and wrap_terminal and upgrade_wrapper reset bo right after the constructor. Only window.keys = nil has an effect, so the test for the stored options asserts that alone. The reset comment now says why the reset runs there: Snacks sets bo on the buffer again on every VimResized. The no-z-index test uses the shape of a real split (relative = "", no z-index).
|
@codex review |
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
|
Codex Review: Didn't find any major issues. Another round soon, please! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
Resolve the scripts/README.md conflict with #531. The run-release-please.sh bullet keeps the verified text and adds main's clause that commonmark must be on the module path too (release-please-runner.js requires it at load). #526 changes only comments and dead window option assignments in terminal/snacks.lua, and no README line of this branch depends on them.
… it contradicts (coder#533) ## Why The goal is that every claim in the README contracts of this repository is true for the code at `main`, and that each correction names its evidence. A contract is the README of one folder. It states what the code does and cites the function that does it. The branch `docs-gtz7` corrected many claims at an old commit of `main`. `main` has moved since (peer PRs coder#445 to coder#522 rewrote several passages and changed the code). This PR merges `main` into that work, re-checks every line that it changes against the current code, and fixes the lines that the peers made stale or that the merge joined into false text. ## What changed Docs only, in seven README files. The branch has four parts. 1. The commits of `docs-gtz7` (three content commits and a merge of `main`): a refresh of the contracts against the code, a pass that fixed the drift that the refresh left, and a pass that corrected claims which runtime probes disproved. 2. Five merge commits of `main` (the second for coder#522, the third for coder#524 and coder#530, the fourth for coder#506, the fifth for coder#531 and coder#526). Where a peer PR and `docs-gtz7` both changed a passage, `main`'s text won. A `docs-gtz7` correction stayed only where it is still true. 3. Nine correction commits. Six verifier agents, one per file or half file, checked every line that this diff changes against the code. They ran headless Neovim 0.12.3 probes (one on 0.10.4) where reading did not decide the claim. I applied their corrections in commits that group the files: server, root and plugin, tools, lua, terminal, scripts, the main-text fixes, and one for the exit sentences and the last seven findings. A second verifier then found one false sentence (the exit sentence below) and seven wording findings, which that last commit fixes. 4. One commit for two P2 findings of the Codex code review on `42ef1bd1`. First, `stop` and the token mismatch in `start` try to remove the lock file and only log a warning when that fails (`lua/claudecode/init.lua:642-647`, `:605-608`), so three sentences in `README.md` now say "tries to". Second, the headless auto-setup check in `plugin/README.md` used `--cmd "set rtp^=$PWD"`, which Ex splits at a space in the checkout path. I ran it in `/…/with space/repo` on Neovim 0.12.3: it fails with `E518` and prints `0`. The `lua vim.opt.rtp:prepend(vim.fn.getcwd())` form prints `2`, and `0` without the auto-setup line, as the README says. Per file, with the number of claims checked and the result: | File | Claims checked | True | False | Incomplete | Unverified | Edits | |---|---|---|---|---|---|---| | `README.md` (Repository Blueprint) | 41 | 39 | 0 | 2 | 0 | 2 | | `plugin/README.md` | 40 | 39 | 0 | 1 | 0 | 1 | | `lua/claudecode/README.md` | 198 | 173 | 11 | 14 | 0 | 23 | | `lua/claudecode/server/README.md` | 88 | 75 | 3 | 9 | 1 | 13 | | `lua/claudecode/terminal/README.md` | 106 | 100 | 2 | 4 | 0 | 5 | | `lua/claudecode/tools/README.md` | 68 | 54 | 4 | 10 | 0 | 14 | | `scripts/README.md` | 7 | 0 | 2 | 4 | 0 | 13 | A false claim was true at the old base or never true. An incomplete claim leaves out a condition that the code has. The row for `scripts/README.md` lists the seven items of the coder#462 verifiers (one more was misleading). The 541 claims of the first six rows split into 480 true, 20 false, 40 incomplete and 1 unverified. ### Re-sync items after the peer PRs - coder#530 (invalid `provider`). `lua/claudecode/README.md` said that an invalid `provider` keeps the previous value "although the warning says Defaulting to 'native'". `main` now warns `Keeping '<provider>'` (`lua/claudecode/terminal.lua:483-488`). The sentence says what the warning names now. The defect is gone from the list of code defects below. - coder#531 (release-please runner). The `run-release-please.sh` bullet of `scripts/README.md` keeps the verified text and adds `main`'s clause that `commonmark` must be on the module path too. The runner requires it at load (`scripts/release-please-runner.js:27`). The Communique, Prettier and output code that the runner bullet cites did not change. - coder#526 (snacks tests). It changes comments and dead window option assignments in `lua/claudecode/terminal/snacks.lua`. No line of this PR depends on them. - coder#524 (visual selection and plugin edits). The two conflicts were passages about the buffer listener and the flush of a visual selection. `main`'s text won in both, and the root `Editor state` bullet keeps the verified autocmd group list with `main`'s listener wording (`lua/claudecode/selection.lua:watch_selection_buffer`, `note_visual_edit`). The selection claims that this PR changes (`selection_changed` positions, `selection.lua` internals) do not depend on the code that coder#524 changed. - coder#459 (lockfile). `README.md` no longer says that `start` leaves the lock file on disk after a token mismatch: `start` removes it and stops the server (`lua/claudecode/init.lua:603-619`). The System Verification bullet about `CLAUDE_CONFIG_DIR` and `tests/lockfile_test.lua` is gone: the test hides the caller's value and stays in a private home (`tests/lockfile_test.lua:340-355`, `:439-442`). `lockfile.update` is removed from `lua/claudecode/README.md`: the module has no such function. The `start` and `stop` bullets use the text of coder#459, and `stop` is described as an attempt to remove the lock file (`init.lua:635-670`). - coder#461 (openFile reload). The reload-error passage of `lua/claudecode/tools/README.md` is the text of `main`. The claim that the recovery read does not end Visual mode stays. A probe confirmed it in both forms: plain Visual mode, and Visual mode that CTRL-O started. The read runs through `nvim_buf_call`, so the mode stays on (`lua/claudecode/tools/open_file.lua`). - coder#462 (WebSocket shell clients removed). No README cites `scripts/lib_claude.sh` or another deleted file (a grep over the seven files finds none). ### Corrections per file <details> <summary>README.md</summary> - The list of what rejects a pending `openDiff` now includes Claude's `close_tab` and `closeAllDiffTabs` calls, which reject it through `close_diff_by_tab_name` (`lua/claudecode/diff.lua:2040-2044`, `:2105-2107`, `lua/claudecode/tools/close_tab.lua:53`, `lua/claudecode/tools/close_all_diff_tabs.lua:30`). - At exit, Neovim fires `BufUnload` for each loaded buffer before `VimLeavePre`, and the proposal buffer's `BufUnload` autocmd rejects its pending diff (`lua/claudecode/diff.lua:1279-1285`). So with one pending diff the rejection runs before the `VimLeavePre` cleanup. With two or more pending native diffs there is one exception: the reject of a new-file diff in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default) deletes its proposal buffer (`diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop then stops firing `BufUnload`, and the cleanup removes the other diffs with no answer. Probes on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3 show both cases, and the `unified` layout answers every diff. The sentence states both. A fix PR (F13) follows, see "Defects in the code". - `start` removes the lock file on a token mismatch (see above). - The Processes bullet adds `:checkhealth claudecode` (`<cli> --version`, `lua/claudecode/health.lua:43-66`) and the `git rev-parse` of `terminal.git_repo_cwd` (`lua/claudecode/cwd.lua:28-42`). - `CLAUDE_CONFIG_DIR` set but empty uses `~/.claude/ide` (`lua/claudecode/lockfile.lua:11-18`). Three lines say so now. - The Side Effects bullet lists the autocmd groups of `lua/` and `plugin/` (`ClaudeCodeShutdown`, `ClaudeCodeSelection`, `ClaudeCodeMCPDiff`, `ClaudeCodeDiffCleanup`, `ClaudeCodeNativeAdopted`, `ClaudeCodeOpenFileNewFiles`, and one `snacks_win_<id>` per Snacks terminal whose split the plugin re-creates, `lua/claudecode/terminal/snacks.lua:259`), the `nvim_buf_attach` listeners (`lua/claudecode/selection.lua:175-191`) and the `"unified"` highlight groups (`lua/claudecode/diff_inline.lua:33-36`). </details> <details> <summary>plugin/README.md</summary> - Commands from auto-setup exist after a startup script that waits (`:sleep` or `vim.wait()`) lets the deferred `setup` run. They do not exist when the `-c` commands and `VimEnter` run. Headless probes on Neovim 0.12.3 (`plugin/claudecode.lua:13-17`). - The other 39 changed claims held: the load guard order, the second `source` doing nothing, the version error on Neovim older than 0.8, the failed module load shown once, the auto-setup global read twice, and the error from the deferred `setup`. </details> <details> <summary>lua/claudecode/README.md: 23 corrections with evidence</summary> - Only :ClaudeCodeSend uses the local add_paths_to_claude. :ClaudeCodeTreeAdd and :ClaudeCodeAdd call M.send_at_mention in their own code. Evidence: lua/claudecode/init.lua:703, init.lua:830, init.lua:904, init.lua:914, init.lua:974-975, init.lua:1021-1022, init.lua:1126. - expand_tilde expands only `~` and `~/...`. A path such as `~user/x` stays as it is. Evidence: lua/claudecode/init.lua:1113-1117, lua/claudecode/utils.lua:167-181. - The fallback split runs create_split, whose leave_preview_window moves from the preview window to a tiled Claude terminal window in the same tab before it splits. Evidence: lua/claudecode/diff.lua:803-810, diff.lua:263-276, diff.lua:279-281. - Since coder#483 and coder#469, diff_inline.lua no longer calls _resolve_diff_as_saved (it calls _write_proposal) and it also calls _register_reject_when_hidden and _close_proposal_window. Evidence: lua/claudecode/diff_inline.lua:471, diff_inline.lua:485, diff_inline.lua:616, lua/claudecode/diff.lua:1228-1234, commits 6eef218 (coder#483) and 36f4a0e (coder#469). - lockfile.update no longer exists: PR coder#459 (0e63cc7) removed it. Evidence: lua/claudecode/lockfile.lua:74, lockfile.lua:84, lockfile.lua:208, lockfile.lua:239, lockfile.lua:292 (the only M functions), commit 0e63cc7 (coder#459). - terminal.setup also calls get_provider, whose fallback warnings go through logger.warn, as the bullet above says. Evidence: lua/claudecode/terminal.lua:584, terminal.lua:124-130, terminal.lua:145, terminal.lua:163-166, terminal.lua:178. - A connected send that the debounce queues still fires ClaudeCodeSendComplete. Only the disconnected branch fires none. Evidence: lua/claudecode/init.lua:383-398, lua/claudecode/init.lua:1395-1400, lua/claudecode/init.lua:401-416. - The terminal call and the event happen only when _broadcast_at_mention succeeds. Evidence: lua/claudecode/init.lua:383-400. - No handshake polling exists since coder#454/coder#480. The 50 ms, 25 ms and connection_wait_delay facts repeat main's queue bullet. A send with debouncing off still queues behind a non-empty queue. Evidence: lua/claudecode/init.lua:283-289, lua/claudecode/init.lua:110-111, lua/claudecode/init.lua:1381-1396. - PR coder#452 added TextChangedI and TextChangedP. Evidence: lua/claudecode/selection.lua:387. - Since coder#452 reconcile_held_selection reports the cursor at CursorMoved, not after visual_demotion_delay_ms. A text change and another buffer also end the hold. Evidence: lua/claudecode/selection.lua:237-265, lua/claudecode/selection.lua:118-159, lua/claudecode/selection.lua:576-584, tests/selection_test.lua:2341. - find_main_editor_window skips only a fixed filetype list, not every explorer or outline sidebar. Evidence: lua/claudecode/diff.lua:157-190. - find_main_editor_window can return a window of another tab (current tab first), as the bullet above says. Evidence: lua/claudecode/diff.lua:125-142, lua/claudecode/diff_inline.lua:382-409. - Probe: proposal "a\n\n" is accepted as "a\n" (split_lines drops one trailing empty line, and the newline fix adds none back). Evidence: lua/claudecode/diff_inline.lua:44-52, lua/claudecode/diff_inline.lua:526-540, lua/claudecode/diff_inline.lua:303, probe_unified_accept.out. - An invalid diff percentage falls back to split_width_percentage, not straight to 0.30. Evidence: lua/claudecode/diff.lua:50-69. - PR coder#469 set the unified proposal buffer to bufhidden=hide (main's bullet above says so), WinClosed/BufHidden reject it. Evidence: lua/claudecode/diff_inline.lua:299, lua/claudecode/diff_inline.lua:475-485, lua/claudecode/diff.lua:1189-1222. - The close_tab tool also passes a client_id. Evidence: lua/claudecode/tools/close_tab.lua:53, lua/claudecode/diff.lua:2105-2148. - At qa! the BufUnload autocmd (diff.lua:1283) calls _resolve_diff_as_rejected before the VimLeavePre cleanup runs, for one pending diff. With two or more native diffs, a keep_empty reject of a new-file diff deletes its buffer and stops the exit loop, so the later diffs stay pending until the cleanup (the Augroups bullet states this). Evidence: lua/claudecode/diff.lua:1171-1175, lua/claudecode/diff.lua:1279-1285, lua/claudecode/diff.lua:1523-1524, probes on 0.8.0 to 0.12.3. - PR coder#478 added the WinClosed autocmd that deletes the handler. Evidence: lua/claudecode/diff.lua:455-463, tests/unit/diff_new_tab_terminal_handler_spec.lua:127. - require('claudecode').setup validates log_level (assert) before logger.setup runs. Evidence: lua/claudecode/init.lua:462-465, lua/claudecode/config.lua:15, lua/claudecode/config.lua:98-106, lua/claudecode/logger.lua:26-40. - Neovim 0.10 has no 'messagesopt' and always stops. The parenthetical read as if only 0.11+ stops. Evidence: probe_echospace.out (0.10.4: NO SUCH OPTION, 0.11.5: hit-enter,history:500). - With laststatus=1 and two windows v:echospace is 68, not 51. Evidence: probe_echospace.out. - PR coder#445 removed the skip. The loop runs every file. Evidence: scripts/run_integration_tests_individually.sh:86-88. </details> <details> <summary>lua/claudecode/server/README.md: 13 corrections with evidence</summary> - The pending check/idle pair of a tick runs judge_silence and judge_stall, not only a stall confirmation Evidence: lua/claudecode/server/tcp.lua:601-611, tcp.lua:424-435, tcp.lua:490. - The state stays `closing` after on_close. On_close only removes the client (README line on client states says it never becomes `closed`) Evidence: lua/claudecode/server/client.lua:363-371, tcp.lua:227-228, tcp.lua:275-283. - start_close_timer also sets `closed` when a keepalive window passes with no write progress Evidence: lua/claudecode/server/client.lua:459-466, client.lua:140-144. - Completes the state list: _disconnect_client does not touch client.state (probe: on_disconnect saw state `connected` after EOF) Evidence: lua/claudecode/server/tcp.lua:209-217, tcp.lua:255-294, probe-server/events.log client_8, client_9. - PR coder#480 added connected_at to get_client_info Evidence: lua/claudecode/server/client.lua:522-531, client.lua:292. - PR coder#454 moved process_mention_queue from on_connect to on_open Evidence: lua/claudecode/server/init.lua:57-73, client.lua:294-296. - After the merged sentences, `It` reads as process_data or the Close frame. Process_data does check the whole message Evidence: lua/claudecode/server/frame.lua:156-168, client.lua:184-188. - parse_frame rejects a 1-byte Close payload with 1002 (same bullet group says so), so only an empty payload reaches the 1000 default Evidence: lua/claudecode/server/frame.lua:157-160, client.lua:352-361, probe S5, S6. - Since PR coder#455/coder#488 last_pong plays no part in the keepalive Evidence: lua/claudecode/server/client.lua:381-383, client.lua:529, tcp.lua:220-222, tcp.lua:474-475. - PR coder#497/coder#500: tools/call answers -32602 for a non-string name before handle_invoke. Contradicts the JSON-RPC errors bullet Evidence: lua/claudecode/server/init.lua:353-368. - Two callbacks share the name: process_data's on_error carries client errors (other bullets say so), server.on_error only server failures Evidence: lua/claudecode/server/tcp.lua:121,190,196,524, tcp.lua:229-231, client.lua:202,275. - The 101/error write callback calls on_error when err or not success Evidence: lua/claudecode/server/client.lua:271-279, probe events client_1..3. - The message carries the tool name Evidence: lua/claudecode/tools/init.lua:90-96. </details> <details> <summary>lua/claudecode/terminal/README.md: 5 corrections with evidence</summary> - FALSE since coder#464: native close and the first get_active_bufnr of a module copy adopt a marked live terminal. The sentence also contradicts the same bullet's second sentence. Evidence: lua/claudecode/terminal/native.lua:292, lua/claudecode/terminal/native.lua:574-577, probe probe-terminal/probe_native_reload.out. - INCOMPLETE: on Neovim 0.12.3 termopen also returns 0 under :silent! for a modified buffer, which is not an invalid argument. Evidence: probe probe-terminal/probe_termopen.out (cases D, E, F, G, H, I), lua/claudecode/terminal/native.lua:237-242. - INCOMPLETE: through the dispatcher a missing Snacks never reaches the ERROR notification, because get_provider falls back to native. Evidence: lua/claudecode/terminal.lua:133-146, lua/claudecode/terminal.lua:192-196, lua/claudecode/terminal/snacks.lua:691-693. - INCOMPLETE: an unset snacks_win_opts.position falls back to split_side (left or right), so cc_show re-creates a split itself. Evidence: lua/claudecode/terminal/snacks.lua:374-377. - INCOMPLETE: for an adopted terminal each entry with a config replaces term._cc.config, so it is not the config captured at open. Evidence: lua/claudecode/terminal/snacks.lua:463-474, lua/claudecode/terminal/snacks.lua:646-647, lua/claudecode/terminal/snacks.lua:747. </details> <details> <summary>lua/claudecode/tools/README.md: 14 corrections with evidence</summary> - FALSE after PR coder#500: handle_invoke uses `params.arguments or {}`, so no Lua error and no -32000 (probe p1: openFile/saveDocument -32602, getDiagnostics []). Also contradicted line 17. Evidence: lua/claudecode/tools/init.lua:88, lua/claudecode/server/init.lua:357, probes/p1_static.out. - FALSE: the script loops over every tests/integration/*_spec.lua with no skip. PR coder#445 (a4d3238) made it run command_args_spec again. Evidence: scripts/run_integration_tests_individually.sh:86. - Misleading: bufnr() finds 'file.txt', 'b/file', './dir/../dir/file.txt' and '' (current buffer). Probes p1 and p5. Evidence: lua/claudecode/tools/save_document.lua:31, lua/claudecode/tools/check_document_dirty.lua:27, probes/p1_static.out, probes/p5_bufnr.out. - INCOMPLETE after PR coder#457: with no stored selection it reads the editor (the bullet above says so), so it does not always return the stored selection. Evidence: lua/claudecode/tools/get_current_selection.lua:37-39, :83-95. - INCOMPLETE: the -32603 table is returned, not raised, so build_response sends it as `{ result = ... }`. Also joins the hard-wrapped bullet like the rest of the file. Evidence: lua/claudecode/tools/close_tab.lua:26-33, lua/claudecode/tools/init.lua:180-182, lua/claudecode/server/init.lua:387. - Format: the merge wrapped a quoted error message across two lines inside a code span, so a search for the message misses it. Every other bullet is one line. Evidence: lua/claudecode/tools/open_diff.lua:56. - Coherence: the inserted sentence split 'finds it' from 'Without one', so 'one' no longer names the loaded buffer. The moved claim is TRUE (probe p1). Evidence: lua/claudecode/tools/open_file.lua:133-140, probes/p1_static.out. - INCOMPLETE: expand_tilde leaves `~user/...` unchanged. Evidence: lua/claudecode/utils.lua:167-181, lua/claudecode/tools/open_file.lua:547. - INCOMPLETE: with makeFrontmost=false the answer is the JSON object, and in the middle of a command openFile appends a suffix. Evidence: lua/claudecode/tools/open_file.lua:735, :741, :746-760, probes/p4_openfile_save.out. - INCOMPLETE: source and code are nil (absent from the JSON) when the diagnostic has none. Evidence: lua/claudecode/tools/get_diagnostics.lua:82-83. - INCOMPLETE: nvim_get_current_tabpage() returns a handle. Probe p1: tabpagenr() 2, handle 3, groupIndex/viewColumn 2/3. Evidence: lua/claudecode/tools/get_open_editors.lua:19, :65-66, probes/p1_static.out. - INCOMPLETE: reload_file_buffers skips a modified buffer, and a diff kept for another client does not close. Evidence: lua/claudecode/diff.lua:2015-2018, :2025-2027, :1104. - INCOMPLETE: no API tells which loaded buffers were opened before their file existed. The loop marks every loaded, named, normal buffer whose file is not readable. Evidence: lua/claudecode/tools/open_file.lua:170-179. - INCOMPLETE (minor): with diff_opts.layout = "unified" diff.lua hands the result to diff_inline, which builds it. Evidence: lua/claudecode/diff.lua:1050-1053, lua/claudecode/diff_inline.lua:526-537. </details> <details> <summary>scripts/README.md: 7 items of the coder#462 verifiers, each checked against the scripts</summary> - The CI paragraph named no job for "the same job". It now names the three jobs of `.github/workflows/test.yml` (`unit-tests`, `integration-tests`, `covered-lock`), says that `integration-tests` runs the runner twice (the second time with a `TMPDIR` that holds a space and a `%`), and says that `Required` needs only `unit-tests` and `integration-tests` (`test.yml` lines 52-80, 98-167, 215-234). - `tla/check-lib.sh` exit precedence: 2 wins over 1, and 1 wins over 3. A stale lock plus a broken rule exits 1. `--hash-only` exits 0 or 3, and `--record` exits 0. A script that sources the lib and ends without `tla_main` turns an exit 0 into exit 2. Probed with a fake `curl` and a fake TLC: default with a broken rule and a stale lock gave rc=1, default with a pass and a stale lock rc=3, a broken `TypeOK` rc=2, `--record` on a stale lock rc=0 (`scripts/tla/check-lib.sh:81-84`, `:226-246`, `:313-333`, `:406-419`). - `tla_init` comes right after `SKILL` and `MODEL`, before `covered_block` (`.agents/skills/verify-diff-lifecycle/check.sh:15-29`, `scripts/tla/check-lib.sh:461`). - `run-release-please.sh` prints nothing itself, and exits 1 with no message when `release-please` is missing. The runner's stdout and file outputs are listed: release-please's own log lines go to stdout (info and debug) and stderr (warnings and errors), the `key=value` lines go to `GITHUB_OUTPUT` or to stdout when it is unset, and `--dry-run` prints JSON after the log lines and still runs Communique. Probed without a token and without network: wrapper rc=1 with no output, and `Error: GITHUB_TOKEN must be set` (`scripts/release-please-runner.js:487-492`, `:555`, `:590`, `:614`). - `--record` and `--hash-only` exit before the TLC jar is fetched, so they never download it and need no `java`. A plain run and `--mutants` do. Probe with an empty cache and a fake `curl`: `--hash-only` and `--record` made 0 `curl` calls, a plain run and `--mutants` made 1 and exited 2 (`scripts/tla/check-lib.sh:452-453`, `:147-151`). - The Lua repros: under `nvim -l` an uncaught error prints `E5113` and exits 1, `cquit N` and `os.exit(N)` exit N, and a bare file name run from `scripts/` fails with `module 'claudecode.diff' not found`. In the `:luafile` form of CI an uncaught error falls through to `cquit 2` (probes on Neovim 0.12.3, and `-l` exit 1 on 0.9.5, 0.10.4 and 0.11.5). - `repro_issue_70.sh` and `repro_issue_277.sh` side effects that the file did not list: work dir names, the `att-home` folder, the empty `/tmp/agent-tty/<8 hex>` socket folder and the `homes.json` entry that `agent-tty` leaves, the inherited environment, the three background probes of 70 and their `PORT.lock` files (a SIGKILL leaves the lock), the unpinned diffview.nvim clone of 277, the state and cache files of `NVIM_APPNAME=issue-277`, the `perl` timeouts, and the nested copy under an existing `issue277-artifacts-latest`. A full run of 277 with private dirs took 32 s. A SIGKILL run left the lock file and 3 processes until `agent-tty destroy`. - `manual_test_helper.lua` calls the handler itself, so no response sender is stored for its coroutine. Any resolution after the handler yields (accept, reject, or `qa!`) logs `No global response sender found for coroutine`. It is expected and harmless (all four CI-form runs exited 0). </details> ## Scope - No code changes. `covered.lock` does not change. - Lines of `scripts/README.md` about `repro_issue_218.sh` stay as they are on `main`. PR coder#458 owns them, and its merge will change them. - I checked every line that this diff changes. Lines that the diff does not touch were not re-verified, except where a verifier found one false while reading its neighbors. Those fixes are in the last correction commit: `server/mock.lua` is required by `tests/unit/server/mock_spec.lua`, the augroup and `utils.lua` lists, the empty `CLAUDE_CONFIG_DIR`, and the Processes bullet. - Probes ran on Linux with Neovim 0.12.3. One probe ran on 0.10.4. The old Neovim claims that earlier lanes proved on 0.8 were not run again. - One claim stays unverified: the sentence in `lua/claudecode/server/README.md` that a client whose EOF the server read in the same read as its request is handled as the code says. Six probe tries did not produce that case. The sentence is a softening, so I kept it. - The terminal README says that the wait before a `close` does not prevent a hang at exit. A probe saw the hang with and without a `close`, so the probe does not prove that the buffer delete causes it. I did not open neovim/neovim#42508 (the host has no network). ### Defects in the code that the verifiers found These need a code fix and a test, so they are not in this docs PR. 1. Accepting a `unified` diff drops one trailing empty line of the proposal: `"a\n\n"` is accepted as `"a\n"` (`lua/claudecode/diff_inline.lua:44-52` and `:531`). The native layout is not affected. A probe shows it. The README says the accepted text is the proposal lines that setup computed. 2. `lua/claudecode/server/tcp.lua:19` says the PRNG is seeded once per process. It is seeded once per load of the module. 3. `lua/claudecode/server/init.lua:59-60` logs "Authenticated WebSocket client connected" from `on_connect`, before the authentication check runs. 4. `lua/claudecode/cwd.lua:36-42` runs the same `git rev-parse` twice. 5. At exit, a pending native diff can stay unanswered. Two native diffs are pending, and the first one (the lower proposal buffer number) is a new file in the current tab with `diff_opts.on_new_file_reject = "keep_empty"` (the default). On `:qa!` its reject deletes its proposal buffer (`lua/claudecode/diff.lua:1171-1175`, `:1523-1524`), Neovim's exit loop stops firing `BufUnload` (`src/nvim/main.c`, the `bufref_valid` check), and the `VimLeavePre` cleanup removes the second diff with no answer. Reproduced on Neovim 0.8.0, 0.9.5, 0.10.4, 0.11.5 and 0.12.3, with and without the server. A separate PR (F13) will make exit answer every pending diff. It will change the exit sentences of this PR: the openDiff bullet in `README.md` (Global Invariants, the sentence that starts "When Neovim exits") and the Augroups bullet in `lua/claudecode/README.md` (the sentences about `BufUnload` and the exception). ## Blast Radius Seven README files. Nothing loads them at runtime. A wrong correction here misleads a reader but breaks no behavior. ## Verification - Six Opus verifiers, one per file (two for the 198 claims of `lua/claudecode/README.md`). Each checked every claim that the diff adds or changes against the code, and every `[file:symbol]` citation, with file and line evidence. Their findings, edits and probe scripts are in the evidence folder of the run. - A second, independent verifier checked the head `bcacd14c` (134 sentences and all seven scripts items, with probes on Neovim 0.8.0 to 0.12.3). It found one false sentence (the exit sentence, now fixed with its exception) and seven wording findings (fixed). It found no other false claim. - Citation check on the final head: 760 citations, links and test paths over the seven files, 1 flagged. The flagged one is `[plugin/claudecode.lua:pcall(require, "claudecode")]`, an expression that `main` already cites in that README. - `mise run all`: exit 0 on the final head `e3e48af1` (1682 successes, 0 failures, 0 errors, 24 pending, `luacheck` 0 warnings and 0 errors in 178 files). `mise run format-check`: exit 0 on the final head (355 files, 0 changed). 1676 successes, 0 failures, 0 errors, 24 pending. `luacheck` reports 0 warnings and 0 errors in 178 files. The format step changes 0 files. - `git merge-tree --write-tree` of the head and `origin/main` (`3a0bb769`) is clean. - The merges of coder#524 and coder#530 changed one sentence of `lua/claudecode/README.md` and merged two conflict hunks. I checked that sentence and the merged bullets against `lua/claudecode/terminal.lua` and `lua/claudecode/selection.lua` at `a41254a4`. I did not run a verifier agent over the merge delta. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
…oder#534) Comment-only change in `lua/claudecode/terminal/snacks.lua`. No behavior changes. The comment above `instance.opts.bo = {}` in `wrap_terminal` said that "the window options that the terminal started with (an older version's, built from the config)" can hold `bo`. That was true before coder#526. coder#526 removed the `window.bo = nil` store from `M.open`, so a start of this version now stores the `bo` of its instance too. I checked it with real snacks.nvim. After `:ClaudeCode` with the snacks provider, `vim.b[buf].claudecode_snacks_window` holds about a dozen window options. The two versions differ only by `bo`: - on `c9e57d1` (before coder#526): no `bo` key - on `3a0bb76` (coder#526 merged): `bo = { filetype = "claudecode" }` The comment now names both sources: a start of this version stores the `bo` of its instance, and an older version's options are built from the config. The reset itself stays, for the same reason as before: Snacks sets `bo` on the buffer again on every `VimResized`, which would fire `FileType` again. ## Validation - `busted tests`: 1509 successes, 0 failures, 0 errors (24 pending). - Integration runner: 331 passed on Neovim 0.12.3, and 244 passed on the 0.8-era build, 0 failures. - One earlier full run on the 0.8-era build printed `FAILED: diff_failed_setup_guards_spec.lua: no plenary summary (nvim exit 0)`. That spec is from coder#529 and this PR does not touch it. It passed 3 of 3 alone on this branch, 2 of 2 alone on a clean `origin/main`, and in a full rerun (244 passed). I did not find the cause of the one-time failure. - `stylua --check lua tests`, `luacheck lua/ tests/`, `treefmt --ci`: clean. - `verify-diff-lifecycle/check.sh`: the lock read STALE because `snacks.lua` is covered as a file. Only the `file` line changed, and no model block did. I re-recorded the lock, and the check passes. ## Notes for the reviewer - `verify-terminal-lifecycle` (coder#525) hashes `snacks.lua` too. coder#525 merges `main` and re-records its `covered.lock` after this PR merges. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
…de terminal lifecycle (coder#525) ## What this adds `.agents/skills/verify-terminal-lifecycle/`: a TLA+ model of the Claude terminal in `claudecode.nvim`, checked by TLC against 34 guards that `check.sh` reads from the Lua code, on the shared harness from coder#450. It covers the `native` and `snacks` providers, the code that finds a Claude after a plugin reload (`:Lazy reload`), the wrapper that adopts a snacks Claude, and the provider choice. A change that removes or rewords a guard makes a rule break, or makes the covered code read STALE (exit 3) until someone confirms the model. The model describes `main` as it is now. The bugs that it found are fixed first: coder#451, coder#464, coder#482 and coder#527 are merged. coder#527 fixed a bug that a review comment on this PR found, and the model has a step for it now. ## The eight rules, as plain sentences | Rule | Plain sentence | | --- | --- | | `AtMostOneClaude` | At most one Claude runs, apart from the one that a close is stopping. | | `CloseStopsClaude` | When `:ClaudeCodeClose` returns, no Claude that ran when it began still runs. | | `CloseNeverReuses` | The plugin never tracks again a terminal that it began to close. | | `OpenShowsLiveClaude` | After an open, a show or a focus, you see a running Claude. A snacks terminal with `auto_close = false` is exempt, on purpose (it keeps an exited Claude). | | `HideKeepsClaude` | Hiding Claude's window keeps Claude running. | | `HideNoError` | Hiding Claude's window raises no error. | | `FailedStartLeavesNoWindow` | A failed start leaves no window, no buffer and no tracked terminal. | | `ExitClosesOnlyOwnWindow` | With `auto_close`, Claude's exit closes only Claude's own window, and never the last window. | ## Bugs this model found The first version of the model broke five rules on seven paths. I replayed each path on a real headless Neovim 0.12.3 (Claude is `sh -c 'sleep ...'`). Updates of the model after those fixes found an eighth and a ninth. Each fix is merged. | # | Rule | Bug | Fixed in | | --- | --- | --- | --- | | 1 | `AtMostOneClaude` | An autocmd that calls open while snacks starts Claude (`BufEnter`, `TermOpen`) started a second Claude. | coder#451 | | 2 | `AtMostOneClaude` | After a plugin reload, the next open started a second Claude (native adopted only a shown terminal, snacks adopted nothing). | coder#464 | | 3 | `CloseStopsClaude` | `:ClaudeCodeClose` after a reload left Claude running. | coder#464 | | 4 | `OpenShowsLiveClaude` | An open between Claude's exit and the scheduled cleanup (native) focused the dead terminal and started no Claude. | coder#451 | | 5 | `OpenShowsLiveClaude` | After `:e file` in Claude's window (native), `:ClaudeCodeOpen` focused your file and Claude stayed hidden. | coder#451 | | 6 | `HideNoError` | The native toggle raised `E444` when Claude's window was the only window. | coder#451 | | 7 | `ExitClosesOnlyOwnWindow` | After a wipe, the native exit cleanup closed the window that showed your file. | coder#451 | | 8 | `OpenShowsLiveClaude` | An exited snacks Claude stayed tracked until its scheduled close, and a Claude that started in that gap lost its Snacks key, so the next reload started a second Claude. | coder#482 | | 9 | `HideNoError` | A `BufEnter` or `TermOpen` autocmd that called `focus_toggle` while native started Claude made the open raise `Invalid window id`, and Claude kept running with no window. | coder#527 | Replays of each bug, against the code before its fix (`replays/`, exit 1 means findings): | Tree | Replays with a finding | | --- | --- | | before coder#451 (`8affa12`) | `snacks-reentrant-open` 2 of 2, `native-open-after-exit` 2 of 2, `native-open-after-swap` 2 of 2, `native-hide-only-window` 2 of 2, `native-wipe-closes-your-window` 1 of 1, plus the reload replays below | | before coder#464 (`14798d1`) | `native-reload-hidden` 1 of 1, `snacks-reload` 2 of 2, `auto-snacks-later` 1 of 2, `native-reload-close` 1 of 1 | | before coder#482 (`3498879`) | `snacks-reload-exit` 16 of 16, `snacks-exit-handlers` 1 of 4 | | this branch | 20 replays, 0 findings (`native-start-autocmd-hide` is new: 18 checks, 10 findings before coder#527 on Neovim 0.12.3 and on the 0.8-era build) | Eight of the 20 replays (`snacks-reload-adopted`, `snacks-reload-keys`, `-tabs`, `-backdrop`, `-older`, `-edit`, `-anchor`, `-focus`) guard the wrapper that coder#482 builds for an adopted snacks Claude: they are no model findings, because the model has no keys, tabs, backdrops or window sizes. Verification of the first drafts of coder#482 found each defect, and each fix landed before coder#482 did. SKILL.md lists them. ## Proof All on this branch (head `a639966`, `main` at `0d55c25` merged), Neovim 0.12.3, Java from mise: - `check.sh`: `main: pass (263060 distinct states found)`, `== RESULT: PASS`, all 34 facts `TRUE`. - `check.sh --mutants` (about 11 minutes on a loaded host): 34 mutant keys (26 single guards and 8 pairs), `== mutants: every guard is caught`, exit 0. Every rule breaks at least once (`AtMostOneClaude` 10, `CloseStopsClaude` 10, `OpenShowsLiveClaude` 9, `CloseNeverReuses` 5, `HideNoError` 3, `FailedStartLeavesNoWindow` 2, `ExitClosesOnlyOwnWindow` 2, `HideKeepsClaude` 1). I ran it on this head. - Scratch break: I removed the `owned.job_ended(terminal.buf)` check from `forget_ended_terminal` in `snacks.lua`. `check.sh` exits 1, `SnacksEntriesForgetEndedJob FALSE`, `main: BROKEN: OpenShowsLiveClaude`. After `git checkout lua`, `git diff --shortstat` is empty and `--hash-only` reads "covered.lock matches the code". - Scratch breaks for the two facts that Codex asked for in round 1: moving the native mark after `nvim_win_set_buf` makes `check.sh` exit 1 with `NativeMarkBeforeTermopen FALSE`, and removing the `jobstop` call of the stop helper in `owned.lua` makes it exit 1 with `OwnedStopOtherStops FALSE`. Both files were restored after each break. - Scratch breaks for the model step and the verifier fixes: with the native.lua from before coder#527, `check.sh` exits 1 (`NativeKeepsHiddenJob FALSE`, `NativeStartSurvivesClosedSplit FALSE`, `main: BROKEN: HideKeepsClaude`). With the `return` deleted from `hide_terminal`, it exits 1 (`NativeHideKeepsLastWindow FALSE`, `main: BROKEN: HideNoError`). The six rewrites that a verifier found to leave a fact TRUE with the guard gone (the adoption, `is_last_window`, the order of `forget_ended_terminal`, `job_ended`, the hide return, `if starting then`) read FALSE now. Files are restored after each break. - `scripts/tla/test-check-lib.sh`: `COUNT cases=44 failed=0 skipped=0`. - Replays: 20 scripts, 0 findings each, exit 0 (see the table above for the code before each fix). `run.sh` exits 2 for a missing Neovim, a replay that raises and one that hangs in `vim.wait` (a replay stuck in a CPU loop can outlive `timeout`'s SIGTERM), and it runs from a path with spaces, commas, pipes and backslashes (the repository and the snacks.nvim checkout). - `treefmt --ci` (stylua, prettier, shfmt -i 2, shellcheck, actionlint, zizmor): 383 files, 0 changed. `busted tests`: 1529 successes, 0 failures, 25 pending. `mise run test` (the CI file set, coverage, seed 1794460250): 1702 successes, 0 failures. luacheck: 0 warnings. - `covered.lock` is re-recorded on this head, which merges `main` at `0d55c25` (it had been recorded at `37eaa0f`). Changed since then in the covered files: `terminal.lua` (a warning message of coder#530, file line only), `native.lua` (coder#527, block `open_terminal`) and `snacks.lua` (coder#526 dead stores, block `snacks_open` and the wrapper blocks, and the comment of coder#534). I read each diff: none changes a guard that a fact reads, and every fact reads TRUE except for the one that coder#527 moved (`NativeKeepsHiddenJob`, updated). `--hash-only` reads "covered.lock matches the code" (about 10 s). ## Run it ```bash .agents/skills/verify-terminal-lifecycle/check.sh # about 1 min (30 to 50 s) .agents/skills/verify-terminal-lifecycle/check.sh --mutants # about 12 to 15 min, after you edit the model or a fact .agents/skills/verify-terminal-lifecycle/check.sh --hash-only # about 10 s, only compares covered.lock with the code SNACKS_NVIM=<snacks.nvim checkout> NVIM=<path to nvim> \ .agents/skills/verify-terminal-lifecycle/replays/run.sh snacks-reload-keys.lua ``` CI runs every `.agents/skills/verify-*/check.sh` in the `covered-lock` job, as for `verify-diff-lifecycle`. ## Notes for the reviewer - The diff is one new skill folder (SKILL.md, `check.sh`, `covered.lock`, `model/` with the TLA+ spec and a `/statechart` view, and `replays/`) and one sentence in `lua/claudecode/terminal/README.md`. The sentence says that a float of an older version has no backdrop "to hide or to show" until Snacks re-creates it (the text said only "to hide"). It touches no Lua code. - The skill does not model the items that SKILL.md lists under "Scope and bounds", each with what you would see if it broke. They include the `external`, `none` and custom table providers, a close that starts during another close's wait, more than one open or toggle per start from an autocmd, a `WinNew` or `WinEnter` autocmd that calls an entry while native's `vsplit` runs before the buffer has its mark (two Claudes run; open PR coder#544 proposes a fix), which window the plugin made (an exit with `auto_close` closes a window of yours that shows the terminal buffer), a cleanup that raises (`E444` in a failed start's window close), a `TermClose` autocmd of your own that closes the terminal, Snacks floats, tab pages, window sizes, a second reload, `:bdelete`, `:q` in Claude's window, and Neovim exit. It assumes Snacks' `fixbuf`, so `:e` in a snacks window is no step. - `DEVELOPMENT.md` is not edited here: the skill-listing change belongs to the PR that owns it. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
Six guards in
lua/claudecode/terminal/snacks.luahad no test that fails without them, and four assignments, in two statements, did nothing. This PR adds the tests and removes the assignments.I found the six by deleting each guard in turn and running the 372 terminal tests. All six deletions passed. Each guard now has a test that fails when the guard is gone.
snacks.luatests/unit/terminal/snacks_reload_spec.luaregister_window_events:_onis a function_onmust not break hide and showskips the registration when Snacks has no _onregister_window_events:fixbufis a functionfixbufskips the registration when Snacks has no fixbuffind_backdrop: backdrop is one z-index below the floatleaves a window alone that sits at another z-indexfind_backdrop: backdrop buffer has the backdrop filetypeleaves a window alone that shows no backdrop bufferfind_backdrop: the terminal's window has a z-indexrelative = "", no z-index) has no backdropleaves a window alone when the terminal's window has no z-indexkeysE5100stores the window options without the keysThe test double for
Snacks.terminal.opennow also gives the instance thekeysthat Snacks resolves. The last test needs them.Four assignments, in two statements, were dead, not untested.
win_opts.keys, win_opts.bo = built.keys, nilinwrapper_options(win_opts.bo) setbotonil.wrap_terminalandupgrade_wrapperresetopts.boright after the constructor, so nothing reads thatnil.window.keys, window.on_buf, window.on_win, window.bo = nil, nil, nil, nilinM.open(window.on_buf,window.on_win,window.bo):plainhas dropped the functions (on_buf,on_win) already, and the same two resets coverbo. Onlywindow.keys = nilhas an effect (the row above), so it stays.A probe that removed each of them changed no test result and no behavior. I removed them and corrected the comment on the reset that does the work: Snacks sets
boon the buffer again on everyVimResized, which would fireFileTypeagain, so the reset must run right after the constructor. The two resets themselves (wrap_terminalandupgrade_wrapper) were already caught by tests.Validation
busted tests: 1496 successes, 0 failures, 0 errors (22 pending).stylua --check lua tests,luacheck lua/ tests/,treefmt --ci: clean.verify-diff-lifecycle/check.sh: PASS. The lock is re-recorded in this PR becausesnacks.luachanged. Only thefileline changed, and no model block did.Notes for the reviewer
verify-terminal-lifecycle(feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle #525) also coverssnacks.lua. Whichever of the two merges second must mergemainand re-record itscovered.lock.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh