Description

lake cache unstage copies every staged artifact into the local artifact cache unconditionally (Lake/CLI/Main.lean, the copyFile stagingPath cachePath loop). Artifacts saved by builds are made read-only (Cache.saveArtifact sets access rights on the cache file, including when it already exists). When the cache already contains one of the staged artifacts the copy fails with EACCES and unstage aborts:

error: failed to copy artifact: permission denied (error code: 13)
  file: .lake/cache/artifacts/<hash>.ltar
error: failed to copy all outputs to the staging directory

Reproduction

In any workspace with enableArtifactCache = true (/ use fresh cache via LAKE_CACHE_DIR=):

lake build -o out.jsonl          # packs module archives; caches them read-only
lake cache stage out.jsonl staging
lake cache unstage staging       # fails: permission denied

Expected behavior

The artifact cache is content-addressed: a file that already exists under the same name has identical contents, so unstage should skip it rather than overwrite it. This is the same assumption Cache.saveArtifact already makes (unless (← cacheFile.pathExists) do ...)

Suggested fix

Skip artifacts whose destination already exists, in both the stage and unstage copy loops.