fix: lake: gracefully handle curl and IO errors during transfer - #14651
Merged
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
tydeu
marked this pull request as ready for review
August 2, 2026 03:31
kim-em
added a commit
to TauCetiProject/TauCeti
that referenced
this pull request
Aug 4, 2026
The stale-`s.didError` read that forces us to grep the fetch log is fixed by leanprover/lean4#14651, which missed v4.33.0-rc2 by hours and was not backported to releases/v4.33.0, so it first ships in v4.34.0. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 6, 2026
kim-em
added a commit
to TauCetiProject/TauCeti
that referenced
this pull request
Aug 6, 2026
The comment attributed partial fetches to Cloudflare rate-limiting the public `*.r2.dev` host, which was replaced by cache.taucetiproject.org. The cause is now known: leanprover/lean4#14651 downloads to a temporary path and renames on success, and tolerates an unreadable artifact instead of aborting the batch. It lands in v4.34.0-rc1. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
kim-em
added a commit
to TauCetiProject/TauCeti
that referenced
this pull request
Aug 6, 2026
Replace the stale r2.dev rate-limiting explanation with the actual cause: leanprover/lean4#14651, landing in v4.34.0-rc1. 🤖 Prepared with Claude Code
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes a number of ways a failed artifact transfer in
lake cache get/lake cache putcould fail to be recorded or could lead to an early abort of the entire transfer batch. Sometimes this would leave a corrupted artifact in the local Lake cache, which could break downstream builds.The transfer now handles any form of IO error with a custom error message, cross-references with curl's reported
exitcodeto determine errors, and stores downloaded artifacts in a sibling.tmpfile before doing an atomic rename.🤖 Diagnosed and reviewed by Claude Code