🔬 Prove persistent tmux pane workers for <Terminal.Grid> (#726) - #727
🔬 Prove persistent tmux pane workers for <Terminal.Grid> (#726)#727taras wants to merge 4 commits into
Conversation
An executable proof of the pane-worker topology #717 needs: one persistent worker per tmux pane owning the pane's terminal, driven over an invocation-private Unix socket, starting interactive children that inherit the terminal through an Effection process resource derived from the native launcher. The proof runs the reader-visible journey, the readiness boundary, explicit row-major layout, atomic attach, the three close signals, negative children, cancellation at every phase, and 2/4/8-pane timings, and records what teardown can and cannot prove. deno task proof:tmux-pane-workers
Evidence from b0fcee9: 8/8 checks, 115 claims, 2/4/8-pane timings over 20 runs each. Recommends adopting the persistent pane-worker topology for #717 with the teardown claim narrowed to process group, ancestry at teardown start and terminal holders — a descendant that left the session, closed the pane's terminal and outlived its parent is outside what a parent can prove.
| rows === Math.ceil(shape.panes / shape.columns), | ||
| rows, | ||
| ); | ||
| // What `select-layout tiled` would have done with the same panes. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // What `select-layout tiled` would have done with the same panes. |
| workspace.links.every((link) => link.connected()), | ||
| ); | ||
| // 3. The server stops underneath everything. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // 3. The server stops underneath everything. |
| await main(function* () { | ||
| const options = parseOptions(process.argv.slice(2)); | ||
| // tmux and ps output is collected, never echoed. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // tmux and ps output is collected, never echoed. |
| // tmux and ps output is collected, never echoed. | ||
| yield* Stdio.around({ | ||
| *stdout() { | ||
| // Collected by the caller, never echoed. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // Collected by the caller, never echoed. |
| // Collected by the caller, never echoed. | ||
| }, | ||
| *stderr() { | ||
| // Collected by the caller, never echoed. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // Collected by the caller, never echoed. |
| // A child that exited on its own may have left descendants in the | ||
| // pane's process group. They are swept before `exited` is reported, | ||
| // because `exited` is what makes the pane free for the next child — | ||
| // and a sweep running beside a new child would reach that child too. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // and a sweep running beside a new child would reach that child too. |
| limitMs: number = DEFAULT_LIMIT_MS, | ||
| ): Operation<T> { | ||
| // Subscribe before scanning, so an event between the scan and the wait | ||
| // is not lost. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // is not lost. |
PR #727: 🔬 Prove persistent tmux pane workers for <Terminal.Grid> (#726)14 files, +6544 / -0 Scope🔴 PR has 6544 lines changed. Split into focused PRs. 🟡 6544 lines changed. PRs under 400 receive more thorough review. 🟡 PR mixes config and source changes. 🟡 New abstraction files: scripts/proofs/tmux-pane-workers/provider.ts. Verify 3+ consumers. StructuralOxlint structural signals:
Slop
Static AnalysisOxlint: 10 diagnostics across 6 files (4 rules) no-floating-promises (5): scripts/proofs/tmux-pane-workers/provider.ts, scripts/proofs/tmux-pane-workers/ipc.ts, scripts/proofs/tmux-pane-workers/worker.ts (+1) CorrectnessNo extraneous code patterns detected. |
A worker's settlement is now the escalation followed by the terminal-holder sweep, on natural exit as well as cancel and shutdown, and `exited` is reported only after it. A new sequential-handoff regression starts a child whose descendant setsid()s, keeps the pane terminal and outlives its parent, and proves a launch sent during settlement is refused, the descendant is named and stopped before `exited`, and only the worker and the second child hold the terminal after admission. Measurements gain the handoff and relaunch latencies the sweep introduces. The setsid() + closed-terminal orphan remains the recorded unprovable boundary.
Evidence from 650510b: 9/9 checks, 127 claims. Adds the handoff and relaunch columns to the measurements and the sequential-handoff regression to the teardown account; the setsid() + closed-terminal orphan stays the recorded unprovable boundary.
| // tmux and ps output is collected, never echoed. | ||
| yield* Stdio.around({ | ||
| *stdout() { | ||
| // Collected by the caller, never echoed. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // Collected by the caller, never echoed. |
| // Collected by the caller, never echoed. | ||
| }, | ||
| *stderr() { | ||
| // Collected by the caller, never echoed. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // Collected by the caller, never echoed. |
| try { | ||
| child.unref(); | ||
| } catch { | ||
| // Already released. |
There was a problem hiding this comment.
Redundant comment — restates what the code does.
| // Already released. |
Why
#717 (
<Terminal.Grid>) needs a process topology that gives reliable readiness, pane output, sequential native launches and complete teardown. #726 asks for an executable proof of the persistent pane-worker topology and a report so the Planner can adopt it or the Architect can narrow the lifecycle contract. This PR is that proof and report; it decides #717's next step and ships nothing in the product binary.What changes
Before: the topology was a hypothesis. tmux's
pane_pidcannot say whether a native process started, and a native command as the pane command leaves no endpoint for document text or a second launch.After:
deno task proof:tmux-pane-workersruns one 2×2 workspace (and the smaller topologies each check needs) end to end and writesevidence.json+summary.md.plans/tmux-pane-workers-proof.mdrecords the run at b0fcee9 — 8/8 checks, 115 claims — the measured lifecycle for 2/4/8 panes, what teardown can and cannot prove, the smallest interfaces the evidence supports, and the recommended decision: adopt the pane-worker topology, with the teardown claim narrowed to process group, ancestry at teardown start, and terminal holders.How it works
Review guide
Start with:
plans/tmux-pane-workers-proof.md— the decision, the acceptance table, and What teardown can and cannot prove.Then review:
scripts/proofs/tmux-pane-workers/interactive-process.ts— the product-boundary resource derived frompackages/runtime/launcher.ts: readiness vs settlement, escalation, the pre-signal snapshot.worker.tsandipc.ts— what a pane worker is, what crosses the socket, admission by token,exitedafter the sweep, the shutdown terminal sweep;run()notmain().provider.tsandlayout.ts— hidden server, explicit layout +swap-paneordering, control-mode classification, detach-before-signal on the visible client,stop()proof.checks.ts— one check per acceptance item;evidence.ts,workspace.ts,proof.tsare harness.Look carefully at:
plans/tmux-pane-workers-evidence.jsonis the raw run with IPC tokens redacted; its pane ids, ttys, pids and socket paths describe one run and nothing durable.What must stay true
spawnevent and nothing earlier;startup-failednever followsready— enforced byuseInteractiveProcess, checked byreadiness-boundary.exitedafterstop(); checked by the journey's sequential-reuse claim.cancellation-pointsat five phases.How to verify it
deno task proof:tmux-pane-workers(≈5 min, unattended; needs tmux 3.6a-class and Deno) proves every claim in the report and fails if any pid, server, socket directory or terminal setting survives teardown.deno task proof:tmux-pane-workers -- --only negative-childrenproves descendant coverage and fails if the pre-signal snapshot or the worker's terminal sweep is removed (both were removed on purpose during development and did fail).-- --only layout-geometryfails ifswap-paneordering is skipped (tmux ignores leaf ids in layout strings).-- --only readiness-boundaryfails ifreadyis sent before the spawn event.-- --only cancellation-pointsfails ifstop()skipskill-server.-- --attachshows the journey on your own terminal and waits for you to detach.deno task lintanddeno task checkare green; the proof lives underscripts/proofs/, outside test discovery, so no CI suite runs it.Scope
Included
Intentionally unchanged
architecture.md, the specs andpackages/runtime/launcher.ts: the decision is recommended here for the Architect to record; nothing in the product moves.Risks and limitations
ps -o tpgid,lsof -tand the pty-revoke behaviour are the macOS facts the report names.new-sessionforking the server and the server listening is a window the proof records rather than tests.Scope confirmation