Caching Tarball by `lake pack`

Stream: general

[SnO2WMaN]

Recently I changed caching strategy in FFL/Foundation. do not cache whole .lake/, cache tarball generated by lake pack (see). Previously, whole .lake caching costs 2GB each time, and currently tarball caching, it costs 200MB, it times 10 times smaller size and effectively afford to cache on GitHub Cache by 10GB limitation.

Now no problem seems to be here in FFL/Foundation. How about this idea? Seems same problem holds on projects using lean-action, like cslib, (see current cslib's GH cache page) I opened PR for lean-action (https://github.com/leanprover/lean-action/pull/152).

[SnO2WMaN]

Very large size cache issue might be related to whole commit logs of mathlib. I'll be working on the issue: https://github.com/leanprover/lean4/issues/10603