Skip to content

fix: lake: skip artifacts already present when staging or unstaging#14002

Closed
marcelolynch wants to merge 1 commit into
leanprover:masterfrom
marcelolynch:lake-cache-skip-existing-artifacts
Closed

fix: lake: skip artifacts already present when staging or unstaging#14002
marcelolynch wants to merge 1 commit into
leanprover:masterfrom
marcelolynch:lake-cache-skip-existing-artifacts

Conversation

@marcelolynch

Copy link
Copy Markdown
Contributor

This PR makes lake skip files that already exist for lake cache unstage, which currently copies artifacts into the local cache unconditionally. Artifacts cached by builds are read-only, so unstaging over a cache that already holds them failed with a permission error. The contents are identical by content-addressing, so skipping is correct.

Closes #13997

`lake cache unstage` copies artifacts into the local cache unconditionally, and artifacts cached by builds are read-only, so unstaging over a cache that already holds them failed with a permission error. Skip files that already exist — content-addressed names guarantee identical contents — in both `stage` and `unstage`. The existing stage/unstage tests always emptied the cache before unstaging, which is why this went unnoticed; the cache test now also unstages over a populated cache.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@marcelolynch marcelolynch requested a review from tydeu as a code owner June 11, 2026 01:42
@marcelolynch marcelolynch changed the title fix: skip artifacts already present when staging or unstaging fix(lake): skip artifacts already present when staging or unstaging Jun 11, 2026
@marcelolynch marcelolynch changed the title fix(lake): skip artifacts already present when staging or unstaging fix: lake: skip artifacts already present when staging or unstaging Jun 11, 2026
@tydeu

tydeu commented Jun 13, 2026

Copy link
Copy Markdown
Member

Thanks for catching this error and proposing a test! I am implementing a variant of this PR as part of #14036.

@tydeu

tydeu commented Jun 23, 2026

Copy link
Copy Markdown
Member

Closed after confirming with Marcelo that this has been suitably addressed.

@tydeu tydeu closed this Jun 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

lake cache unstage fails with "permission denied" when the artifact cache already holds the artifact

2 participants