Skip to content

fix: lake: atomic cache writes for downloads - #16461

Draft
tydeu wants to merge 2 commits into
leanprover:masterfrom
tydeu:lake/atomic-cache-downloads
Draft

tydeu wants to merge 2 commits into
leanprover:masterfrom
tydeu:lake/atomic-cache-downloads

Conversation

@tydeu

@tydeu tydeu commented Nov 13, 2026

Copy link
Copy Markdown
Member

This PR ensures downloaded artifacts are written to the cache automatically. In particular, on-demand artifacts now use a temporary file for their download before being stored as their final name (as lake cache get downloads already do).

Concurrent downloads may still fail as they will still contend for a single temporary file, but they will not publish artifacts with improper hashes to the cache.

@tydeu tydeu added the changelog-lake Lake label Nov 13, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 13, 2026
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants