diff --git a/.gitea/scripts/prepare-mathlib.sh b/.gitea/scripts/prepare-mathlib.sh index f407a58..5f55227 100755 --- a/.gitea/scripts/prepare-mathlib.sh +++ b/.gitea/scripts/prepare-mathlib.sh @@ -27,7 +27,14 @@ else cd "$DIR" elan toolchain install "$(cat lean-toolchain)" >&2 timeout 1800 lake update >&2 - timeout 5400 lake exe cache get >&2 + # The cache is ~9,000 files; a few transient transfer failures are normal, and a + # re-run fetches only what is still missing (downloads persist in ~/.cache/mathlib). + for attempt in 1 2 3 4; do + if timeout 5400 lake exe cache get >&2; then break; fi + [ "$attempt" -eq 4 ] && { echo "prepare-mathlib: cache get failed 4 times" >&2; exit 1; } + echo "prepare-mathlib: cache get attempt $attempt failed; retrying" >&2 + sleep $((attempt * 15)) + done start=$(date +%s) timeout 1200 lake env lean LeanBench.lean >&2 || { status=$? diff --git a/docker/Dockerfile b/docker/Dockerfile index cd706e8..a6dc00d 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -46,7 +46,12 @@ RUN elan toolchain install "$(cat lean/lean-toolchain)" \ RUN cd lean && timeout 1800 lake update # Mathlib's prebuilt artifacts. Slow, large, and cached as its own layer. -RUN cd lean && timeout 5400 lake exe cache get +# A handful of the ~9,000 transfers failing is normal; a re-run fetches only what is missing. +RUN cd lean && for attempt in 1 2 3 4; do \ + timeout 5400 lake exe cache get && break; \ + [ "$attempt" -eq 4 ] && exit 1; \ + echo "cache get attempt $attempt failed; retrying" >&2; sleep $((attempt * 15)); \ + done # The honest check that this image can do its job, and it is exactly what # verification does at runtime: elaborate a file against Mathlib with `lake env lean`.