Comments (5)
Maybe the cache key should be like this, specifying lean-toolchain
and lake-manifest.json
key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }}
restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }}
from lean-action.
Thank you @SnO2WMaN for raising this issue and coming up with suggestions for improved caching keys! #71 implements these changes.
from lean-action.
duplicate of #62
from lean-action.
Even though the failure is the same as #62, I think the suggestion to improve the key for the caching is still valid.
Maybe the cache key should be like this, specifying
lean-toolchain
andlake-manifest.json
key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }} restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }}
I think this is an improvement over the existing key
input for the cache
However, it seems to me that the restore-keys
need to be a prefix match of whatever existing cache key is hit. If you have the same value for the key
and restore-key
input it seems redundant, although I could be missing something here.
For the restore-key
input what about:
restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
With this lean-action
can restore caches where lean-toolchain
and lake-manifest.json
remain unchanged.
@SnO2WMaN what do you think?
Also for reference, the initial discussion of what key to use for the hash was here.
from lean-action.
Thanks for your advice.
Once considered, we added ${{ github.ref }}
to prevent build errors caused by cache from different Lean versions, but now we have switch to use lean-toolchain
. It might no longer necessary so we might be able to remove ${{ github.ref }}
from both the key
and restore-key
.
from lean-action.
Related Issues (20)
- Support repositories with subdirectory Lean packages
- v1-beta release HOT 1
- Add an option to disable GitHub caching
- Mathlib detection prints unnecessary error when lakefile.toml not present
- Update the lint step to use the more flexible `lake lint`
- Automatically check if test runner is available HOT 18
- Leverage output parameters for `lake build` and `lake test` steps to to verify the expected steps ran during a test
- Leverage Lake's API to determine if a package is downstream of Mathlib
- build args default should be 'quiet' HOT 2
- Create `auto-config` input HOT 1
- bug: run `lake update` and `lean-action` gets an error HOT 18
- Parameterize functional tests by lean version.
- Save cache even if a build fails
- v1-beta.1 release HOT 2
- Update `RELEASING.md` based on improvements to release process
- Fix GitHub cache keys to reduce problems with the cache when updating Lean version
- (DRAFT RFC) Add support for building leanblueprint to lean-action
- install elan on windows HOT 2
- v1.0.0 release HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from lean-action.