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