Commit 2026-08-28 00:22 5ba95124

fix(cache): retry transport errors, improve transfer robustness (#43145) Since CI cache reads moved to cache.mathlib.org (#42777), the transport is HTTP/2: one connection carries many parallel transfers, and a dropped connection fails them all at once with Send failure: Broken pipe. curl's --retry does not cover transport errors, so a short network fault fails the job. Seven bors runs failed this way in six days (example: 14 of 8750 files, one connection); the same step failed zero times in the previous four weeks (429 runs). Fix: --retry 5 --retry-all-errors on the parallel download path and the upload path (curlRetryArgs). curl retries a failed transfer on a fresh connection, with exponential backoff. An HTTP 4xx is not a curl error on these paths, so a 404 miss never retries and the container fallback works as before.

• The serial download path keeps plain --retry 5: it serves curls below 7.71, which reject --retry-all-errors. It now drops --fail and decides by the written-out status, like the parallel path, so no download path treats a miss as an error.
• The marker probe keeps no retry flags: it is diagnostic, a false negative is cheap, and retry backoff would stall the up-to-50-probe cache query walk against an unreachable endpoint. It adds --connect-timeout 10 --max-time 30 as time bounds.
• A retried PUT is safe: a non-overwrite put sends If-None-Match: *, and a duplicate answers 409/412, which the upload path already excuses.
• validateCurl raises the parallel-mode floor to curl 7.75: --retry-all-errors needs 7.71, and the per-transfer JSON report carries exitcode and errormsg from 7.75 on. CI runners have 8.5; old Linux curls already fetch a static 7.88.1. An outage that outlives the five retries still fails the step. This PR also fixes five pre-existing bugs in these paths:
• A transfer can die after the 200 status arrives: curl reports http_code: 200 with a nonzero exit code, but the code matched the status alone and renamed the truncated part file into the cache, where only a manual clean removed it. A transfer now counts as delivered only when curl also exits cleanly. The verdict is a pure table with unit tests (classifyDownload / classifyUpload).
• An error answer to a PUT carries a body, which landed on stdout and glued to curl's per-transfer JSON report. The report did not parse, so a 409 did not count as a skip and a 403/404/500 did not count as a failure — the upload step passed either way. The put config now discards each response body, so stdout carries only the reports.
• On a miss, the parallel path left the error body behind as a .part file. It now removes the file, like the serial path.
• A 404 answer to a PUT was excused as a cache miss. It now counts as an upload failure.
• The marker PUTs carry their credential in the curl argument list, and a failure message echoed that list. Their failure messages now name the command, its exit state, and stderr only. (In CI the token is also masked in logs; this guards local runs and transformed output.) Tested with lake build cache, the cache-test suite, and a forced re-download of 64 files through cache.mathlib.org. Against a local server that truncates every body, all 64 transfers fail and no truncated or partial file stays in the cache; against a server that answers 404, misses stay quiet and leave no partial files. For uploads, a put against a local server that answers 409 with an error body skips and exits 0; against a 404 server it reports the failed blob by URL and exits 1. Two ci_dev runs built the branch's cache tool in CI: the download path served through cache.mathlib.org, and the upload job wrote 3 files to the forks container over OIDC.