For this PR to be merged in, you will first need to manually evict all caches, so that merging this can create a fresh cache for subsequent PRs. GitHub Actions doesn't seem to overwrite caches as often as one would like!
I'd call this PR "experimental" because it involves reusing agda build caches for subsequent PRs. I've tested it with 1 comments-level change (locally, not easy to show on GitHub) and 1 code-level change to make sure that subsequent PRs aren't infected by a "good, working build" of agda-categories.
I have no idea if cross-repo PRs are able to use caches, so this is a bit of a live test This PR changes the paths designated in the actions/cache use, so it doesn't/won't hit the cache. :smile:
This PR adds reusable build caching for agda-stdlib and agda-categories by adding their respective agda-produced _build/ folders to the GH Cache. In my testing, it reduces build times for no-diff changes to 2min (which really should be reducible to 0min if there are no changes...) by simply not having to recompile any Agda code. For other changes, the normal recompilation is done as needed (aside: I edited Categories.Adjoint.Equivalence, which I assume is seemingly depended on by many modules, so the build time is >2min && <20min).
Notes:
agda-categories.I have no idea if cross-repo PRs are able to use caches, so this is a bit of a live testThis PR changes the paths designated in the actions/cache use, so it doesn't/won't hit the cache. :smile:This PR adds reusable build caching for
agda-stdlibandagda-categoriesby adding their respective agda-produced_build/folders to the GH Cache. In my testing, it reduces build times for no-diff changes to 2min (which really should be reducible to 0min if there are no changes...) by simply not having to recompile any Agda code. For other changes, the normal recompilation is done as needed (aside: I editedCategories.Adjoint.Equivalence, which I assume is seemingly depended on by many modules, so the build time is >2min && <20min).