coop pull is not --delete-symmetric with push, and can leave the host on a stale git ref

Summary

coop push mirrors with --delete; coop pull does not. Because the pull is additive, anything the guest removed stays on the host. For .git/ specifically this can make the host repo resolve a branch to an older commit than the guest's, with no error — coop pull reports success.

Mechanism

rsync_push appends --delete (src/workspace.rs:761); rsync_pull does not (src/workspace.rs:776-793). The tar-pipe fallback has no equivalent either.

Git resolves loose refs ahead of packed-refs, so:

1. Host has a loose .git/refs/heads/<branch> at commit A — any branch created with git switch -c / git branch before the workspace goes into the guest.
2. Guest commits; its loose ref advances to B.
3. Guest runs git gc or git pack-refs (or gc --auto fires). The guest's loose ref file is deleted and B now lives in packed-refs.
4. coop pull copies the new packed-refs but, lacking --delete, leaves the host's stale loose ref file at A in place.
5. Host git reads the loose ref first, so the branch resolves to A. Commit B is in the object store but unreferenced.

Reproduction

I reproduced the rsync-level behaviour directly rather than through a live VM, since the relevant path is just rsync -a without --delete:

set -e
W=$(mktemp -d); cd $W
git init -q guest && cd guest
git commit -q --allow-empty -m A
git switch -q -c work
git commit -q --allow-empty -m "commit A on work"
A=$(git rev-parse work)
cd $W
cp -R guest host          # host snapshot: loose ref at A

cd guest
git commit -q --allow-empty -m "guest work B"
B=$(git rev-parse work)
git pack-refs --all       # guest-side gc: loose ref removed, B in packed-refs
cd $W

rsync -a guest/ host/     # what rsync_pull does today

echo "A=$A"; echo "B=$B"; echo "host sees: $(git -C host rev-parse work)"

Output:

A=410ce70e567db47f458d3bec7f3972e09ce6fc34
B=f910d32348e6fd86da4f3e1af591a5292b230f97
host sees: 410ce70e567db47f458d3bec7f3972e09ce6fc34

Adding --delete to that rsync makes the host resolve work to B.

Anything downstream that reads the pulled repo — git log, a git fetch from it, a build — sees the pre-gc state and looks perfectly healthy. That's what makes this one unpleasant: there's no signal.

Second, milder symptom, same root cause

Files the guest deleted are never removed on the host, so they come back as untracked files after a pull. Tooling that treats a clean tree as "nothing to do", or a dirty tree as "unsafe to proceed", gets the wrong answer after any guest-side deletion.

Possible fixes

• Pass --delete on rsync_pull. rsync protects excluded files from deletion by default — only --delete-excluded removes them — so the existing .gitignore merge and DEFAULT_EXCLUDES should keep node_modules/ and friends safe on the host. It's still a user-visible behaviour change, so it might want to be opt-in (coop pull --delete) before becoming the default.
• The tar-pipe fallback can't express deletion, so it would need separate handling or a documented caveat.
• Narrower option if a full --delete is too blunt: mirror .git/ exactly (delete-during for that subtree only) and leave the worktree additive. That closes the silent-wrong-commit case — the one with no user-visible signal — and leaves stray files as a documented quirk.

Either way, docs/workspaces.md documents the push-side dirty check in detail but doesn't mention that pull is additive. Worth a note there regardless of which fix lands.

Environment

• coop main @ a34b64f (read from source; docs/workspaces.md describes the same asymmetry)
• Reproduction run on macOS arm64

Happy to send a PR for whichever shape you prefer.

Start in src/workspace.rs at rsync_push around line 761 and rsync_pull around lines 776-793, then inspect the tar-pipe fallback. Reproduce the stale-ref and deleted-file behavior with the shell example, choose and implement a consistent pull policy, and update docs/workspaces.md to describe the resulting behavior.