Commit 2023-12-11 07:34 1ec84029

feat: lake exe cache lookup (#8838) This allows you to query information regarding the cache:

$ lake exe cache lookup Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean: /home/mario/.cache/mathlib/0875116721fafda8.ltar
  comment: git=mathlib4@a4d9e50aa274cb8057bf09c845de139ccd4b0164

This says, for a given lean file, where to find the ltar file that it is unpacked from/to, as well as the metadata contained in the file, which currently means the commit which built the file. (This is not necessarily the same as the current commit, because not every commit builds all files, many files are grandfathered from earlier commits, sometimes even builds that failed, like in this example.) This is useful for debugging certain issues. The leantar version was bumped from 0.1.9 to 0.1.10, mainly because this includes a bugfix for the -k option of leantar that was exposed while testing this command.