Coarseness of Mathlib.Cache

Stream: mathlib4

[Wojciech Nawrocki]

I was very confused why in my usage, lake exe cache get almost never works. I am realizing now that it is because the hashing is quite coarse. In particular, the hash of every Lean file mixes in the "root hash" which is a mix of lakefile.lean/lake-manifest.json/lean-toolchain. So if I change something unrelated, e.g. the version of docgen I depend on in lake-manifest.json, the entire cache gets invalidated. Lake traces are much better at this; even if I change some pinned versions of the manifest, if those don't end up in the build dependencies of a module, the Lake trace of that module remains the same. Is there a reason why Mathlib.Cache doesn't use Lake traces?

[Arthur Paulino]

The computation of Lake traces is tied to the building routine, but if we build in order to know the traces we no longer need cached files. So cache should be totally able to reuse Lake traces, but that would require a refactor of Lake itself.

Note: if we ever want to reuse Lake implementations, we'd need to add Lake as a dependency in Mathlib's lakefile. Not a prohibitive thing, but Mathlib maintainers will need to chime in for this decision

[Wojciech Nawrocki]

Gotcha. It sounds like either a parse-only (but don't build) trace generation routine could be exposed by Lake as a library, or Cache could become part of Lake. The latter option would certainly benefit non-mathlib projects. Lake already has its cloud build support, but I am understanding that it was insufficient in some respects for mathlib.

[Wojciech Nawrocki]

(Short of integrating with Lake, though, Mathlib.Cache could also attempt finer trace generation that looks at import statements beyond those just in Mathlib.)