From dd82de121caa1f4b92df70ad54327f825f1d967b Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Thu, 1 Oct 2026 13:31:22 -0400
Subject: [PATCH] fix: cache test and lint build artifacts

This PR saves the GitHub cache after testing and linting so their build artifacts can be reused, while preserving separate build, test, and lint reporting. It retains caching after test or lint failures and skips saves on exact cache hits.

Based on [Chris's suggestion](https://github.com/leanprover/cslib/pull/1015#issuecomment-5935191124).

Codex assisted with implementation and validation.
---
 CHANGELOG.md |  4 ++++
 README.md    |  3 +++
 action.yml   | 18 ++++++++++++------
 3 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c85943..eb1cdbf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Fixed
+
+- save the GitHub cache after testing and linting so their build artifacts can be reused, preserving caching after test or lint failures and skipping saves on an exact cache hit
+
 ## v1.6.1 - 2026-10-02
 
 ### Changed
diff --git a/README.md b/README.md
index 9f6004f..add0c4e 100644
--- a/README.md
+++ b/README.md
@@ -33,6 +33,9 @@ however if you encounter an issue when using a different runner, please still op
 
 ## Caching `.lake` directory with GitHub's `actions\cache`
 By default, `lean-action` uses [`actions\cache`](https://github.com/actions/cache) to cache the `.lake` directory and speed up builds.
+The cache is saved after building, testing, and linting, so it includes artifacts produced by all three steps.
+A test or lint failure still allows completed build artifacts to be cached; setup or build failures do not.
+Saving is skipped when the exact cache key was restored.
 
 > [!NOTE]
 GitHub caching is distinct from Mathlib caching with `lake exe cache get`
diff --git a/action.yml b/action.yml
index b0bc7ed..8ebeca1 100644
--- a/action.yml
+++ b/action.yml
@@ -261,6 +261,7 @@ runs:
       working-directory: ${{ inputs.lake-package-directory }}
 
     - uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5
+      id: cache-restore
       if: ${{ inputs.use-github-cache == 'true' }}
       with:
         path: ${{ inputs.lake-package-directory }}/.lake
@@ -302,12 +303,6 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
-    - uses: actions/cache/save@caa296126883cff596d87d8935842f9db880ef25 # v5
-      if: ${{ inputs.use-github-cache == 'true' }}
-      with:
-        path: ${{ inputs.lake-package-directory }}/.lake
-        key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
-
     - name: test ${{ github.repository }}
       id: test
       if: ${{ steps.config.outputs.run-lake-test == 'true'}}
@@ -331,6 +326,17 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - uses: actions/cache/save@caa296126883cff596d87d8935842f9db880ef25 # v5
+      # Keep successful build artifacts even when tests or linting fail.
+      # Failures before those steps must still prevent saving the cache.
+      if: >-
+        ${{ !cancelled() && inputs.use-github-cache == 'true' &&
+            steps.cache-restore.outputs.cache-hit != 'true' &&
+            (success() || steps.test.outcome == 'failure' || steps.lint.outcome == 'failure') }}
+      with:
+        path: ${{ inputs.lake-package-directory }}/.lake
+        key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }}
+
     - name: check reservoir eligibility
       if: ${{ inputs.check-reservoir-eligibility == 'true' }}
       # Passes in the private status, number of stars, and license id of the repository to check_reservoir_eligibility.sh script