CI: reinstate cache check (#18715)

This check had been removed (cf #17490 and #17491) since it stopped working temporarily. It seems that it works again! 🐙 (According to a comment on #17491, the fix was apparently in leanprover/lean4#5641)
leanprover-community · Nov 7, 2024 · 61ccb31 · 61ccb31
1 parent 3bc5360
commit 61ccb31
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -133,8 +133,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -143,8 +143,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -150,8 +150,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -147,8 +147,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get #Mathlib.Init
-          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all