Skip to content

feat: Tarball caching in GitHub Actions#152

Open
SnO2WMaN wants to merge 8 commits intoleanprover:mainfrom
SnO2WMaN:tarball-caching
Open

feat: Tarball caching in GitHub Actions#152
SnO2WMaN wants to merge 8 commits intoleanprover:mainfrom
SnO2WMaN:tarball-caching

Conversation

@SnO2WMaN
Copy link

@SnO2WMaN SnO2WMaN commented Feb 16, 2026

Full .lake caching is very heavy (in FFL/Foundation, it costed 2GB each cache, see cslib's Caches). I changed caching strategy only caching tarball by creating lake pack.

See

IMPORTANT: I didn't tested it on macos-latest and windows-latest, so name of generating tarball might be wrong on these environment. please check get_gh_tarball_cache_path.sh.

@SnO2WMaN SnO2WMaN changed the title feat: Tarball caching feat: Tarball caching in GitHub Actions Feb 16, 2026
@SnO2WMaN SnO2WMaN marked this pull request as draft February 16, 2026 20:43
@SnO2WMaN SnO2WMaN marked this pull request as ready for review February 16, 2026 20:44
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'
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I noticed that cache-hit is only true when cache is hit by exact key, not restore-keys. we trigger this job when tarball exists.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant