Commit 2023-09-15 00:38 9db9cbb1

feat: add git origin info to cache .ltar files (#7143) This should have no user-visible effects, but from here on .ltar files in the cache will contain the commit from which they were generated. Because of the way cache works, when you download the cache for a commit you might be using files built from several different commits, because later commits only invalidated some files and the old files are still good. If an .ltar file turns out to be bad (e.g. has a surprising .trace and is causing lake build to ignore it), this is helpful information for debugging, and it's only a few extra bytes in the file. The new version of leantar has a new function: leantar -k 1234.ltar will print out the "comments" in the file. If it is a file generated by an old version of leantar it will be empty, but files generated subsequent to this commit will show something along the lines git=mathlib4@12de34 containing the commit sha for the run that generated this ltar file.