From d16134137f6d10801fa7caacbd079763404f5fc1 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 13 Jun 2026 16:39:48 +0200
Subject: [PATCH] fix(mathlib): always lake build after cache get (fill
 incomplete-cache gaps)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Nightly cold-cache CI failed intermittently (06-11/06-12, self-healed 06-13):
`lake exe cache get` returned 0 but Mathlib's upstream Azure cache was
momentarily incomplete ('some files were not found'), so lib/Mathlib came out
empty and the CC-006 consolidation check (correctly) failed the fetch. The
source-build fallback only fired on a NON-ZERO cache get, so a 0-exit-but-empty
cache slipped through.

Fix: retry cache get for transient misses, then ALWAYS run `lake build Mathlib`
— the canonical workflow. Fast no-op when the cache was complete; fills any
missing oleans otherwise. (aeneas_lean_lib already always builds, so it was
unaffected.)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 lean/private/repo.bzl | 39 +++++++++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 14 deletions(-)

diff --git a/lean/private/repo.bzl b/lean/private/repo.bzl
index 5494a0b..19f1b5b 100644
--- a/lean/private/repo.bzl
+++ b/lean/private/repo.bzl
@@ -180,25 +180,36 @@ def _mathlib_repo_impl(rctx):
     if result.return_code != 0:
         fail("lake update failed:\n" + result.stderr)
 
-    # Download pre-built oleans (fast path)
+    # Download pre-built oleans (fast path). Retry a few times to ride out
+    # transient upstream cache misses: `lake exe cache get` can return 0 yet
+    # leave gaps when Mathlib's Azure cache is momentarily incomplete ("some
+    # files were not found in the cache").
+    for attempt in range(3):
+        result = rctx.execute(
+            [str(lake), "exe", "cache", "get"],
+            environment = env,
+            timeout = 1200,
+            quiet = False,
+        )
+        if result.return_code == 0:
+            break
+        # buildifier: disable=print
+        print("WARNING: `lake exe cache get` attempt {} failed; retrying.".format(attempt + 1))
+
+    # ALWAYS follow with `lake build Mathlib` — the canonical Mathlib workflow.
+    # It is a fast no-op when the cache supplied every olean, and fills any the
+    # cache was missing. Building only on a non-zero `cache get` (as before) let
+    # a 0-exit-but-incomplete cache through, leaving lib/Mathlib empty and
+    # tripping the consolidation check downstream (an intermittent nightly
+    # failure when upstream Mathlib cache was incomplete).
     result = rctx.execute(
-        [str(lake), "exe", "cache", "get"],
+        [str(lake), "build", "Mathlib"],
         environment = env,
-        timeout = 1200,
+        timeout = 7200,
         quiet = False,
     )
     if result.return_code != 0:
-        # Pre-built cache may be unavailable — fall back to building from source
-        # buildifier: disable=print
-        print("WARNING: pre-built Mathlib cache unavailable, building from source (this will take a long time)...")
-        result = rctx.execute(
-            [str(lake), "build", "Mathlib"],
-            environment = env,
-            timeout = 7200,
-            quiet = False,
-        )
-        if result.return_code != 0:
-            fail("Failed to build Mathlib:\n" + result.stderr)
+        fail("Failed to build Mathlib (after cache get):\n" + result.stderr)
 
     # Consolidate all package oleans into lib/
     # Lake v4 stores oleans at: .lake/packages/<name>/.lake/build/lib/lean/<Module>/...