feat(cache): record transport fields on a failed transfer

[marcelolynch]

Get cache failed 6 of 260 master and staging runs in the week to 2026-09-21. curl receives HTTP 200, then the connection stops mid-body. The log records only this:

6033dea46cb996d6.ltar.2212.part: Transfer failed (error code: 200) (curl exit code: 55): Send failure: Broken pipe

The line omits how far the body got and which edge served it. curl can report both, so append them:

... (curl exit code: 56): Recv failure: Connection reset by peer [bytes=4096/1421777 cf_ray=a3f27b336fa59434-EZE cf_cache_status=HIT http_version=1.1 time_total=0.000788]

bytes gives the truncation point against the size content-length promised, so bytes=0/1421777 means nothing arrived. cf_ray names the colo in its suffix and finds the request in Cloudflare's own logs. cf_cache_status says whether the edge cache served the body. Each value describes curl's final attempt, because --retry hides the earlier ones.

curl's %{json} report carries no response headers, so the get path nests that report inside an object that also records the headers. monitorCurl merges the two only where it reports a failure, so the per-transfer path does the same work as before. A backend that sends no cf-* header contributes fewer pairs.

The upload path shares monitorCurl and keeps writing curl's object on its own. Its failure lines gain bytes, http_version and time_total, and carry no cf-* pair. bytes follows the direction, because curl reports the error response body in size_download: a read counts size_download, a write counts size_upload.

Only the failure line changes. Transfer behavior stays the same.

Tested against local servers that answer 200 and then truncate, with and without cf-* headers; the line above is one such result. lake build cache is clean.

The next failure in CI shows where the body stopped and which colo served it.

🤖 Generated with Claude Code

[github-actions]

PR summary 3b776b8315

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ curlGetWriteOut
+ transferDiagnostics

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3b776b8).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 3b776b8315
Reference commit 09712d488f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[bryangingechen]

Apparently %header{} was only added in curl 7.84.0 which is higher than all the other versions we require.

Claude also suggested a solution using %{header_json} here (which is in 7.83.0) that lets curl take care of escaping, but I guess that only matters if we might add other headers later on.

[marcelolynch]

ah, good catch. this is mainly for CI so I wouldn't sweat not supporting the diagnostics if they're not there, but it needs to be guarded

[bryangingechen]

Sorry if I'm misunderstanding: did you want to add a guard first, or do you think this is ready to go?