ci: Change cache strategy

.github/workflows/ci.yml

@@ -5,10 +5,17 @@ on:
     branches:
       - main
   pull_request:
-  merge_group:
+    branches:
+      - main
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
 
 permissions:
   contents: read
+  pages: write
+  id-token: write
 
 jobs:
   build:
@@ -20,17 +27,22 @@ jobs:
         run: |
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      # Restore project cache
+      - name: Get Mathlib cache
+        run: lake exe cache get
       - name: Restore cache
         id: cache-restore
         uses: actions/cache/restore@v5
         with:
-          path: .lake
-          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          path: .lake/Catalogue-x86_64-unknown-linux-gnu.tar.gz
+          # NOTE: including github branch name and SHA for avoding cache key reserving problem
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}-${{ github.sha }}
           restore-keys: |
+            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}
             lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-      - name: Get Mathlib cache
-        if: steps.cache-restore.outputs.cache-hit != 'true'
-        run: lake exe cache get
+      - name: Unpack project cache
+        if: hashFiles('.lake/Catalogue-x86_64-unknown-linux-gnu.tar.gz') != ''
+        run: lake unpack
 
       # Build Catalogue
       - name: Download JuliaMono
@@ -44,11 +56,14 @@ jobs:
       - name: Build Catalogue
         run: lake exe catalogue
 
+      - name: Pack project cache
+        run: lake pack
       - name: Save project cache
         if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
+        id: cache-save
         uses: actions/cache/save@v5
         with:
-          path: .lake
+          path: .lake/Catalogue-x86_64-unknown-linux-gnu.tar.gz
           key: ${{ steps.cache-restore.outputs.cache-primary-key }}
 
       # Upload pages artifact

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "3f0a7510645c5562a1341aef0e631bd3db17c658",
+   "rev": "e2ecd0d283f5724c04e24e1249a9e2aae4cf5b61",
    "name": "Foundation",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "05bb84181739ecc0897184a3e2906241267bcdfd",
+   "rev": "7be6082d00bb0cfc1e136505dba7718cd5fcaa84",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f317236f66fce00be8a8e0f01cdd31619909f887",
+   "rev": "58d8468384df017604272605bb0ec709826199e7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f317236f66fce00be8a8e0f01cdd31619909f887",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba",
+   "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9",
+   "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,17 +125,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -145,7 +145,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -155,7 +155,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01aa23996c2e12e81e33f81b1a7f65305519331d",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.28.0-rc1