Repository navigation
docs(terminal): correct the comment on the bo reset in wrap_terminal - #534
Merged
Merged
Conversation
The comment said that only an older version's stored window options carry `bo`. Since #526 a start of this version stores the `bo` of its instance too (the terminal style's filetype), so both can hold it. The reset of `instance.opts.bo` is unchanged.
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 Review: Didn't find any major issues. Already looking forward to the next diff. 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. |
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 13, 2026
…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`_
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.
Comment-only change in
lua/claudecode/terminal/snacks.lua. No behavior changes.The comment above
instance.opts.bo = {}inwrap_terminalsaid that "the window options that the terminal started with (an older version's, built from the config)" can holdbo. That was true before #526. #526 removed thewindow.bo = nilstore fromM.open, so a start of this version now stores theboof its instance too.I checked it with real snacks.nvim. After
:ClaudeCodewith the snacks provider,vim.b[buf].claudecode_snacks_windowholds about a dozen window options. The two versions differ only bybo:c9e57d1(before test(terminal): test the snacks guards that no test reached, and drop four dead window option assignments #526): nobokey3a0bb76(test(terminal): test the snacks guards that no test reached, and drop four dead window option assignments #526 merged):bo = { filetype = "claudecode" }The comment now names both sources: a start of this version stores the
boof its instance, and an older version's options are built from the config. The reset itself stays, for the same reason as before: Snacks setsboon the buffer again on everyVimResized, which would fireFileTypeagain.Validation
busted tests: 1509 successes, 0 failures, 0 errors (24 pending).FAILED: diff_failed_setup_guards_spec.lua: no plenary summary (nvim exit 0). That spec is from test(diff): pin that a failed openDiff setup in a new tab closes its tab #529 and this PR does not touch it. It passed 3 of 3 alone on this branch, 2 of 2 alone on a cleanorigin/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 becausesnacks.luais covered as a file. Only thefileline changed, and no model block did. I re-recorded the lock, and the check passes.Notes for the reviewer
verify-terminal-lifecycle(feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle #525) hashessnacks.luatoo. feat(skills): add verify-terminal-lifecycle, a TLA+ model of the Claude terminal lifecycle #525 mergesmainand re-records itscovered.lockafter this PR merges.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh