Closed balacij closed 9 months ago
It seems that GitHub doesn't overwrite caches if hits occurred. On my fork, this wasn't an issue (because I have no caches!), but on this repo, we probably should have evicted all caches before merging this in. My bad!
Contributes to #375
cabal
cache. It looks like @JasonGross had the right idea.I don't think this PR closes #375 because it doesn't have an Agda build cache, so building
agda-categories
is still completely fresh for each CI run, so we can have a look at that too.To audit this solution, please have a look at my fork's CI runs, specifically the earliest 2's build times and logs. The first one is a completely fresh run without a cache, and the second one has a cache. There's a ~20min time cut with the cache hit, but I would hope that it can be brought down further by adding the Agda build cache to the CI cache too.