feat: resume interrupted downloads via HTTP Range headers #191
+161
−26
Conversation
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
Port download resumption from rustup. When a download fails due to a network error, elan now automatically retries once, resuming from where it left off using HTTP Range headers. Also adds a stall timeout (30s at <10 bytes/sec) so downloads no longer hang indefinitely on unreliable connections. Closes https://github.com/leanprover/elan/issues/XXX Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Address review feedback: - Detect when server returns 200 instead of 206 (ignoring Range header) and fall back to a fresh download to avoid data corruption - On HTTP 416 (Range Not Satisfiable), fall back to fresh download instead of permanently failing - Only treat read-open errors as "no file" for NotFound; propagate other errors (permissions, I/O) instead of silently appending Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Any failure to open the partial file (not just NotFound) falls back to downloaded_so_far=0. This is safe because truncate(downloaded_so_far==0) ensures a fresh start, and avoids turning a recoverable situation (e.g. permission error on a temp file) into a hard failure. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Member
|
Tested? :) |
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 ports download resumption from rustup. When a download fails due to a network error, elan now automatically retries once, resuming from where it left off using HTTP Range headers. Also adds a stall timeout (30s at <10 bytes/sec) so downloads no longer hang indefinitely on unreliable connections.
Discussed at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.60elan.60.20can't.20resume.20download/near/572363501
Changes
Core download library (
src/download/src/lib.rs):curl::download()acceptsresume_from: u64and callshandle.resume_from()(matching rustup)resume_from(server reports remaining bytes; progress needs total)low_speed_limit(10)+low_speed_time(30s)aborts hung transfersdownload_to_path_with_backend()handles partial files: checks size, opens in append mode, seeks to endRetry logic (
src/elan-utils/src/utils.rs):resume_from_partial=trueProgress display (
src/elan-cli/download_tracker.rs):ResumingPartialDownloadnotification, resetting speed tracking on resume🤖 Prepared with Claude Code