feat: Tarball caching in GitHub Actions

.editorconfig

@@ -0,0 +1,13 @@
+root = true
+
+[*]
+indent_style = space
+indent_size = 2
+end_of_line = lf
+charset = utf-8
+trim_trailing_whitespace = true
+insert_final_newline = true
+
+[*.{yml,yaml}]
+indent_style = space
+indent_size = 2

action.yml

@@ -1,6 +1,6 @@
 name: "Lean Action - CI for Lean Projects"
 description: |
-  Standard CI for Lean projects. 
+  Standard CI for Lean projects.
   Steps:
     - install elan
     - get Mathlib cache (optional, must be downstream of Mathlib)
@@ -133,7 +133,7 @@ outputs:
 
 runs:
   using: "composite"
-  steps: 
+  steps:
     - name: install elan
       run: |
         : Install Elan
@@ -174,15 +174,6 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
-    - uses: actions/cache/restore@v4
-      if: ${{ inputs.use-github-cache == 'true' }}
-      with:
-        path: ${{ inputs.lake-package-directory }}/.lake
-        # cache key includes the operating system, the architecture (X86, X64, ARM, ARM64), the Lake manifest, and the git commit hash
-        key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-        # if no cache hit, fall back to the cache from previous commit
-        restore-keys: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
-
     - name: detect mathlib
       # only detect Mathlib if the user did not provide the mathlib-cache input
       if: ${{ inputs.use-mathlib-cache == 'auto' }}
@@ -205,22 +196,48 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - name: get tarball path for github cache
+      if: ${{ inputs.use-github-cache == 'true' }}
+      id: get-gh-tarball-cache-path
+      run: |
+        : Get GitHub Cache Tarball Path
+        ${GITHUB_ACTION_PATH}/scripts/get_gh_tarball_cache_path.sh
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
+    - name: restore tarball from github cache
+      id: github-cache-restore
+      uses: actions/cache/restore@v4
+      if: ${{ inputs.use-github-cache == 'true' }}
+      with:
+        path: ${{ inputs.lake-package-directory }}/.lake/${{ steps.get-gh-tarball-cache-path.outputs.tarball-file }}
+        key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        restore-keys: |
+          lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+    - name: unpack tarball from github cache
+      if: steps.github-cache-restore.outputs.cache-hit == 'true'
+      shell: bash
+      run: lake unpack
+
     - name: build ${{ github.repository }}
       id: build
       if: ${{ steps.config.outputs.run-lake-build == 'true'}}
-      env: 
-          BUILD_ARGS: ${{ inputs.build-args }}
+      env:
+        BUILD_ARGS: ${{ inputs.build-args }}
       run: |
         : Lake Build
         ${GITHUB_ACTION_PATH}/scripts/lake_build.sh
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - name: save tarball to github cache
+      if: ${{ inputs.use-github-cache == 'true' }}
+      shell: bash
+      run: lake pack
     - uses: actions/cache/save@v4
       if: ${{ inputs.use-github-cache == 'true' }}
       with:
-        path: ${{ inputs.lake-package-directory }}/.lake
-        key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        path: ${{ inputs.lake-package-directory }}/.lake/${{ steps.get-gh-tarball-cache-path.outputs.tarball-file }}
+        key: ${{ steps.github-cache-restore.outputs.cache-primary-key }}
 
     - name: test ${{ github.repository }}
       id: test

scripts/get_gh_tarball_cache_path.sh

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+echo "::group::Get GitHub cache tarball path"
+
+if [ -f lake-manifest.json ]; then
+  PROJECT_NAME=$(jq -r .name lake-manifest.json)
+  TARBALL_FILE="$PROJECT_NAME-x86_64-unknown-linux-gnu.tar.gz"
+
+  echo "Tarball file name: $TARBALL_FILE"
+  echo "tarball-file=$TARBALL_FILE" >> $GITHUB_OUTPUT
+else
+  echo "::error::No lake-manifest.json found. Run lake update to generate manifest"
+  echo "::error::Exiting with status 1"
+  exit 1
+fi