diff --git a/.gitea/scripts/prepare-mathlib.sh b/.gitea/scripts/prepare-mathlib.sh index 5f55227..32bb92d 100755 --- a/.gitea/scripts/prepare-mathlib.sh +++ b/.gitea/scripts/prepare-mathlib.sh @@ -26,12 +26,13 @@ else cp -r "$SRC" "$DIR" cd "$DIR" elan toolchain install "$(cat lean-toolchain)" >&2 - timeout 1800 lake update >&2 + # Keep the cache fetch out of the post-update hook so it goes through the retries. + MATHLIB_NO_CACHE_ON_UPDATE=1 timeout 1800 lake update >&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 + for attempt in 1 2 3 4 5 6; 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; } + [ "$attempt" -eq 6 ] && { echo "prepare-mathlib: cache get failed 6 times" >&2; exit 1; } echo "prepare-mathlib: cache get attempt $attempt failed; retrying" >&2 sleep $((attempt * 15)) done diff --git a/docker/Dockerfile b/docker/Dockerfile index a6dc00d..cf4c92e 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -43,13 +43,17 @@ RUN elan toolchain install "$(cat lean/lean-toolchain)" \ && elan default "$(cat lean/lean-toolchain)" # Resolve dependencies: clones Mathlib and writes the manifest. -RUN cd lean && timeout 1800 lake update +# Mathlib's post-update hook would fetch the cache here, outside the retry loop below. +RUN cd lean && MATHLIB_NO_CACHE_ON_UPDATE=1 timeout 1800 lake update # Mathlib's prebuilt artifacts. Slow, large, and cached as its own layer. # 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 \ +# The downloaded archives live in a BuildKit cache mount on the build host, so a +# retried build resumes instead of starting over; only the unpacked oleans enter the image. +RUN --mount=type=cache,target=/root/.cache/mathlib \ + cd lean && for attempt in 1 2 3 4 5 6; do \ timeout 5400 lake exe cache get && break; \ - [ "$attempt" -eq 4 ] && exit 1; \ + [ "$attempt" -eq 6 ] && exit 1; \ echo "cache get attempt $attempt failed; retrying" >&2; sleep $((attempt * 15)); \ done