Repository navigation
feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle - #525
Merged
Merged
Conversation
…de terminal lifecycle The model covers the native and snacks providers, the code that finds a Claude after a plugin reload, the wrapper that adopts a snacks Claude, and the provider choice. It checks eight rules against 32 guards that check.sh reads from the Lua code. Nineteen replays drive the real plugin in a headless Neovim. covered.lock is recorded in the next commit.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
🛡️ 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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 383f22bf2c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…the stop helper of owned.lua Codex round 1 on #525. The fact NativeMarkBeforeTermopen checked only that the mark precedes termopen, but a BufEnter autocmd fires at nvim_win_set_buf, so the fact orders the mark before that call too. The model's StopAll step relied on owned.stop_other and stop_buffer without reading them: the new fact OwnedStopOtherStops reads the loop and the stop, wait and delete of the buffer, and the model's StopAll step depends on it.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3b6b65c291
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
- check.sh: SnacksAvailabilityCached no longer reads load_provider's own providers table. require keeps the module, so that table is a second cache, and a refactor that drops it left the fact FALSE while the behavior stayed cached. - SKILL.md: say what the facts read. get_active_bufnr adopts and runs forget_ended_terminal too, but no fact reads it, and the model has no step for it, because none of the eight rules depends on which entry adopts first. - replays/run.sh: exit 2 for a Neovim that is not there, and for a snacks.nvim checkout without Snacks.terminal. - model/statechart-view.ts: name a state where snacks.nvim became loadable after the module loaded, because the view cannot read SnacksAvailabilityCached.
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 12, 2026
… four dead window option assignments (coder#526) Six guards in `lua/claudecode/terminal/snacks.lua` had 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. | Guard in `snacks.lua` | What it protects | New test in `tests/unit/terminal/snacks_reload_spec.lua` | | --- | --- | --- | | `register_window_events`: `_on` is a function | A Snacks without `_on` must not break hide and show | `skips the registration when Snacks has no _on` | | `register_window_events`: `fixbuf` is a function | Same, for `fixbuf` | `skips the registration when Snacks has no fixbuf` | | `find_backdrop`: backdrop is one z-index below the float | A window at another z-index is not the backdrop | `leaves a window alone that sits at another z-index` | | `find_backdrop`: backdrop buffer has the backdrop filetype | A window with another buffer is not the backdrop | `leaves a window alone that shows no backdrop buffer` | | `find_backdrop`: the terminal's window has a z-index | A split (`relative = ""`, no z-index) has no backdrop | `leaves a window alone when the terminal's window has no z-index` | | the stored window options leave out `keys` | A buffer variable cannot hold a table that mixes list and map keys (a Snacks key does), which fails with `E5100` | `stores the window options without the keys` | The test double for `Snacks.terminal.open` now also gives the instance the `keys` that Snacks resolves. The last test needs them. **Four assignments, in two statements, were dead, not untested.** - `win_opts.keys, win_opts.bo = built.keys, nil` in `wrapper_options` (`win_opts.bo`) set `bo` to `nil`. `wrap_terminal` and `upgrade_wrapper` reset `opts.bo` right after the constructor, so nothing reads that `nil`. - `window.keys, window.on_buf, window.on_win, window.bo = nil, nil, nil, nil` in `M.open` (`window.on_buf`, `window.on_win`, `window.bo`): `plain` has dropped the functions (`on_buf`, `on_win`) already, and the same two resets cover `bo`. Only `window.keys = nil` has 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 `bo` on the buffer again on every `VimResized`, which would fire `FileType` again, so the reset must run right after the constructor. The two resets themselves (`wrap_terminal` and `upgrade_wrapper`) were already caught by tests. ## Validation - `busted tests`: 1496 successes, 0 failures, 0 errors (22 pending). - Integration runner: 316 passed on Neovim 0.12.3 and 229 on the oldest supported build (0.8 era), 0 failures. - `stylua --check lua tests`, `luacheck lua/ tests/`, `treefmt --ci`: clean. - `verify-diff-lifecycle/check.sh`: PASS. The lock is re-recorded in this PR because `snacks.lua` changed. Only the `file` line changed, and no model block did. - Each new test fails when I delete its guard (checked by mutation). The four dead assignments change no result when put back. ## Notes for the reviewer - `verify-terminal-lifecycle` (coder#525) also covers `snacks.lua`. Whichever of the two merges second must merge `main` and re-record its `covered.lock`. - No behavior changes for users. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
…e verifiers of verify-terminal-lifecycle The model's autocmd step now calls open or a toggle while a start runs (AutocmdCalls). A native focus_toggle there adopts the half-started terminal and hides its split, and the start then read a window that was gone (#527). Finish raises (HideNoError) unless the new fact NativeStartSurvivesClosedSplit reads the guards of #527. NativeKeepsHiddenJob reads both bufhidden=hide assignments of #527: the early one, so that a window that closes during the start never unloads the buffer, and the late one, which overrides an autocmd of the start. The model reaches the kill that the early one prevents (a TermOpen hide with 'nohidden' ends Claude). The replay native-start-autocmd-hide.lua runs the forms on real Neovim, 18 checks. Verifier fixes: six facts that a rewrite of the guard could leave TRUE now read the guard (the adoption returns only for a missing buffer, is_last_window ends with return true, each native entry runs forget_ended_terminal before it looks at the terminal, job_ended is owned's, hide_terminal returns for the last window, snacks M.open returns at once under `starting`), with a followed_by helper for adjacent lines. SnacksAvailabilityCached no longer needs load_provider's own table. SKILL.md says what the facts read, what you would see for each thing it does not model, and the corrected counts. statechart-view.ts shows a healthy close wait as busy. replays/run.sh exits 2 for a missing Neovim, a replay that raises and one that hangs.
…efore the mark
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aff01dbba7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
- replays/run.sh passes the repository, the snacks.nvim checkout and the replay to Neovim through the environment and a Lua call, not through `set rtp^=` and `luafile`. A path with a space, a comma, a pipe or a backslash was split or cut by those Ex commands. - SKILL.md names two things the model does not check, with what you would see: which window the plugin made (an exit with auto_close closes a window of yours that shows the terminal buffer, which ExitClosesOnlyOwnWindow cannot tell), and a cleanup that raises (the facts read the order of calls, so a failed start whose window close raises E444 leaves its buffer behind).
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 06907c1f94
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
- replays/run.sh makes SNACKS_NVIM and NVIM absolute before it changes into the work directory. A relative SNACKS_NVIM made the Snacks provider unavailable, and a replay could exit 0 on the native fallback without exercising Snacks. - native-start-autocmd-hide.lua shell-quotes the log path in the claude script that it generates. - snacks-reload-backdrop.lua requires a shown float with one backdrop after a show step, so a show that leaves no window is a finding. - model/statechart-view.ts marks a state broken when a closed terminal is tracked again or a failed start leaves a window, a buffer or tracked state, as it does for `bad`.
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
|
Codex Review: Didn't find any major issues. 🚀 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. |
4 tasks
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…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`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
… split (coder#527) A `BufEnter` or `TermOpen` autocmd that calls `focus_toggle` while the native provider starts Claude makes `:ClaudeCode` raise `Invalid window id: <n>` at `native.lua:263`. Claude keeps running, but no window shows it, and the error reaches the user. This PR makes the start survive that. I found this while answering a Codex review comment on coder#525 (the `verify-terminal-lifecycle` skill), which asked the model to cover an autocmd that calls a toggle during a native start. ## What happens 1. `open_terminal` creates the split and the buffer, and marks the buffer. The mark goes before `termopen` on purpose, so that an `open()` from a start-time autocmd adopts this terminal and starts no second one. 2. `nvim_win_set_buf` fires `BufEnter`, and `termopen` fires `TermOpen`. Neither has set `bufnr` or `winid` yet. 3. The autocmd calls `focus_toggle`. It finds no tracked terminal, adopts the marked, half-started buffer, sees that its window is the current one, and calls `hide_terminal`. The split closes. 4. `open_terminal` goes on and calls `nvim_win_get_buf(new_winid)` on the closed split. Neovim raises. Any other way to close the split during the start does the same: a second `simple_toggle` from the autocmd, or a plain `:close`. ## The fix `open_terminal` no longer assumes that its split survives the start (`lua/claudecode/terminal/native.lua`): - It reads the buffer of the split only while the split exists. - It sets `winid = new_winid` and `bufnr = new_bufnr`, then calls `is_valid()`, which looks for the window that shows Claude now. If the autocmd hid Claude and nothing showed it again, no window shows it: Claude runs as a hidden terminal, and the next toggle shows it. If a later autocmd of the start showed it again in another window, that window is the tracked one. - It focuses the terminal only when a window shows it and the start was asked to focus, and then enters insert mode as before. Otherwise it returns to the window where you started. - It sets `bufhidden=hide` on the new buffer before it shows it. It also keeps the assignment after `termopen`, which overrides an autocmd of the start that changed `bufhidden` (to `wipe`, for example), so a later hide still keeps the job. With `'nohidden'`, a window that closes during the start unloads a buffer that is not `bufhidden=hide`. In `BufEnter`, Neovim then loads the buffer again before `termopen`, and on 0.8 its `term://` reader starts a second terminal in it: a bare `claude`, with no arguments, no plugin env and no IDE connection, which the plugin then tracks and sends text to. In `TermOpen`, the unload ends Claude and the start reports "Failed to open native terminal". The verifier of this PR found both. This is the same defense that the function already has for an autocmd that swaps another buffer into the split or wipes the buffer. `terminal/README.md` describes the new branches. I kept `focus_toggle` as it is: from inside a window that shows the terminal it hides the terminal, also during a start. So after such an autocmd, Claude usually runs hidden (also with `'nohidden'`, because of the `bufhidden` line), and `:ClaudeCodeFocus` or `:ClaudeCode` shows it again. ## Snacks has no such gap The snacks provider tracks its terminal only after `Snacks.terminal.open` returns, and a `starting` flag makes a nested `open` return. I ran the same shape against real snacks.nvim: a `BufEnter` or `TermOpen` autocmd that calls `focus_toggle`, `simple_toggle` twice, `close`, or closes the window. 8 of 8 start without an error, run at most one Claude, and track the one that runs. I did not change `snacks.lua`. ## Tests 11 new tests in `tests/unit/native_terminal_toggle_spec.lua`: - 6 tests, each for a `BufEnter` and a `TermOpen` autocmd that calls `focus_toggle`, calls `simple_toggle` twice, or closes the window. Each calls `open` under `pcall` and asserts that it raises nothing, that one job runs and is tracked, that no window shows it, that a later `simple_toggle` shows it, and that no second Claude starts. - 2 tests, for a `BufEnter` and a `TermOpen` autocmd that calls `simple_toggle` three times (adopt, hide, show again in another window). They call `open` directly, so a raise fails them too. They check that one window shows Claude, that you are in it, and that the exit of the job closes it with `auto_close`. - 2 tests with `'nohidden'` (a `BufEnter` autocmd that closes the split, a `TermOpen` autocmd that calls `focus_toggle`): one job runs, no "Failed to open" notice, Claude is tracked and hidden. The mock unloads a buffer that is not `bufhidden=hide` when its last window closes with `'nohidden'`, and loads it again with a second job, as the 0.8 reader does. - 1 test: a `TermOpen` autocmd sets `bufhidden=wipe` on the new buffer, and the start must leave `bufhidden=hide` on it. The tests make `nvim_set_current_win` raise for a window that is gone, as Neovim does. - On `c9e57d1` (main), the first 10 fail (9 of them with `Invalid window id: 1000`). The `wipe` test passes on main, which sets `hide` after `termopen`, and it guards that this PR keeps that line. - With the fix, all 11 pass. I removed each changed guard in turn (the `nvim_win_is_valid` check before `nvim_win_get_buf`, the `is_valid()` rescan, the `focus and winid` check, the early `bufhidden` and the late one): each removal makes tests fail. The rescan alone fails both hide-and-show tests. I also ran the same cases as a replay against real Neovim, with `sh -c 'sleep 60'` standing in for Claude: the 6 cases above, the hide-and-show case, then a toggle that shows Claude again (16 checks), and the 2 `'nohidden'` cases (18 checks in all). The `'nohidden'` cases use a script named `claude` that logs each start. On `c9e57d1` the replay has 10 `BUG` lines on Neovim 0.12.3 and on the 0.8-era build (on the 0.8-era build, `'nohidden'` starts Claude twice). With the fix it has 0 findings on both. The replay goes into the skill folder in coder#525 once this merges. ## Validation - `busted tests`: 1520 successes, 0 failures, 0 errors (24 pending), on the head merged with `main` at `036427a`. - Integration runner: 331 passed on Neovim 0.12.3, 244 passed on the 0.8-era build, 0 failures. - `stylua --check lua tests`, `luacheck lua/ tests/`, `treefmt --ci`: clean. - `verify-diff-lifecycle/check.sh`: the lock read STALE because `native.lua` is covered as a file. Only the `file` line changed, and no model block did. The change cannot reach diff state (it only affects how `open_terminal` tracks its own window after a start). I re-recorded the lock, and the check passes. ## Notes for the reviewer - A nested `close()` from a start-time autocmd still cancels the start (it notices the wiped buffer and sends the existing "Failed to open native terminal. Its buffer was deleted" notice). That path was already designed and tested, and I left it alone. On the 0.8-era build, a `close()` from a `TermOpen` autocmd crashes Neovim (`corrupted double-linked list`, segfault, exit 139), on `main` and with this fix alike. - Found while verifying this PR, and not changed here: an autocmd of `WinEnter` or `WinNew` that fires during the `vsplit` of the start, before the buffer is marked, can call a toggle or `open` that starts a second Claude, and a `:close` there makes Claude take your only window. A follow-up PR handles that start-up window (`fix/native-start-reentry`). - `verify-terminal-lifecycle` (coder#525) covers `native.lua`. After this PR merges, coder#525 merges `main`, re-records its `covered.lock`, and adds the model step and the replay. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…it (coder#544) Two ways an autocmd could interrupt a native start still broke it after coder#527, and a third broke a hide later. This PR fixes all three. I found the first two while verifying coder#525 and coder#527 (the verifiers of both PRs reproduced them on `main`). This is round 7. The maintainer allowed one review round past the cap of six for this push (the [waiver](coder#544 (comment))). Round 3 of this PR ran the `vsplit` under `:noautocmd`. Both verifiers of that head (`a7b86897`) found the same blocker: `:noautocmd` skips `WinLeave` of the window you leave, so a `WinLeave` autosave (`autocmd WinLeave * silent! update`) no longer saved the file before Claude started (7 of 8 cases, on both Neovim builds). Round 4 dropped `:noautocmd`, so no autocmd is skipped any more. Round 5 (`fdb2b082`) got two blockers from the verifier (the skill's runner could not run the new replay, and a close right after `termopen` ended Neovim in a few runs in 100 under load) and three P2 findings from Codex. Round 6 (`a171a86f`) fixed both blockers and two of the three P2 findings, and Codex found no major issue. The verifier of `a171a86f` then returned ISSUES, all about the wait that round 6 added to `close_terminal` (it asked `nvim_get_proc` for the name of the child, and `nvim_get_proc` runs `ps` on Unix): (1) where `ps -p` does not work, every native close raised after it had cleared its state, so Claude kept running untracked and the next open started a second one. (2) A close from a `TermClose` autocmd raised `Invalid 'pid'` on a job that had exited, and no test covered the guard. (3) Every close cost 100 to 190 ms (1.1 to 1.3 s for a child named `nvim`). (4) No test covered the limit of the wait. (5) The docs gave a failure rate that the verifier could not reproduce, and none of them named the `ps` call or its cost. This push fixes all five (see "The fix" and "Tests"). ## What breaks 1. **Two Claudes.** The `vsplit` of a start fires `WinLeave`, `WinNew` and `WinEnter`, and creating the buffer fires `BufNew` and `BufAdd`, all before the plugin has marked a buffer for Claude. An `open`, `simple_toggle` or `focus_toggle` that such an autocmd calls finds nothing to adopt and starts a second Claude. Nothing tracks it, and a close returns with one still running. (A verifier found the `BufNew`/`BufAdd` form: 60 of 64 cases on `main`.) 2. **A close in the middle of `termopen`.** A `close()` from a `BufEnter` or `TermOpen` autocmd cancels the start with a "Failed to open native terminal" error, and a `close()` from a `TermOpen` autocmd waits for the job inside `termopen`. On the 0.8-era build, that wait aborts Neovim (`corrupted double-linked list`, segfault, exit 139). 3. **A hide that ends Claude.** An autocmd of yours can change `bufhidden` after the start (a `TermEnter` autocmd that sets `wipe`). The next hide closed the window, which wiped the buffer and ended Claude. (The verifier of coder#527 found this; coder#527 sets `hide` again after `termopen`, but not at the hide.) 4. **A hide that raises.** The write of `bufhidden` in a hide fires `OptionSet`, and an autocmd of that event can end Claude (`close()`), hide it or show it again. The hide then closed `winid`, which was `nil` (`Invalid 'win'`) or the window that a nested toggle had shown. This came with the fix of 3 (Codex found it in round 4). Codex then found a second form in round 5: an autocmd shows a file of yours in Claude's window, and the hide closed your window. 5. **A close right after a start ends or hangs Neovim.** A job that was just started is still a fork of Neovim until its child runs `exec`. A `jobstop` on it ended Neovim with `SIGHUP` (exit 1), or left it hanging in the buffer delete. A close that an autocmd of a start asked for (item 2) stops the job right after `termopen`, and so does `open()` followed by `close()` in one call, which also does it on `main`. On my host it happened in 6 of 1260 runs at a load average of 50 to 100 (7 orders: the three autocmd closes and `open()` then `close()`, on both builds). The verifier saw 62 of 1120 at a median load of 105, and 0 of 1120 with the wait. **Not in this PR** (each is a follow-up after this PR, with its own tracking issue): - An autocmd of `WinNew`, `WinEnter` or `WinLeave` that closes the new split, or moves to another window, still makes the start take the window you are in (as on `main`). The fix needs a proof of which window the plugin made, and it goes with the change that makes the exit close only a window that the plugin made. - A plugin reload from inside an autocmd of a start (Codex round 5): the new module copy has `starting = false` and no marked buffer yet, so it can start a second Claude. `main` has the same gap. The fix needs a start flag that survives a reload, the pending close request, and a model with separate module generations. - Two notes of the verifier about an `OptionSet` hide (on the 0.8-era build, and that `OptionSet` runs with Claude's window current). ## The fix (`lua/claudecode/terminal/native.lua`) - **`open_terminal` returns while a start runs** (`if starting then return end`). The start makes the one Claude, so an entry that one of its autocmds calls does nothing. The `vsplit` keeps every autocmd. This fixes 1. - **`close_terminal` waits for the exec, only for a job that was just started.** `job_started_at` records when `termopen` returned. A close of a job that this module started less than 10 s ago waits up to 1 s (a terminal adopted after a plugin reload has no start time and does not wait) (checked every 5 ms) until the child of the job has the name of its command, not the name of Neovim, and then calls `jobstop`. An older job calls `jobstop` at once, with no lookup. A job that already exited has no pid (`jobpid` raises), so the wait does not run. The names come from `/proc/<pid>/comm` (a read of a few bytes) where `/proc` exists. Elsewhere (macOS, the BSDs) `nvim_get_proc` gives them, which runs `ps`, under `pcall`: when no name can be read (`ps` is missing, or it fails), the close goes on to `jobstop` as before, with no wait and no raise. This fixes 5, and the five findings of the verifier (the `ps` raise, the guard, the cost, the limit). - A `close()` during a start sets `close_after_start`, and the start runs it when it returns. It no longer waits inside `termopen`. If the start raises after the job started, the close still runs first, and then the error of the start propagates. This fixes 2. - `open_terminal` is now a small wrapper that calls `start_terminal` under `pcall`, so an error of the start cannot leave `starting` set (which would defer every later close). The old body of `open_terminal` is `start_terminal`. - `hide_terminal` sets `bufhidden=hide` before it closes the window, and only when it is not `hide` already, because a write of the same value fires `OptionSet`. This fixes 3. After the write it looks at the window again, and it returns when `winid` changed, when its window is gone, when it shows another buffer than Claude's, or when it became the last window. This fixes 4. **Behavior effects:** no autocmd is skipped. An entry that a start's early autocmd calls does nothing, where it started a second Claude. A `close()` that an autocmd of the start calls returns before Claude stops, and Claude stops when the start returns. `terminal/README.md` says so. ## Tests 29 new tests in `tests/unit/native_terminal_toggle_spec.lua` (101 before, 130 now). The mock gets a hook that runs an autocmd inside the `vsplit`, one that runs it inside `nvim_create_buf` (`BufNew`, `BufAdd`), one that runs an `OptionSet` autocmd inside a write of `bufhidden`, a strict `nvim_get_proc` (it raises for a pid that is not a number, like `ps -p` with a bad pid, and counts its lookups), `getpid`, `vim.loop.hrtime`, and a stub of `/proc/<pid>/comm` that a test can switch off (`io.open`, set with `rawset` as the other specs do). The shared mock `tests/mocks/vim.lua` gets `loop.hrtime`. - An entry (`open`, `simple_toggle`, `focus_toggle`) that a `WinLeave`/`WinNew`/`WinEnter` autocmd of the split or a `BufNew`/`BufAdd` autocmd of the new buffer calls: one Claude runs, tracked, in one window, with no notice (6 tests). - A `vsplit` that raises does not leave `starting` set (1). A start that raises after the job started leaves a Claude that a close still stops (1). A close that an autocmd asked for during such a start still runs before the error propagates (1), and the error of the start is the one that propagates when the close raises too (1). - `close()` from a `BufEnter` or `TermOpen` autocmd: Claude stops after the start, with no notice, no window and no buffer left (2). The next open starts Claude again after a close that waited for the start (1). - A close of a job that was just started (7 tests): `jobstop` comes only after the exec, with the name from `/proc` (1) and from `nvim_get_proc` (1). The wait ends at its limit when the child never runs `exec` (1). A close where no name can be read (no `/proc`, `ps` missing) goes on to `jobstop` with no wait and no raise (1). A close of a job that exited (`jobpid` raises) makes no lookup (1). A close of a job older than 10 s makes no lookup (1). A close that an autocmd asked for during a good start raises the error of that close (1). - A hide after `bufhidden` was changed to `wipe`: Claude keeps running, and a toggle shows it again (1). A hide that finds `bufhidden` already `hide` writes nothing (1). - An `OptionSet` autocmd of `bufhidden` that runs inside the hide: it calls `close()` (Claude stops, nothing raises), a nested `simple_toggle` or `focus_toggle` (Claude stays hidden), hides and shows Claude again (the new window stays), closes Claude's window itself, closes every other window (the window stays), or swaps a file of yours into Claude's window (the window stays and shows your file). That is 7 tests. On `main` (`5c7a4db9`), 20 of the 29 fail (19 failures and 1 error). The other 9 guard state that the fix introduces. I removed each guard in turn (the `starting` return, setting `starting`, resetting it, the deferral, running the deferred close, resetting `close_after_start`, the `pcall`, the hide-time `bufhidden`, writing it only when it differs, and which error propagates (also when the start went well), the four clauses of the look at the window after the write, the wait for the exec, the condition of that wait, the `jobpid` guard, the 10 s rule, the limit of the wait (1000 ms to 1 ms), the `pcall` around `nvim_get_proc`, the read of `/proc`, and the own name): each removal fails a test. ## On real Neovim I ran the verifiers' own probe scripts against this head, the old head `a7b86897` and `main`, on Neovim 0.12.3 and the 0.8-era build, with `set hidden` and `set nohidden`. Claude is the repo's stub `tests/bin/claude`. - **Autosave on `WinLeave` or `FocusLost,WinLeave`** (`autosave-probe.lua`, 8 cases per configuration): the file is saved before Claude starts in 8 of 8 on every configuration. `main` also saves 8 of 8. The old head left it stale in 7 of 8 (a control run on 0.12.3 with `set hidden`; the verifiers saw 7 of 8 on every configuration). - **User impact** (`design-probe.lua`: event traces and 7 user setups): the output is byte-identical to `main` on both builds (37 lines each). The old head differed in 15 setup rows. - **Start matrix** (`start-matrix-d.lua`): 7 events (`WinNew`, `WinEnter`, `WinLeave`, `BufEnter`, `BufWinEnter`, `TermOpen`, `TermEnter`) × 8 actions (`focus_toggle` once and twice, `simple_toggle` once and twice, `close()`, `ensure_visible()`, `open()`, `setlocal bufhidden=wipe`) × 4 entries × 2 follow-ups, in 4 configurations: 0 cases with two Claudes, 0 untracked, 0 where a hide ended Claude. I left out the three actions that close or wipe the split (`:close`, `:bwipeout`, `:bwipeout!`): they show the item that is not in this PR (the start takes your window, `USER-FILE-GONE`), as on `main`. On the 0.8-era build the groups of a `TermEnter` autocmd that hides or closes the window segfault (exit 139). The verifiers showed that on `main`, and in plain Neovim 0.8 without this plugin. I see the same exit 139 on this head. - **`BufNew` and `BufAdd`** (4 actions × 2 events): 60 cases with two Claudes on `main`, 0 on this head. - **Close right after a start** (a probe that runs 7 orders: a `close()` from a `BufWinEnter`, `BufEnter` or `WinLeave` autocmd of the start, and `open()` followed by `close()` in one call, on both builds, `hidden` and `nohidden`; 12 runs at a time, with the stub `claude`): without the wait, 6 of 1260 runs ended with `Caught deadly signal 'SIGHUP'` (exit 1, at a load average of 50 to 100). With the wait of this head (`/proc`, young jobs only), 0 of 1750 runs did, and none hung or left a Claude running (36 CPU burners, load average 33 to 88). - **Cost of a close** (`close-latency.lua`, 1 start and 1 close of a settled Claude, real Neovim, load average 20 to 30): `main` 1.7 ms, `a171a86f` 180 to 400 ms, this head 1.0 to 3.8 ms. - **Replay** `native-start-reentry.lua` (new, in `verify-terminal-lifecycle`; 25 checks: the 15 entries, the autosave, both `close()` cases, the `wipe` hide, 5 `OptionSet` hides that call `close`, `simple_toggle`, `focus_toggle`, hide and show, or swap a file in, and a close when no process name can be read: no `/proc`, empty `PATH`): `NVIM=<nvim> .agents/skills/verify-terminal-lifecycle/replays/run.sh native-start-reentry.lua` exits 0 with 0 findings on both builds. The replay shows 23 findings on `main`, 21 on the `:noautocmd` head (`a7b86897`), and 1 on `a171a86f` (the new check: the close raises `ENOENT` for `ps` and leaves Claude running). The `OptionSet` checks run after startup (`lib.after_startup`), because Neovim fires no `OptionSet` during its startup. `run.sh` now waits for a replay that announces this, where it ran `cquit 2` right after the file loaded. At times the host ran at a load average of 50 to 100, and a few matrix groups then died or showed a `DEAD-WINDOW-LEFT` flag in a "then exit" follow-up. I reran each of those groups on its own, and none of them showed a flag. ## `verify-terminal-lifecycle` The skill is on `main` now (coder#525), so this PR updates it: - The model has a phase `begin` (the `vsplit` and the new buffer exist, the buffer has no mark) and the step `SplitRuns`. `AutocmdCalls` can run in `begin`. A new step `CloseDuringStart` records a close that an autocmd asked for, and `StartReturns` runs it like a typed close. The new fact `NativeOpenSkipsDuringStart` reads `if starting then return` and the `starting = true` / `starting = false` pair around `pcall(start_terminal, ...)`. Without it, the model starts a second Claude and breaks `AtMostOneClaude`. `NativeMarkBeforeTermopen` and `OwnedUnstartedIsNotEnded` now pair with it, because the guard also covers the entry that they covered. The new fact `NativeRunsDeferredClose` reads the `close_requested` block of `open_terminal`. Without it the request is lost and the Claude that the start made runs on, which breaks `CloseStopsClaude`. The deferral in `M.close` (`if starting then close_after_start = true`) stays a documented limit in `SKILL.md`: the model has no wait nested in a start, so it cannot show the close that waits inside `termopen`. `native_terminal_toggle_spec.lua` and the replay test that half. - The facts that read the start now read `start_terminal`, and `close_terminal` is a forward-declared `function close_terminal()`. - `check.sh` passes (279,492 states, was 263,060), and `--mutants` shows every one of the 36 keys caught (26 single, 10 pairs). `SKILL.md` has bug 10 and the replay row, drops the not-modeled item that this change fixes, and lists the wait for the exec as not modeled (the model has no processes). - `run.sh` quits with 2, as before, for a replay that raises, one that returns without calling `lib.after_startup`, and one that hangs for 60 s (I ran all three). - I re-recorded both locks (`verify-terminal-lifecycle` and `verify-diff-lifecycle`; for the diff skill only the `file` line of `native.lua` changed). ## Validation Run on `ec480c7e`, the head of this push (it includes `main` at `0a4ebbbc`, and all four skill locks match): - `busted tests`: 1662 successes, 0 failures, 0 errors (33 pending). - Integration runner: 637 passed on Neovim 0.12.3 and 619 on the 0.8-era build, 0 failures. - `mise run check` (syntax, `luacheck`, the static proofs of `verify-claudecode-nvim`), `stylua --check lua tests`, `treefmt --ci`: clean (`luacheck`: 0 warnings in 193 files). - `verify-terminal-lifecycle/check.sh`: PASS (279,492 states), `--mutants`: every guard is caught (36 keys, 26 single and 10 pairs; run on `abdb9157`, and the merge of `main` since then changes no file that the skill reads). `verify-diff-lifecycle`, `verify-mention-queue` and `verify-selection-tracking` hash checks: pass. - Replay `native-start-reentry.lua`: 25 checks, 0 findings on Neovim 0.12.3 and on the 0.8-era build. ## Notes for the reviewer - Merges of `main` since `30c57e3b` also changed other skills, the diff code and its tests, scripts, `fixtures/` (the issue-218 configs), `mise.toml`, and docs including `AGENTS.md`. coder#569 changed `lua/claudecode/terminal.lua` (the cwd of a terminal) and its lock lines. None of the merges changes `lua/claudecode/terminal/`. - A close during a start is deferred, so `:ClaudeCodeClose` from such an autocmd returns before Claude stops. It stops when the start returns, in the same call stack, and also when the start raises after the job started. - Rounds so far: Codex rounds 1 to 3 (a P1 that "the window that did not exist before the `vsplit`" proves nothing, a P2 about a close that is deferred past a raised start, then a clean round 3), then the two verifiers blocked on `:noautocmd`. Round 4 (`29345666`) got two Codex P2 findings, round 5 (`fdb2b082`) got two verifier blockers and three Codex P2 findings, round 6 (`a171a86f`) got a clean Codex round and the verifier ISSUES that this push (round 7) answers. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this adds
.agents/skills/verify-terminal-lifecycle/: a TLA+ model of the Claude terminal inclaudecode.nvim, checked by TLC against 34 guards thatcheck.shreads from the Lua code, on the shared harness from #450. It covers thenativeandsnacksproviders, 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
mainas it is now. The bugs that it found are fixed first: #451, #464, #482 and #527 are merged. #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
AtMostOneClaudeCloseStopsClaude:ClaudeCodeClosereturns, no Claude that ran when it began still runs.CloseNeverReusesOpenShowsLiveClaudeauto_close = falseis exempt, on purpose (it keeps an exited Claude).HideKeepsClaudeHideNoErrorFailedStartLeavesNoWindowExitClosesOnlyOwnWindowauto_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.AtMostOneClaudeBufEnter,TermOpen) started a second Claude.AtMostOneClaudeCloseStopsClaude:ClaudeCodeCloseafter a reload left Claude running.OpenShowsLiveClaudeOpenShowsLiveClaude:e filein Claude's window (native),:ClaudeCodeOpenfocused your file and Claude stayed hidden.HideNoErrorE444when Claude's window was the only window.ExitClosesOnlyOwnWindowOpenShowsLiveClaudeHideNoErrorBufEnterorTermOpenautocmd that calledfocus_togglewhile native started Claude made the open raiseInvalid window id, and Claude kept running with no window.Replays of each bug, against the code before its fix (
replays/, exit 1 means findings):8affa12)snacks-reentrant-open2 of 2,native-open-after-exit2 of 2,native-open-after-swap2 of 2,native-hide-only-window2 of 2,native-wipe-closes-your-window1 of 1, plus the reload replays below14798d1)native-reload-hidden1 of 1,snacks-reload2 of 2,auto-snacks-later1 of 2,native-reload-close1 of 13498879)snacks-reload-exit16 of 16,snacks-exit-handlers1 of 4native-start-autocmd-hideis new: 18 checks, 10 findings before #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 #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 #482 found each defect, and each fix landed before #482 did. SKILL.md lists them.Proof
All on this branch (head
a639966,mainat0d55c25merged), Neovim 0.12.3, Java from mise:check.sh:main: pass (263060 distinct states found),== RESULT: PASS, all 34 factsTRUE.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 (AtMostOneClaude10,CloseStopsClaude10,OpenShowsLiveClaude9,CloseNeverReuses5,HideNoError3,FailedStartLeavesNoWindow2,ExitClosesOnlyOwnWindow2,HideKeepsClaude1). I ran it on this head.owned.job_ended(terminal.buf)check fromforget_ended_terminalinsnacks.lua.check.shexits 1,SnacksEntriesForgetEndedJob FALSE,main: BROKEN: OpenShowsLiveClaude. Aftergit checkout lua,git diff --shortstatis empty and--hash-onlyreads "covered.lock matches the code".nvim_win_set_bufmakescheck.shexit 1 withNativeMarkBeforeTermopen FALSE, and removing thejobstopcall of the stop helper inowned.luamakes it exit 1 withOwnedStopOtherStops FALSE. Both files were restored after each break.check.shexits 1 (NativeKeepsHiddenJob FALSE,NativeStartSurvivesClosedSplit FALSE,main: BROKEN: HideKeepsClaude). With thereturndeleted fromhide_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 offorget_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.run.shexits 2 for a missing Neovim, a replay that raises and one that hangs invim.wait(a replay stuck in a CPU loop can outlivetimeout'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.lockis re-recorded on this head, which mergesmainat0d55c25(it had been recorded at37eaa0f). Changed since then in the covered files:terminal.lua(a warning message of fix(terminal): name the provider that setup keeps for an invalid provider value #530, file line only),native.lua(fix(terminal): keep the native start going when an autocmd closes its split #527, blockopen_terminal) andsnacks.lua(test(terminal): test the snacks guards that no test reached, and drop four dead window option assignments #526 dead stores, blocksnacks_openand the wrapper blocks, and the comment of docs(terminal): correct the comment on the bo reset in wrap_terminal #534). I read each diff: none changes a guard that a fact reads, and every fact reads TRUE except for the one that fix(terminal): keep the native start going when an autocmd closes its split #527 moved (NativeKeepsHiddenJob, updated).--hash-onlyreads "covered.lock matches the code" (about 10 s).Run it
CI runs every
.agents/skills/verify-*/check.shin thecovered-lockjob, as forverify-diff-lifecycle.Notes for the reviewer
check.sh,covered.lock,model/with the TLA+ spec and a/statechartview, andreplays/) and one sentence inlua/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.external,noneand custom table providers, a close that starts during another close's wait, more than one open or toggle per start from an autocmd, aWinNeworWinEnterautocmd that calls an entry while native'svsplitruns before the buffer has its mark (two Claudes run; open PR fix(terminal): keep a native start single when an autocmd interrupts it #544 proposes a fix), which window the plugin made (an exit withauto_closecloses a window of yours that shows the terminal buffer), a cleanup that raises (E444in a failed start's window close), aTermCloseautocmd of your own that closes the terminal, Snacks floats, tab pages, window sizes, a second reload,:bdelete,:qin Claude's window, and Neovim exit. It assumes Snacks'fixbuf, so:ein a snacks window is no step.DEVELOPMENT.mdis not edited here: the skill-listing change belongs to the PR that owns it.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh