You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
One area for improvement is that currently the action caches the mathlib cache generated by lake exe cache get which seems redundant and takes up significant space in the GitHub cache.
One potential fix for this would be to exclude certain subfolders of .lake from the cache. This behavior of the cache action may be relevant.
The text was updated successfully, but these errors were encountered:
Did you figure out what is happening with the github cache?
In use on my projects I don't find that it increases the speed of successive runs, I think github cache is never actually used. As yet I didn't investigate what was happening since possibly someone else already knows the solution.
One area for improvement is that currently the action caches the mathlib cache generated by
lake exe cache get
which seems redundant and takes up significant space in the GitHub cache.One potential fix for this would be to exclude certain subfolders of .lake from the cache. This behavior of the cache action may be relevant.
The text was updated successfully, but these errors were encountered: