ltar contents + cache

Stream: lean4

[Julian Berman]

I'm on some custom compiled lean setup and trying to figure out why lake is unhappy with the downloaded cache -- i.e. I run lake exe cache get but lake build still does a full build of Mathlib4 and ignores what it downloaded. As far as I know, I'm on the exact commit that corresponds to the nightly in Mathlib4's lean-toolchain (i.e. right now 2023-07-30) -- how do I understand what's in an .ltar file and/or what else needs to match for lean to want to use the files that are downloaded by cache get?

[Mac Malone]

@Julian Berman afaik, custom built Lean is always considered different from a release Lean because built Lean has an empty Lean.githash.

[Julian Berman]

Aha... ok, fair enough, thanks.