Fix pull mirroring and reject additive Git overlays

.github/workflows/ci.yml

@@ -33,8 +33,8 @@ jobs:
       # coop-proxy's aws-lc-sys crypto backend (issue #411) needs cmake; the
       # `--workspace` clippy/test below build it. Preinstalled on ubuntu-latest,
       # installed explicitly so the job doesn't depend on the image contents.
-      - name: Install cmake
-        run: sudo apt-get update && sudo apt-get install -y cmake
+      - name: Install build and workspace test tools
+        run: sudo apt-get update && sudo apt-get install -y cmake git rsync
 
       - name: Format check
         run: cargo fmt -- --check

docs/commands.md

@@ -623,14 +623,21 @@ coop pull [NAME] [FLAGS]
 |------|-------------|
 | `NAME` | Instance name (required if multiple instances exist) |
 | `--dir <dir>` | Local directory to pull into (defaults to the workspace host path) |
-| `--force` | Overwrite local changes without confirmation |
-| `--exclude-git` | Skip the `.git/` directory in this transfer |
+| `--force` | Skip the local dirty check (does not enable deletion or bypass the Git overlay guard) |
+| `--delete` | Mirror the guest, removing non-excluded host-only paths; requires rsync on both ends |
+| `--exclude-git` | Preserve all host `.git` entries, including gitfiles and symlinks |
 
 ```
-coop pull
+coop pull --delete
 coop pull my-project --dir ./local-copy --force
 ```
 
+Additive pulls into an existing Git repository require `--exclude-git`; use
+`--delete` to include Git metadata safely with respect to stale refs. Mirror
+mode can remove host-only branches even when the working tree is clean.
+See [workspace sync](workspaces.md#pulling-guest-to-host) for exclusions,
+transport requirements, and worktree limitations.
+
 ### `editor`
 
 Open an editor (VS Code or Zed) connected to the guest VM over SSH remote.

docs/editor.md

@@ -138,3 +138,9 @@ VS Code's Remote SSH extension exposes a Ports panel that handles forwarding onc
 `coop push` and `coop pull` sync files between host and guest. Both work while an editor is connected; there is no need to disconnect.
 
 Watch for conflicts. `coop push` overwrites guest files, and `coop pull` overwrites local files. Both commands check for uncommitted git changes and refuse to proceed unless you pass `--force`.
+
+For an existing host Git repository, choose `coop pull --delete` to mirror the
+guest (including removal of host-only files and refs), or `coop pull
+--exclude-git` to copy files additively while preserving host Git metadata.
+`--force` only bypasses the dirty check; it does not bypass this choice. Avoid
+concurrent Git operations during transfers.

docs/getting-started.md

@@ -336,12 +336,17 @@ Push local changes into a running VM:
 coop push
 ```
 
-Pull guest changes back to the host:
+Mirror guest changes back to the host, including deletions:
 
 ```
-coop pull
+coop pull --delete
 ```
 
+This can remove host-only files and Git branches, even with a clean working
+tree. To copy files additively while preserving host Git metadata, use
+`coop pull --exclude-git`. Ordinary additive pulls refuse to overlay an
+existing Git repository; see [workspace sync](workspaces.md#pulling-guest-to-host).
+
 Both commands default to the workspace path recorded by `coop up`. Override with `--dir`:
 
 ```

docs/testing.md

@@ -43,6 +43,12 @@ boot session through `post_start` for fresh `up`, `start`, and a stopped-project
 `up`, checks that model credentials still arrive, and witnesses normal GitHub
 forwarding on an intervening invocation without the flag.
 
+The `--full` workspace phase exercises mirror pulls: packed refs, guest-deleted
+files and branches, incoming ignore rules, Git exclusions, additive-overlay
+refusal, and refusal to fall back to tar when mirror mode lacks rsync. Library
+workspace tests additionally use local Git and rsync, which must be on `PATH`.
+Run this phase on both Firecracker and Lima in copy mode.
+
 When adding new features, consider whether they should be covered here. New
 commands or guest-visible changes are good candidates for a new test phase.
 

docs/trust-model.md

@@ -61,6 +61,13 @@ user launched it.
   descriptor. Other paths remain **host** paths: `MountGuard::simple` is a
   loop mount, not a chroot, so the traversal rule below still applies to the
   hostname and network-config writes. Those paths are not currently validated.
+  `pull --delete` explicitly authorizes removal of non-excluded host paths
+  absent from the guest, including host-only Git refs. It requires rsync and
+  does not fall back to tar. `--force` bypasses only the dirty check; additive
+  pulls cannot overwrite existing root Git metadata unless it is excluded.
+  Root gitfiles and symlinked `.git` entries require `--exclude-git`. These
+  preflight checks are compatibility guards, not protection against a guest
+  changing its files during transfer.
 - **Guest command output read by the host.** e.g. `check_guest_dirty` reads
   `git status --porcelain` from the guest. Today this only gates control flow /
   is printed to the user — it is never fed into `sh -c` on the host. Keep it

docs/workspaces.md

@@ -105,16 +105,46 @@ Transfer method selection is automatic:
 ## Pulling: guest to host
 
 ```bash
-coop pull                                       # uses host_path from workspace.json
+coop pull --delete                              # mirror back to the recorded host path
 coop pull --dir ./local-copy                    # pull into a specific directory
-coop pull --force                               # skip local dirty check
-coop pull my-instance                           # target a specific instance
+coop pull --delete --force                       # mirror, skipping the local dirty check
+coop pull my-instance --exclude-git              # additive copy, preserving host Git metadata
 coop pull my-instance --dir ./local-copy        # combined
 ```
 
 Before overwriting the local destination, `pull` runs `git status --porcelain` against it. If the directory has a `.git` and any uncommitted changes (tracked or untracked), pull refuses unless you pass `--force`. Unlike push's guest-side check, the local check does not inspect unpushed commits — committing your local work first is enough to satisfy it.
 
-The destination directory is created if absent. Transport selection follows the same rsync-then-tar-pipe order. The tar-pipe fallback verifies SHA-256 checksums end-to-end.
+Without `--delete`, pull is additive: destination-only files remain. An additive
+pull refuses to overwrite an existing destination `.git` directory, even with
+`--force`, because copying Git metadata without deletions can leave stale loose
+refs that override newer packed refs. Choose `--delete` to mirror the guest or
+`--exclude-git` to preserve host Git metadata. Pulling into a fresh directory
+can include Git metadata normally.
+
+`--delete` removes non-excluded destination paths absent from the guest,
+including host-only Git branches and commits' references. A clean working tree
+does **not** protect host-only committed work. This is a filesystem mirror, not
+a Git fetch or merge. `--force` only skips the dirty check; it never enables
+deletion or bypasses the additive Git guard. A failed Git status check also
+blocks pull unless `--force` is supplied.
+
+Mirror mode requires working rsync on both host and guest and checks that
+before creating or modifying the destination. It never falls back to tar.
+Rsync uses `--delete-after` so incoming `.gitignore` rules are available before
+deletions; default exclusions and matching ignore rules protect host paths.
+Changing or removing ignore rules can therefore change which paths are deleted.
+If a `.gitignore` file itself is removed, rsync can retain its previously
+protected files until a subsequent pull.
+`--delete --exclude-git` mirrors files while preserving host Git metadata.
+
+When including Git metadata, a root `.git` file (linked worktree) or symlink
+on either side is unsupported; use `--exclude-git` instead. On pull this flag
+excludes `.git` entries of every type, including files and symlinks.
+
+The destination directory is created if absent. Additive transfers use rsync
+when available in the guest, otherwise tar-pipe. The tar-pipe fallback verifies
+SHA-256 checksums end-to-end. Transfers are not atomic snapshots: avoid concurrent
+Git operations in either repository and treat interrupted transfers as incomplete.
 
 ## Default exclusions
 

src/lib.rs

@@ -491,10 +491,13 @@ enum Commands {
         /// Local directory to pull into (defaults to `workspace.json` `host_path`)
         #[arg(long)]
         dir: Option<String>,
-        /// Overwrite local changes without confirmation
+        /// Skip the local dirty check (does not bypass the Git overlay guard)
         #[arg(long)]
         force: bool,
-        /// Skip the `.git` directory in this transfer
+        /// Delete non-excluded destination paths absent from the guest (requires rsync)
+        #[arg(long)]
+        delete: bool,
+        /// Skip all `.git` entries in this transfer
         #[arg(long)]
         exclude_git: bool,
     },
@@ -1421,10 +1424,21 @@ pub fn run() -> Result<()> {
             name,
             dir,
             force,
+            delete,
             exclude_git,
         } => {
             let running = resolve_running(&be, &cfg, name.as_ref())?;
-            workspace::pull(&running, dir.as_deref(), force, exclude_git)
+            workspace::pull(
+                &running,
+                dir.as_deref(),
+                force,
+                exclude_git,
+                if delete {
+                    workspace::PullMode::Mirror
+                } else {
+                    workspace::PullMode::Additive
+                },
+            )
         }
         Commands::Exec { name, command } => cmd_exec(&be, &cfg, name.as_ref(), &command),
         Commands::Editor {
@@ -2252,6 +2266,26 @@ token = "test-pat"
         assert!(!force);
     }
 
+    #[test]
+    fn pull_delete_is_explicit_and_independent_of_force() {
+        for (args, expected_delete, expected_force) in [
+            (vec!["pull"], false, false),
+            (vec!["pull", "--force"], false, true),
+            (vec!["pull", "--delete"], true, false),
+            (
+                vec!["pull", "--delete", "--exclude-git", "--force"],
+                true,
+                true,
+            ),
+        ] {
+            let super::Commands::Pull { delete, force, .. } = parse(&args).command else {
+                panic!("expected Pull variant");
+            };
+            assert_eq!(delete, expected_delete);
+            assert_eq!(force, expected_force);
+        }
+    }
+
     #[test]
     fn pull_positional_name_and_dir_flag_parse() {
         let cli = parse(&["pull", "myvm", "--dir", "./out", "--force"]);