lake cache get fails a whole batch after one transient network failure

Description

lake cache get and lake cache put transfer a batch of artifacts with one curl invocation. When one transfer fails in a transient way, the whole batch fails. Lake does not retry the failed transfer.

curl --retry does not prevent this. It retries only timeouts and a fixed set of response codes (408, 429, 500, 502, 503, 504). It does not retry a connection that drops mid-body. It also cannot detect a corrupted body: when the response has no Content-Length, a stream that ends early looks like a complete transfer. Only Lake's content hash check can catch that case.

Context

Mathlib runs a daily CI job that exercises Lake's artifact cache against a remote bucket. The job downloads the full cache (~8300 artifacts) with lake cache get. One dropped connection failed the whole job (log).

Steps to Reproduce

The mock cache server in tests/lake/tests/cacheTransfer/server.py reproduces the failure classes deterministically. The steps below use its reset fault mode, which drops every request without a response.

# Start the mock server; it writes its port to a file when it is ready
python3 tests/lake/tests/cacheTransfer/server.py \
  --store /tmp/store --port-file /tmp/port > /tmp/server.log 2>&1 &
sleep 1
URL="http://127.0.0.1:$(cat /tmp/port)"

# A minimal workspace and a mappings file that names one artifact
mkdir -p /tmp/repro && cd /tmp/repro
printf 'name = "repro"\n' > lakefile.toml
printf '"2026-03-17"\n["aaaaaaaaaaaaaaaa","0123456789abcdef.ltar"]\n' > outputs.jsonl

# Fetch the batch through the fault mode
LAKE_CACHE_DIR=.lake/cache \
LAKE_CACHE_ARTIFACT_ENDPOINT="$URL/reset/a0" \
LAKE_CACHE_REVISION_ENDPOINT="$URL/reset/r0" \
lake cache get outputs.jsonl --scope=repro
echo "exit: $?"

# Count the requests that Lake made for the artifact
grep -c 'GET /reset' /tmp/server.log

Expected behavior: Lake retries a transfer that fails in a transient way, and the request count is greater than 1. The batch succeeds when a retry succeeds; this fault is persistent, so the batch fails after the retries. A failure that a retry cannot fix, such as a 404, fails the batch immediately.

Actual behavior: The request count is 1. Lake makes one attempt, the batch fails, and lake cache get exits with code 1:

error: repro: failed to download artifact 0123456789abcdef (status code: 0)
  curl error: Empty reply from server
  local path: .lake/cache/artifacts/0123456789abcdef.ltar
  remote URL: http://127.0.0.1:53646/reset/a0/repro/0123456789abcdef.art
error: repro: failed to download some artifacts
error: repro: curl exited with code 52
exit: 1
requests: 1

Versions

Observed with leanprover/lean4:v4.33.0-rc1 on Linux (ubuntu-latest GitHub runners).
Reproduced on current master (7c90644a5f) on macOS (Darwin 25.4.0, arm64). On master, #14651 reports the failure cleanly, but the batch still fails.

Additional Information

Forensics on the failed CI run

• Two of 8309 downloads failed, 10 ms apart. Both failures are consistent with one dropped connection that carried several multiplexed HTTP/2 streams.
• The artifact bytes in the bucket were correct. They were byte-identical to the uploaded staging files, and all 8309 staged files hash to their names.
• The reported mismatch hash (aab4dd01e694a7f6) is the Lake hash of exactly the first 131072 bytes (128 KiB) of the correct artifact. The stream died mid-body, at a clean buffer boundary.
• The second artifact failed with no such file or directory: its stream died before the first body byte, so curl wrote no output file.

Impact

A CI job that downloads a full cache fails when any single transfer breaks. The data at rest is intact, so a manual rerun succeeds. The failure rate grows with the batch size.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with tests/lake/tests/cacheTransfer/server.py and run its reset fault-mode reproduction to confirm the single-request failure. Then locate the Lake cache transfer entry point and its existing tests; done means transient transfer failures are retried, successful retries allow the batch to finish, and persistent or non-retryable failures still fail as expected.