Repository navigation
Use a native graph list with scoped local copy deletion - #79
Conversation
…cal-copy-20261015
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: 0e3075c614
ℹ️ 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".
| Unix.rename graph_directory retired; | ||
| ignore (Ownership.release ownership); | ||
| remove_mirror_tree retired; |
There was a problem hiding this comment.
If remove_mirror_tree retired raises after the rename—for example because of an I/O or permission error—the function reports deletion failure but leaves the mirror under the .deleted-* name. The original UUID path is then absent, so a retry treats the copy as already deleted and never removes that tombstone; the graph is unavailable despite the reported failure and its storage is leaked. Restore the directory on cleanup failure or persist and retry tombstone cleanup.
Useful? React with 👍 / 👎.
| if waiter.request <> None && snapshot.local_deletion = None | ||
| then finish (match snapshot.last_error with None -> Ok () | Some message -> Error message))); |
There was a problem hiding this comment.
When a concurrent catalog refresh removes the currently selected graph while another graph's deletion is in flight, clear_selected_graph_for_catalog clears local_deletion and last_error without changing the account generation. This condition therefore resolves the deletion promise as Ok () before the matching Mirror_deleted terminal arrives; the worker then rejects the now-unauthorized cleanup, while the application marks the target as not downloaded. Resolve the waiter only from the terminal event for its captured deletion request.
Useful? React with 👍 / 👎.
| let owned = match state.manager with | ||
| | Some manager -> manager.startup.account_generation = request.Graph_service.account_generation | ||
| && (if deleting then state.local_copy_deleting = Some request else (not confirm || state.local_copy_check = Some request)) |
There was a problem hiding this comment.
If a visibility-triggered inspection is still in flight when the user performs the explicit check and confirms deletion, the requests can overlap because the automatic request is not represented by local_copy_check. A late automatic response is always considered owned through not confirm, so a pre-deletion Downloaded result can arrive after successful deletion and overwrite the Not_downloaded state, leaving the row incorrect and re-enabling deletion. Ignore inspection results once that graph has entered or completed a newer deletion, or fence them with a per-graph generation.
Useful? React with 👍 / 👎.
| let* () = asset_unit t | ||
| ~scope:{ Sync.account = request.account; graph_id = request.graph_id; graph_generation = 0 } | ||
| Sync.Delete_graph_assets |> Result.map_error (fun _ -> | ||
| "The local copy is still in use. Close attachment previews and try again.") in |
There was a problem hiding this comment.
When mirror removal fails after this call—for example because another process acquires the mirror ownership lock, authorization changes at the following current check, or the filesystem rejects the rename—the function returns an error while Delete_graph_assets has already permanently removed cached attachments and staged upload sources. The retained mirror is therefore no longer a retryable intact copy, and pending uploads can lose their source files despite the UI reporting that deletion failed. Defer destructive asset cleanup until the mirror has been safely retired, or restore it as part of a transactional rollback.
Useful? React with 👍 / 👎.
1 participant
Switch graph now keeps the active graph attached and presents a native List across the whole screen, with Timeline-style floating close, refresh and existing account controls. The current graph remains in its catalog position; names switch graphs and each row's menu offers Delete local copy. Long names wrap and the native list supports accessibility Dynamic Type.
Deletion names the graph and explains that unsynced changes, drafts and attachments on this device will be lost while the cloud copy remains downloadable. The user explicitly authorized discarding unsynced content. The current graph must be switched away from first; persisted account ownership, catalog authorization and generation checks fence every request.
The worker acquires mirror ownership before preparing attachment retirement, drains target operations/leases, captures exact upload checkpoints and persists a recovery journal. Mirror commit has durable, retirement-specific evidence; pending collection retries without touching replacement files. Before commit, cancellation restores only the captured namespace through an atomic no-replace rename. Late completions and duplicate/replayed requests retain exact account/graph/retirement identity. Journal I/O failures return a retryable deletion error while preserving the current Worker; catalog refresh loading/failure is visible, including after an earlier local-copy error.
The old Delete_graph_assets, Database.delete_mirror and graph-wide upload-checkpoint delete APIs and callers are removed without compatibility wrappers. Delete_account_assets remains. The two protected deletion specs were explicitly approved; Dune, lockfiles and shared opam/pins are unchanged.
Validation:
All generated hosts, screenshots, reports and build artifacts remain outside Git. No personal graph, phone, real credentials or remote graph deletion was used.