🤖 fix: give each Xum installation its own SSH plan namespace (#5174) - #5611
Merged
Merged
Conversation
|
Preview deployment for your docs. Learn more about Mintlify Previews.
💡 Tip: Enable Automations to automatically generate PRs for you. |
Codex Review SummaryThis 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. |
![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: 6dc67b0ac4
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8e292d160a
ℹ️ 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".
Member
Author
|
@codex review Round 2 is resolved: the downgrade-rename case is now documented as a known limitation (reply on the thread). Please review the current head. |
🛡️ Codex Security Review · Automatically triggeredSecurity 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: 807023c1d4
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3f1f186d01
ℹ️ 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".
4 tasks
Member
Author
|
Review loop stopped. This PR is not ready to merge. Head: Blocker: #5611 (comment) The fix needs a decision:
Required CI fails only because the unresolved thread fails |
… SSH plans (#5174) Design pass for a reduced replacement of #5469. PlanMigration.tla models a single migration point (location resolution): under the row's lock, re-check the flag, copy the id plan (else the shared basename plan) into the scoped namespace unless a scoped plan exists (temp, fsync, link, fsync dir), then persist the row flag whatever the source was. Reads after that see the scoped namespace only. check.sh runs the new MC_mig_* configs against PlanMigration.tla. The #5469 r9 finding (MC_mig_reported) violates NoReactivation, NoForeignAfterId and NoLegacyTouch; the reduced design holds under concurrent reads, clear, foreign writes, identity reset, a restart between any two writes, a power cut, and downgrade/upgrade. Eight mutants stay caught. Full check.sh: 174 runs, all as expected. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
SSH and Coder plans live under ~/.mux/plans/installation-<uuid>/<project id>/<name>.md; the UUID is created once in the data root (fail closed when unusable). Older rows migrate once in resolvePlanFileLocation: their own plans/<id>.md plan is copied (temp, fsync, link, fsync dir), then the monotone row flag remotePlanMigrated is set; afterwards only the scoped path is read. Option B: the shared pre-#5174 plan is never imported automatically; the user imports it with workspace.importLegacyPlan (notice above the chat input, or the command palette), which never replaces an existing plan and never moves or deletes the legacy file. Supersedes #5469. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_
…t tab after an import; run the model on config changes
…hared plan alone; list only migrated SSH ancestors
…; model the shared-ID boundary A copy of a data root that stays usable must get a fresh installation ID before it accesses remote plans: the migration flag and lock are local to a root, so two roots with one ID can restore each other's cleared plans. Xum does not detect copies. - docs: the contract, and verified steps that give a copy its own ID and copy the old plan tree on the host without replacing files (cp -Rn src/. dst/ copies nothing on BusyBox, so the step copies only into a tree that does not exist yet). - formal: state the unique-identity assumption; actor k (a copy of a pre-upgrade root) with CopyIdentity fresh in MC_mig_full; MC_mig_boundary_shared_uuid documents the shared-ID counterexample (NoResurrection fails).
ThomasK33
force-pushed
the
fix/plan-installation-scoped-migration
branch
from
October 4, 2026 11:05
3f1f186 to
8dc11f9
Compare
Member
Author
Dogfood: two data roots with their own IDs (contract reduction for the copied-root finding)Setup: Alpine sshd in Docker (BusyBox
Steps:
The old file I verified the recovery procedure and found a bug in my first draft. The first draft used
Terminal evidence (host file listings and API reads) |
Member
Author
|
Codex Review: Didn't find any major issues. Delightful! 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 Review · Automatically triggeredSecurity 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. |
macOS uuidgen prints uppercase, and Xum uses the lowercase form in remote plan paths, so step 4 copied the tree to a name Xum never reads. Step 3 now writes the ID in lowercase, and step 4 lowercases both pasted IDs.
Member
Author
Docs fix on 2a31d4f: lowercase the new ID in the copied-root stepsAn independent pre-merge review found a defect in the round-5 docs. On macOS, The fix:
I verified the fix on the Docker sshd host:
The first attempt failed for an unrelated reason. Restarting the container wiped the host, so the workspace checkout directory was missing and the read failed. I recreated the host state and ran it again. The log below shows both attempts.
Terminal evidence |
Member
Author
|
Codex Review: Didn't find any major issues. Breezy! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
🛡️ Codex Security Review · Automatically triggeredSecurity 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. |
This was referenced Oct 4, 2026
yermakoffivan
pushed a commit
to yermakoffivan/mux
that referenced
this pull request
Oct 4, 2026
coder#5621) ## Summary Three fixes from the coder#5611 review (round 4), tracked in coder#5620: 1. **A legacy plan path that cannot be checked no longer counts as missing.** The one-time SSH plan migration now treats a legacy plan as absent only when Xum can confirm it. If a folder on the way cannot be searched, the migration fails and leaves the row unmigrated, and the next access retries. Before, Xum marked the row migrated and never offered that plan again. 2. **The import notice settles after `nothing_to_import`.** When the shared file vanished after the offer, the notice kept its **Import plan** button and palette action, which could only fail again. Now the notice keeps the reason and drops both. 3. **The installation-identity temp file is removed when its write fails.** An outer `finally` removes `tempPath` (for example after ENOSPC). Refs coder#5620. Item 4 (a rename made while downgraded) needs a new remote layout keyed by workspace ID. It stays open in backlog. ## Implementation - `migrateRemotePlanScript` (`planLocation.ts`): the new shell function `known` accepts a path that exists, or a path whose nearest existing ancestor is a searchable directory. Only then did the lookup really find nothing. Anything else exits with the new code `unverified` (7). `migrateRemotePlan` turns that code into a `RemotePlanMigrationError`, so plan reads, the import offer and clears fail closed, as they already did for a failed copy. The check runs only where the answer matters: on the id plan when Xum would fall back to the shared path, and on the shared path when Xum would record "no legacy plan". - `LegacyPlanImportNotice`: a `vanished` state hides the status text and the button, and it unregisters the palette source. The alert stays visible. The notice goes away on the next mount, when the backend no longer offers the path. - `loadOrCreateInstallationId`: the temp file's open, write, sync and link run inside one `try`, and its `finally` removes the temp file. I checked `known` with dash and bash: an unsearchable folder exits 7, a missing file or a missing ancestor is accepted, and an existing path is accepted. ## Validation Pre-fix failures (the new tests on main at 235980f): ``` Expected: "refused" Received: "offered null" (fail) SSH plans are installation-scoped (coder#5174) > a legacy path that cannot be checked fails closed, and its plan is offered once it can be - [] + [ + ".installation_id.62d4a7a0-cc3d-48bc-94a4-c341d548c107.tmp", + ] (fail) installation identity creation failures (coder#5620) > a failed write of the new identity leaves no temp file in the data root Received: HTMLButtonElement { (fail) LegacyPlanImportNotice (coder#5174) > an import that finds nothing settles the offer: the reason stays, the actions go 0 pass 3 fail ``` After the fix, all three pass, together with the rest of `workspaceService.remotePlanNamespace.test.ts`, `installationIdentity.test.ts`, `LegacyPlanImportBanner.test.tsx` and `src/node/utils/runtime/`. `formal/plan-storage/check.sh` passes, and this PR does not change `formal/`. The new Storybook story `NothingToImport` has a play that clicks **Import plan** and checks the alert and the missing button. Storybook, before the click (the offer) and after an import that found nothing:     ## Risks Low. Item 1 can turn a host with odd permissions on `~/.mux/plans` from "no plan" into a plan read error until the permissions are fixed. That is the fail-closed direction the issue asks for, and the error says what Xum could not check. --- _Generated with `xum` • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ <!-- mux-attribution: model=anthropic:claude-opus-5-5 thinking=high -->
yermakoffivan
pushed a commit
to yermakoffivan/mux
that referenced
this pull request
Oct 4, 2026
…oder#5479) (coder#5622) ## Summary A full clear and a rename of the same workspace no longer leave a cleared workspace with its plan. In one backend they now exclude each other. A clear refuses while that workspace is being renamed. A rename refuses while a clear deletes that workspace's plan. Both refusals commit nothing and keep the plan, and the user can retry. Refs coder#5479 (item 2). Items 1 (ssh_config `HostName` aliases) and 3 (a one-time test failure) stay parked. ## Background `deletePlanFilesForWorkspace` reads the workspace's name with `getInfo` and deletes the plan path derived from that name several awaits later. coder#5611 added three awaits there: the installation identity, the SSH migration flag and the plan location. A rename in that window moves the plan to the new name. The clear then deletes the old, missing path and commits, and the plan stays with the cleared workspace. A clear that starts after the rename's config write but before its plan move has the same result: it deletes the new, still missing path, and the move then brings the plan back. ## Implementation - `deletePlanFilesForWorkspace` refuses while `renamingWorkspaces` holds the workspace. Otherwise it counts itself in `planDeletionsInFlight` (a count, because two clears can overlap) for the whole deletion. The body moved unchanged to `deletePlanFilesForWorkspaceWhileNotRenaming`. - `rename()` refuses while `planDeletionsInFlight` holds the workspace. It checks this right before it sets its renaming flag, in the same synchronous step. - Only the rename that set the renaming flag clears it (review round 1). Before, an overlapping second rename that exited early deleted the first rename's flag. That ended the exclusion of streams and clears while the first rename still ran. A rename that finds the flag already set now refuses at once. - I updated the stale comment that called `getInfo` the last await before the delete. - Not covered: a rename in another backend on the same data root. Both sets are in-process. ## Validation Three repros in `workspaceService.planStorageFormalRepro.test.ts`, with real local workspaces and real plan files: 1. A rename runs inside the clear's `getInfo`, after it read the old name. 2. A clear runs inside the rename's `movePlanFile`, after the rename registered the new name. 3. Review round 1: inside the first rename's `movePlanFile`, a second rename is refused, and then a clear runs. Before that fix the clear committed (`Received: "cleared"`). Pre-fix (main at 235980f): ``` - "new": undefined, + "new": + "# The plan (fail) ... > a rename that lands while the clear deletes the plan does not carry the plan past it Expected to contain: "renamed" Received: "cleared" (fail) ... > a clear while a rename moves the plan does not commit without deleting it 0 pass 2 fail ``` After the fix, both pass, with the rename, truncateHistory, history, removePlanFiles, planNamespace, remotePlanNamespace and workspaceService suites (230 tests). `formal/plan-storage/check.sh` passes. The model does not cover a rename racing a clear of the same workspace, so `formal/` is unchanged. ## Risks Low. The only new behavior is a refusal when a clear and a rename of one workspace overlap in one backend. Both are user actions that take seconds at most. --- _Generated with `xum` • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ <!-- mux-attribution: model=anthropic:claude-opus-5-5 thinking=high -->
yermakoffivan
pushed a commit
to yermakoffivan/mux
that referenced
this pull request
Oct 4, 2026
…oder#5462) (coder#5623) ## Summary `PlanStorage.tla` now models the removal guard and the clear guard as separate steps from their deletes, and it adds a create that races each of them. The model now shows the window that coder#5462 item 2 describes, and it confirms that the create re-check from coder#5468 closes it. This PR changes only `formal/plan-storage`. Fixes coder#5462. Item 1 was done by coder#5468. Item 3 is done on main by coder#5611, as shown in the triage comment on the issue. ## Background The code reads the workspace registry (the sharing guard) and deletes the plan in separate awaits, both in removal (`deletePlanFilesOfRemovedWorkspace`) and in a full clear (`deletePlanFilesForWorkspace`). The model treated guard and delete as one atomic step, so it could not show a row that joins between them. It also deregistered before the delete, which is the order before coder#5019. The code deletes before it deregisters, so the name stays taken during the delete. ## Model changes - **Removal:** three sub-steps in the code's order: `guard` (records whether a visible row shares the path), `del` (keeps the path when the guard saw one), `dereg`. A new mutant, `removeDeregFirst`, uses the order before coder#5019. - **Clear:** with `ClearGuard`, two sub-steps, `guard` and `do`. Without the guard it stays one step, as the code was before coder#5467. - **New variable `keep`:** the guard's result, which the delete uses later. - **New scenarios:** `remove_race` (b creates the name and removes it while a creates the same name and writes a plan) and `clear_race` (the same with a guarded clear). - The header cites the current code (`workspaceService.ts` at 235980f). | Config | Fixes / mutant | Expected violations | |---|---|---| | `MC_remove_race` | none | UniqueOwner, NoForeignClobber | | `MC_remove_race_fixed` | createRecheck (the code since coder#5468) | none | | `MC_mut_remove_deregfirst` | createRecheck + removeDeregFirst | NoForeignClobber | | `MC_clear_race` | clearGuard | UniqueOwner, NoForeignClobber | | `MC_clear_race_fixed` | clearGuard + createRecheck (the code since coder#5467/coder#5468) | none | The shortest counterexample for `MC_remove_race` NoForeignClobber is the window from the issue: b and a pass their name preflights, b registers, b's guard sees no other row, a registers (no re-check), a writes its plan, and b's delete removes it. ## Validation - `formal/plan-storage/check.sh` (all configs, PlanMigration included) exits 0 on this head. Every existing config keeps its EXPECT verdict, including the pre-fix finding configs. - **The split is what exposes the window.** In a scratch copy, I gave each delete the guard result from the same step, which is the old atomic model. Then `NoForeignClobber` holds in both `MC_remove_race` and `MC_clear_race`, and only the create race's `UniqueOwner` remains. --- _Generated with `xum` • Model: `anthropic:claude-opus-5-5` • Thinking: `high`_ <!-- mux-attribution: model=anthropic:claude-opus-5-5 thinking=high -->
This branch was successfully deployed
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
1 participant
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.
Summary
Each Xum installation now keeps its SSH and Coder plans in its own folder on the remote host. A clear or delete in one installation can no longer remove another installation's plan. This PR replaces #5469 and closes #5174.
Workspaces created before this change move their plan once, on first access:
Background
Before this change, every installation that used one SSH host wrote plans to the same path,
~/.mux/plans/<project>/<name>.md. Two installations with the same project and workspace name used one file. A clear in one deleted the other's live plan (#5174).#5469 fixed the path. It kept the old shared file as a fallback that every plan reader could adopt. That fallback needed special handling in each plan consumer, and nine Codex review rounds kept finding new cases. The last finding: after a reset of the installation ID, a read adopted another installation's stale shared plan. This PR removes the fallback. Migration happens once, in one function.
Persisted-state contract
installation_idfile in the data root (~/.xumby default)~/.mux/plans/installation-<uuid>/<project-id>/<name>.mdremotePlanMigratedconfig.jsonplans/<id>.md(this workspace's own) andplans/<project>/<name>.md(shared)How the migration works
resolvePlanFileLocation(planLocation.ts) is the single resolver that every plan consumer uses (reads, attachments, snapshots, rename, fork, clear, removal, turns). For a row without the flag, it migrates once, under a lock for that row, and checks the flag again inside the lock:plans/<id>.mdexists, Xum copies it in this order: temp file, fsync, hard link, fsync the folders. Then Xum sets the flag.Explicit import (Option B):
workspace.getImportableLegacyPlanreturns the shared file's path, but only for an older row whose only old plan is that file.workspace.importLegacyPlanruns the same migration, with the shared file allowed as the source. It never replaces an existing plan, so a second import returnsalready_present. It never deletes the shared file. After a full clear there is nothing to import.UI: a self-gating notice above the chat input (after an import, the Context tab fetches again, so it shows the plan),
LegacyPlanImportBanner. It shows the file's path, warns that other installations can own that file, and has an Import plan button. The command palette has the same action, Import plan from an older Xum, for keyboard use. I chose the notice over a Context tab row because the right sidebar is hidden at phone widths (768 px and below).Validation
formal/plan-storage/PlanMigration.tla, checked bycheck.sh.MC_mig_reportedreproduces 🤖 fix: give each Xum installation its own SSH plan namespace #5469's last finding. Its fixed twin passes.MC_mig_boundary_shared_uuiddocuments the boundary: a copy that keeps the ID restores a cleared plan (NoResurrectionfails there, as expected).check.shexits 0.workspaceService.planStorageFormalRepro.test.tsis an ordinary passing test now. It was an expected-failure test before.workspaceService.remotePlanNamespace.test.tshas 23 tests on a real shell (a local runtime stands in for the SSH host). They cover the reported sequence, the ID-file-first rule, recovery after a failed copy or flag write, a clear racing a migration, removal, downgrade edits, every consumer, and import, repeat import, overwrite refusal and import after a clear.LegacyPlanImportBanner.test.tsx: one import at a time (a button click and the palette action), errors, and the palette action is removed when the notice goes.config.jsonto simulate an older row, and put a plan at the shared path on the host. The notice appeared. Importing through the command palette copied the plan intoinstallation-<uuid>/…. The shared file stayed in place, the Context tab showed "Plan file", and a second import returnedalready_present.Risks
installation_idfile starts an empty folder. Plans under the old ID stay on the host but unused. The plan-mode docs explain how to recover them.Follow-ups
Supersedes #5469.
Generated with
xum• Model:anthropic:claude-opus-5-5• Thinking:high• Cost:$77.03