ci: fetch the Mathlib cache only through the retry loop

Mathlib's post-update hook fetched the cache inside 'lake update', where a few
dropped transfers failed the build before the retries could run. Disable the
hook, retry up to six times, and keep the archives in a BuildKit cache mount so
a retried image build resumes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6

.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

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