ci: Revert cache get default behavior for skip-proofwidgets (leanprover-community#35542)

For backwards compatibility, as downstream projects depend on this tool

Author: marcelolynch

.github/workflows/build_template.yml

@@ -323,7 +323,7 @@ jobs:
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -343,10 +343,10 @@ jobs:
           if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
             echo "Fetching all remaining cache..."
 
-            ../tools-branch/.lake/build/bin/cache get
+            ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
 
             # Run again with --repo, to ensure we actually get the oleans.
-            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
+            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --skip-proofwidgets get
           else
             echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
             echo "No cache for 'Mathlib.Init' available or it could not be prepared."
@@ -413,8 +413,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../tools-branch/.lake/build/bin/cache get Archive.lean
-          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
 
       - name: build archive
         id: archive
@@ -708,16 +708,16 @@ jobs:
       - name: get cache for Mathlib
         run: |
           # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
-          lake exe cache --include-proofwidgets get
+          lake exe cache get
           # Run again with --repo, so ensure we actually get the oleans.
-          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --include-proofwidgets get
+          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
 
       - name: get cache for Archive and Counterexamples
         run: |
           # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
-          lake exe cache --include-proofwidgets get Archive Counterexamples
+          lake exe cache get Archive Counterexamples
           # Run again with --repo, so ensure we actually get the oleans.
-          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --include-proofwidgets get Archive Counterexamples
+          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples
 
       - name: verify that everything was available in the cache
         run: |

Cache/Main.lean

@@ -39,7 +39,7 @@ Commands:
 Options:
   --repo=OWNER/REPO  Override the repository to fetch/push cache from
   --staging-dir=<output-directory> Required for 'stage', 'stage!', 'unstage' and 'put-staged': staging directory.
-  --include-proofwidgets  Include fetching/building ProofWidgets release assets during 'get'
+  --skip-proofwidgets  Skip fetching/building ProofWidgets release assets during 'get'
 
 * Linked files refer to local cache files with corresponding Lean sources
 * Commands ending with '!' should be used manually, when hot-fixes are needed
@@ -101,9 +101,7 @@ def main (args : List String) : IO Unit := do
   -- parse relevant options, ignore the rest
   let repo? ← parseNamedOpt "repo" options
   let stagingDir? ← parseNamedOpt "staging-dir" options
-  let includeProofWidgets := parseFlagOpt "include-proofwidgets" options
-  let inGitHubActions := (← IO.getEnv "GITHUB_ACTIONS") == some "true"
-  let skipProofWidgets := inGitHubActions && !includeProofWidgets
+  let skipProofWidgets := parseFlagOpt "skip-proofwidgets" options
 
   let mut roots : Std.HashMap Lean.Name FilePath ← parseArgs args
   if roots.isEmpty then do