Skip to content

Commit 3548d6b

Browse files
bryangingechenriccardobrasca
authored andcommitted
ci: skip cache warmup if the "previous" commit uses a different toolchain (leanprover-community#37653)
leanprover-community#37564 changed `cache` so that it looks for a bundled `leantar` rather than downloading a copy. This caused the "warmup cache" step introduced in leanprover-community#36623 to break since the "previous" commit being fetched could be using an older toolchain. We fix this by simply skipping getting the cache for the previous commit if the toolchain differs. It's likely that the oleans are all invalidated anyways. Prepared with claude code.
1 parent 9fee804 commit 3548d6b

1 file changed

Lines changed: 13 additions & 7 deletions

File tree

.github/workflows/build_template.yml

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -310,13 +310,19 @@ jobs:
310310
# cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
311311
echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
312312
if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
313-
git checkout "$PREV_SHA"
314-
../tools-branch/.lake/build/bin/cache get
315-
# Run again with --repo, to ensure we actually get the oleans.
316-
../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
317-
318-
echo "Switching back to branch head"
319-
git checkout "$ORIG_SHA"
313+
# Skip warmup if the previous commit uses a different toolchain
314+
PREV_TOOLCHAIN=$(git show "$PREV_SHA:lean-toolchain" 2>/dev/null || true)
315+
if [[ "$PREV_TOOLCHAIN" != "$(cat lean-toolchain)" ]]; then
316+
echo "Previous commit $PREV_SHA uses a different toolchain ($PREV_TOOLCHAIN); skipping warmup."
317+
else
318+
git checkout "$PREV_SHA"
319+
../tools-branch/.lake/build/bin/cache get
320+
# Run again with --repo, to ensure we actually get the oleans.
321+
../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
322+
323+
echo "Switching back to branch head"
324+
git checkout "$ORIG_SHA"
325+
fi
320326
else
321327
echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
322328
fi

0 commit comments

Comments
 (0)