feat(Cache): make use of Lake artifact cache

[tydeu]

This PR extends Mathlib's cache to enable packing and unpacking files to/from the machine-local Lake artifact cache.

In the new caching strategy, a module's artifacts are stored differently in the leantar archives and thus the new archives are incompatible with setups without the local Lake cache. The archive packs the trace file from the build directory and the artifacts from the local Lake cache. When unpacked, they will also be restored to local Lake cache.

With the new setup, after fetching the cache once for a version of Mathlib, the built modules will be available to all instances o Mathlib on the system which are on the same version or have the same version of those modules. Furthermore, Lake passes these modules to Lean directly from the cache, avoiding the need for multiple copies of the same module artifacts.

---

[kim-em]

@tydeu

Just recording this for later, but here's what Claude identified as possibly problematic in Mathlib:

Location	Severity	Issue
scripts/bench/size/run:31	Will break	Glob .lake/build/**/*.olean finds nothing
build_template.yml:369	Will break	du .lake/build/lib/lean/Mathlib reports nothing
build_template.yml:297	Harmless no-op	rm -rf on now-empty directory
build_template.yml:24-30	Needs update	LAKE_NO_CACHE comment/setting is stale
Cache/README.md:243-244	Docs wrong	File locations table
ImportGraph/Meta.lean:168	Low risk	Assumes searchPath.findWithExt "olean" will work