Repository navigation
fix(terminal): keep the native start going when an autocmd closes its split - #527
Conversation
… split A BufEnter or TermOpen autocmd that calls focus_toggle while the native provider starts Claude made open() raise "Invalid window id" at nvim_win_get_buf: the toggle adopted the half-started terminal, found its window focused, and hid it, and the start then read the window that was gone. Claude kept running with no window, and the error reached the user. A second simple_toggle from such an autocmd, or a plain :close, did the same. open_terminal no longer assumes that its split survives the start. When the split is gone, Claude is tracked as a hidden terminal, and the next toggle shows it. The check on the buffer that an autocmd swapped in, and the focus step, take the window only while it exists. The snacks provider has no such gap: it tracks its terminal only after Snacks.terminal.open returns, and a nested open, toggle or close during the start does nothing.
|
@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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 23112eb95d
ℹ️ 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".
🛡️ 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. |
When one autocmd of a native start hid the terminal and a later one showed it again, show_hidden_terminal tracked the replacement window, and the start then replaced it with nil because the split it created was gone. Claude was visible but tracked as hidden: a focused open returned to the original window, and the exit of the job did not close the replacement window with auto_close. open_terminal now tracks the split while it exists and then looks for the window that shows the terminal, as is_valid does for every other entry point.
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Chef's kiss. 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. |
…can close An autocmd that closes the new split during a native start unloaded the buffer when 'nohidden' was set, because the buffer got bufhidden=hide only after termopen. On Neovim 0.8, a BufEnter autocmd made Neovim load the buffer again before termopen, and its term:// reader started a second terminal in it, which the plugin tracked: a bare claude with no arguments and no plugin env. A TermOpen autocmd ended Claude with a "Failed to open native terminal" error. open_terminal now sets bufhidden=hide before it shows the buffer. The README says what a start does when an autocmd closes the split and when another one shows Claude again, and the hide-and-show tests reject a window that is gone, so that dropping the rescan fails them.
|
@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. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d0ea2888fd
ℹ️ 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".
…e start The early bufhidden=hide of the previous commit replaced the assignment after termopen. An autocmd of the start that sets another value (a terminal cleanup autocmd that sets wipe) then won, and a later toggle wiped the buffer and ended Claude. The start sets hide before it shows the buffer, for 'nohidden', and again after the autocmds, as it did before.
|
@codex review |
|
@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. |
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. You're on a roll. 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. |
covered.lock conflicted with #527. Took main's covered.lock and re-recorded it with check.sh --record after check.sh passed on the merged tree. Also names exit 139 (SIGSEGV) next to exit 134 in the comment of the workaround and in the spec comment. No code line changed.
…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.
…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`_
…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`_
A
BufEnterorTermOpenautocmd that callsfocus_togglewhile the native provider starts Claude makes:ClaudeCoderaiseInvalid window id: <n>atnative.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 #525 (the
verify-terminal-lifecycleskill), which asked the model to cover an autocmd that calls a toggle during a native start.What happens
open_terminalcreates the split and the buffer, and marks the buffer. The mark goes beforetermopenon purpose, so that anopen()from a start-time autocmd adopts this terminal and starts no second one.nvim_win_set_buffiresBufEnter, andtermopenfiresTermOpen. Neither has setbufnrorwinidyet.focus_toggle. It finds no tracked terminal, adopts the marked, half-started buffer, sees that its window is the current one, and callshide_terminal. The split closes.open_terminalgoes on and callsnvim_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_togglefrom the autocmd, or a plain:close.The fix
open_terminalno longer assumes that its split survives the start (lua/claudecode/terminal/native.lua):winid = new_winidandbufnr = new_bufnr, then callsis_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.bufhidden=hideon the new buffer before it shows it. It also keeps the assignment aftertermopen, which overrides an autocmd of the start that changedbufhidden(towipe, for example), so a later hide still keeps the job. With'nohidden', a window that closes during the start unloads a buffer that is notbufhidden=hide. InBufEnter, Neovim then loads the buffer again beforetermopen, and on 0.8 itsterm://reader starts a second terminal in it: a bareclaude, with no arguments, no plugin env and no IDE connection, which the plugin then tracks and sends text to. InTermOpen, 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.mddescribes the new branches.I kept
focus_toggleas 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 thebufhiddenline), and:ClaudeCodeFocusor:ClaudeCodeshows it again.Snacks has no such gap
The snacks provider tracks its terminal only after
Snacks.terminal.openreturns, and astartingflag makes a nestedopenreturn. I ran the same shape against real snacks.nvim: aBufEnterorTermOpenautocmd that callsfocus_toggle,simple_toggletwice,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 changesnacks.lua.Tests
11 new tests in
tests/unit/native_terminal_toggle_spec.lua:6 tests, each for a
BufEnterand aTermOpenautocmd that callsfocus_toggle, callssimple_toggletwice, or closes the window. Each callsopenunderpcalland asserts that it raises nothing, that one job runs and is tracked, that no window shows it, that a latersimple_toggleshows it, and that no second Claude starts.2 tests, for a
BufEnterand aTermOpenautocmd that callssimple_togglethree times (adopt, hide, show again in another window). They callopendirectly, 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 withauto_close.2 tests with
'nohidden'(aBufEnterautocmd that closes the split, aTermOpenautocmd that callsfocus_toggle): one job runs, no "Failed to open" notice, Claude is tracked and hidden. The mock unloads a buffer that is notbufhidden=hidewhen its last window closes with'nohidden', and loads it again with a second job, as the 0.8 reader does.1 test: a
TermOpenautocmd setsbufhidden=wipeon the new buffer, and the start must leavebufhidden=hideon it.The tests make
nvim_set_current_winraise for a window that is gone, as Neovim does.c9e57d1(main), the first 10 fail (9 of them withInvalid window id: 1000). Thewipetest passes on main, which setshideaftertermopen, and it guards that this PR keeps that line.nvim_win_is_validcheck beforenvim_win_get_buf, theis_valid()rescan, thefocus and winidcheck, the earlybufhiddenand 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 namedclaudethat logs each start. Onc9e57d1the replay has 10BUGlines 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 #525 once this merges.Validation
busted tests: 1520 successes, 0 failures, 0 errors (24 pending), on the head merged withmainat036427a.stylua --check lua tests,luacheck lua/ tests/,treefmt --ci: clean.verify-diff-lifecycle/check.sh: the lock read STALE becausenative.luais covered as a file. Only thefileline changed, and no model block did. The change cannot reach diff state (it only affects howopen_terminaltracks its own window after a start). I re-recorded the lock, and the check passes.Notes for the reviewer
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, aclose()from aTermOpenautocmd crashes Neovim (corrupted double-linked list, segfault, exit 139), onmainand with this fix alike.WinEnterorWinNewthat fires during thevsplitof the start, before the buffer is marked, can call a toggle oropenthat starts a second Claude, and a:closethere makes Claude take your only window. A follow-up PR handles that start-up window (fix/native-start-reentry).verify-terminal-lifecycle(feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle #525) coversnative.lua. After this PR merges, feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle #525 mergesmain, re-records itscovered.lock, and adds the model step and the replay.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh