fix: comment more cache (#17491)

The previous fix was an improvement, but was not aggressive enough in commenting the failing step.

This step used to use `cache` to download the cache for `Mathlib.Init`.  If this was successful, then it would continue trying to download all of the available cache.  Otherwise, it would start with building.  The underlying reason is that if even the cache for `Mathlib.Init` is not there, there is not much of an available cache and there is no need to spend a couple of minutes realizing as much.

However, changes to `lake build --no-buld` (possibly) have made this step always fail to download any cache, so we revert to the old behaviour of trying to get the cache no matter what.

.github/build.in.yml

@@ -134,7 +134,7 @@ jobs:
           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 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

.github/workflows/bors.yml

@@ -144,7 +144,7 @@ jobs:
           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 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

.github/workflows/build.yml

@@ -151,7 +151,7 @@ jobs:
           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 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

.github/workflows/build_fork.yml

@@ -148,7 +148,7 @@ jobs:
           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 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