[Merged by Bors] - fix(cache): time out stalled downloads and retry hard failures in a fresh pass by marcelolynch · Pull Request #45096 · leanprover-community/mathlib4

marcelolynch · 2026-10-20T17:54:53Z

cache get can lose a few downloads when a transfer stops early, or when a connection freezes and curl waits without a time limit. On 2026-10-27 a frozen connection held a CI job for 95 minutes on 5 of 9,080 files.

The download curl runs with --connect-timeout 30 --speed-time 30 --speed-limit 1. A connection setup that takes more than 30 s, or a transfer that receives no bytes for 30 s, fails with curl exit 28. curl retries a failed connection setup on a new connection. After the first pass over all cache locations, the tool retries the failed downloads once, in new curl processes. curl retries a timed-out transfer on the same connection. The new process of the second pass opens a new connection, which recovers the file.

A healthy get has a first-byte time under 1 s, and a slow transfer keeps its bytes flowing, so the limit trips on a frozen connection only. When every transfer fails, the second pass repeats the first, so the time to failure about doubles.

Tested against a local proxy that interrupts transfers, and against a local HTTP/2 server that leaves 3 of 94 requests unanswered on the first connection. The tool recovers in both tests and exits 1 when a failure persists. Without the stall flags it hangs in the second test.

depends on: [Merged by Bors] - fix(Cache): retry uploads and report missing transfers #44940

🤖

curl below 8.14.0 truncates the output file before it retries a transfer that received a body. It cannot truncate the null device, so it abandons the transfer without a retry or a report (curl issue leanprover-community#17371). The upload now sends every response body to one regular file. The jobs that run the cache tool on a GitHub runner use ubuntu-24.04 and have a timeout: curl 8.18.0 on ubuntu-26.04 hangs on a pending retry in parallel mode (curl issue leanprover-community#20669).

…ery transfer

…obs on ubuntu-latest curl 8.18 hangs on a pending retry in parallel mode (curl issue leanprover-community#20669), and Ubuntu 26.04 ships it. The tool already downloads a static curl for versions that are too old; 8.18 now takes the same path. The upload and Post-Build jobs get a timeout.

Name the error first, then add a note or a hint. Use one message for every failure case.

…UploadFix # Conflicts: # Cache/CI.md

curl 8.18 and 8.19 hang on a pending retry in parallel mode (curl issue leanprover-community#20669). The download path now treats them like an old curl: Linux fetches the static binary, other platforms run serial downloads. Uploads already require curl 8.20.

Uploads require curl 8.20. curl 8.14 fixed the retry of a transfer that received a body while writing to the null device (curl issue leanprover-community#17371), so the shared regular-file sink is unnecessary.

`test_curlGetWriteOut_real_curl` runs one curl `file://` copy.

The release has x86_64 and aarch64 assets. The binary's file name carries the version, so an existing download refreshes once.

Ubuntu 26.04 ships curl 8.18, which the tool rejects for parallel transfers, so the Linux job covers the static curl fallback. The Windows job covers the download path with the system curl. actionlint does not know the ubuntu-26.04 label yet; the config file declares it.

After the location chain, walk it once more over the hard failures that no location served, in a fresh curl. curl's own retries share one process's connection pool, and a reset pool stalls all six attempts while the sibling transfers of the same run complete. The exit code counts the failures left after that pass.

github-actions · 2026-10-20T17:55:58Z

PR summary afeb1e2b37

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ curlStallArgs

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 afeb1e2).

+0 new declarations
−0 removed declarations

No declaration differences.

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

Current commit afeb1e2b37
Reference commit 3aae103a67

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).

actionlint reads one config file, and a new actionlint.yaml shadowed the existing actionlint.yml with the self-hosted labels.

curl 8.18 and 8.19 hang on a pending retry in parallel mode (curl issue leanprover-community#20669). Ubuntu 26.04 and Fedora 44 ship 8.18, so sending them to the static curl would put a self-built binary on most machines, and the static binary cannot find Fedora's CA bundle. The tool now keeps the system curl on these versions and omits curl's retry flags. `CurlMode` carries the choice from `validateCurl` to the download pass. The post-build job installs the pinned curl so CI keeps retries after `ubuntu-latest` moves to Ubuntu 26.04. The `cache-get` job on `ubuntu-26.04` checks the retry-free mode.

… 2026/10/CacheGetRetryPass # Conflicts: # Cache/Requests.lean

A parallel pass that curl ends before it reports every transfer counts the gap as failures (leanprover-community#44940), but those failures have no hashes, so the retry pass skipped them and the exit code dropped them. Every file such a pass leaves unserved now joins the retry pass. A miss retried there reads as a miss again.

… pass

mathlib-dependent-issues · 2026-10-21T23:48:25Z

This PR/issue depends on:

~~[Merged by Bors] - fix(Cache): retry uploads and report missing transfers #44940~~
By Dependent Issues (🤖). Happy coding!

mathlib-merge-conflicts · 2026-10-22T01:10:26Z

This pull request has conflicts, please merge master and resolve them.

…etryPass # Conflicts: # .github/actionlint.yml # .github/workflows/build_template.yml # .github/workflows/cache_test.yml # Cache/CI.md # Cache/IO.lean # Cache/README.md # Cache/Requests.lean # Cache/Test.lean # Cache/Upload/Curl.lean

…etryPass

Give the download curl `--speed-time 30 --speed-limit 1`. A transfer that receives no bytes for 30 s ends with curl exit 28. The retry pass then fetches it in a fresh curl, over a new connection. Without a stall limit, a frozen connection holds `cache get` until the network closes it. A CI job waited 95 minutes on 5 of 9,080 files.

State what each docstring describes: the stall flags, the failed-hash set, the per-location download, the download result, and the two passes. The comment on a curl run that reports fewer transfers than requested says that the round marks the unserved files as failed.

bryangingechen · 2026-10-28T17:29:02Z

+frozen connection, so we rely on the second download pass in `downloadFiles` to actually
+retry these. -/
+def curlStallArgs : Array String :=
+  #["--speed-time", "30", "--speed-limit", "1"]


Maybe also include something like --connect-timeout 30 here too to catch hanging connects?

nice, that makes sense

bryangingechen · 2026-10-28T22:00:46Z

Thanks!
bors r+

…resh pass (#45096) `cache get` can lose a few downloads when a transfer stops early, or when a connection freezes and curl waits without a time limit. On 2026-10-27 a frozen connection held a CI job for 95 minutes on 5 of 9,080 files. The download curl runs with `--connect-timeout 30 --speed-time 30 --speed-limit 1`. A connection setup that takes more than 30 s, or a transfer that receives no bytes for 30 s, fails with curl exit 28. curl retries a failed connection setup on a new connection. After the first pass over all cache locations, the tool retries the failed downloads once, in new `curl` processes. curl retries a timed-out transfer on the same connection. The new process of the second pass opens a new connection, which recovers the file. A healthy get has a first-byte time under 1 s, and a slow transfer keeps its bytes flowing, so the limit trips on a frozen connection only. When every transfer fails, the second pass repeats the first, so the time to failure about doubles. Tested against a local proxy that interrupts transfers, and against a local HTTP/2 server that leaves 3 of 94 requests unanswered on the first connection. The tool recovers in both tests and exits 1 when a failure persists. Without the stall flags it hangs in the second test. - [x] depends on: #44940 🤖

mathlib-bors · 2026-10-28T23:23:02Z

Pull request successfully merged into master.

Build succeeded:

marcelolynch added 22 commits October 16, 2026 09:29

fix(Cache): fail a transfer pass when curl stops before it reports ev…

b7421e8

…ery transfer

fix(Cache): consolidate curl upload checks and diagnostics

b84928b

refactor(Cache): use one curl version threshold

22eeb21

fix(Cache): require a recent system curl for uploads

0f144d9

fix(Cache): pin curl in upload jobs

4949cf0

refactor(Cache): simplify upload report tracking

330f064

chore(CI): reword the post-build cache verification messages

f6885d5

Name the error first, then add a note or a hint. Use one message for every failure case.

chore(CI): state that no action is needed when a PR changes Cache/

c71d292

chore(CI): drop the cause from the cache verification hint

ce77127

chore(CI): report a skipped cache check as a notice

b84dae2

chore(CI): trim the skipped cache check notice

9b5482d

chore(CI): suggest an empty commit to re-run CI

975c2e7

Merge remote-tracking branch 'upstream/master' into 2026/10/CacheCurl…

09ddcf8

…UploadFix # Conflicts: # Cache/CI.md

fix(Cache): send upload response bodies to the null device

3c1b398

Uploads require curl 8.20. curl 8.14 fixed the retry of a transfer that received a body while writing to the null device (curl issue leanprover-community#17371), so the shared regular-file sink is unnecessary.

chore(Cache): list the local curl copy in the test header

f8cdccd

`test_curlGetWriteOut_real_curl` runs one curl `file://` copy.

chore(Cache): download static curl 8.23.0

10497ae

The release has x86_64 and aarch64 assets. The binary's file name carries the version, so an existing download refreshes once.

chore(Cache): drop a blank line after the unreported-transfers test

4ca390a

github-actions Bot added the CI Modifies the continuous integration setup or other automation label Oct 20, 2026

marcelolynch added 5 commits October 20, 2026 15:03

ci: declare the ubuntu-26.04 label in the existing actionlint config

2e45d21

actionlint reads one config file, and a new actionlint.yaml shadowed the existing actionlint.yml with the self-hosted labels.

refactor(cache): simplify download retry passes

7894b80

Merge remote-tracking branch 'origin/2026/10/CacheCurlUploadFix' into…

3f6f98b

… 2026/10/CacheGetRetryPass # Conflicts: # Cache/Requests.lean

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 21, 2026

chore(cache): reword the comment on unreported transfers in the retry…

4712fbb

… pass

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 21, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 22, 2026

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 22, 2026

marcelolynch mentioned this pull request Oct 22, 2026

ci: warm master's build from the staging cache artifact #45169

Draft

marcelolynch added 2 commits October 22, 2026 13:05

doc(cache): state what the download counts hold after the retry pass

cc4fb24

refactor(cache): trim retry state and clarify download results

879b31a

marcelolynch marked this pull request as ready for review October 23, 2026 18:21

marcelolynch added 3 commits October 28, 2026 00:05

Merge remote-tracking branch 'upstream/master' into 2026/10/CacheGetR…

6699902

…etryPass

marcelolynch changed the title ~~fix(cache): retry hard download failures in a fresh pass~~ fix(cache): time out stalled downloads and retry hard failures in a fresh pass Oct 28, 2026

marcelolynch added 4 commits October 28, 2026 10:06

doc(cache): shorten the download docstrings and comments

6a33d85

doc(cache): explain the stall flags

f2a7677

doc(cache): say which retries reuse the frozen connection

f8c676c

doc(cache): say that the second download pass retries a frozen transfer

5a6d6ce

bryangingechen reviewed Oct 28, 2026

View reviewed changes

fix(cache): time out stalled connects

afeb1e2

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Oct 28, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Oct 28, 2026

mathlib-bors Bot changed the title ~~fix(cache): time out stalled downloads and retry hard failures in a fresh pass~~ [Merged by Bors] - fix(cache): time out stalled downloads and retry hard failures in a fresh pass Oct 28, 2026

mathlib-bors Bot closed this Oct 28, 2026

Navigation Menu

Repository navigation

[Merged by Bors] - fix(cache): time out stalled downloads and retry hard failures in a fresh pass - #45096

[Merged by Bors] - fix(cache): time out stalled downloads and retry hard failures in a fresh pass#45096
marcelolynch wants to merge 39 commits into
leanprover-community:masterfrom
marcelolynch:2026/10/CacheGetRetryPass

marcelolynch commented Oct 20, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 20, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

mathlib-dependent-issues Bot commented Oct 21, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 22, 2026

Uh oh!

bryangingechen Oct 28, 2026

Uh oh!

marcelolynch Oct 28, 2026

Uh oh!

bryangingechen commented Oct 28, 2026

Uh oh!

mathlib-bors Bot commented Oct 28, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

marcelolynch commented Oct 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary afeb1e2b37

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-dependent-issues Bot commented Oct 21, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 22, 2026

Uh oh!

bryangingechen Oct 28, 2026

Choose a reason for hiding this comment

Uh oh!

marcelolynch Oct 28, 2026

Choose a reason for hiding this comment

Uh oh!

bryangingechen commented Oct 28, 2026

Uh oh!

mathlib-bors Bot commented Oct 28, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

marcelolynch commented Oct 20, 2026 •

edited

Loading

github-actions Bot commented Oct 20, 2026 •

edited

Loading