chore: CI: verify lake cache step (#13735)

This PR adds a CI step to the build job which verifies that the uploaded
Lake cache can be downloaded and used without issue.

.github/workflows/build-template.yml

@@ -195,7 +195,8 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Lake Cache
+      - id: upload-lake-cache
+        name: Upload Lake Cache
         # Caching on cancellation created some mysterious issues perhaps related to improper build
         # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
         if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
@@ -210,6 +211,20 @@ jobs:
           LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
         timeout-minutes: 20 # prevent excessive hanging from network issues
         continue-on-error: true
+      - name: Verify Lake Cache
+        if: steps.upload-lake-cache.outcome == 'success'
+        run: |
+          mv build/stage1/lib/lean build/stage1/lib/lean.bak
+          cd src
+          ../build/stage0/bin/lake cache clean
+          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
+          ../build/stage0/bin/lake build --no-build
+        continue-on-error: true
+      - name: Restore Build
+        if: steps.upload-lake-cache.outcome == 'success'
+        run: |
+          rm -rf build/stage1/lib/lean
+          mv build/stage1/lib/lean.bak build/stage1/lib/lean
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install