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.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: digama0

Cache/IO.lean

@@ -69,7 +69,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.5"
+  "0.1.7"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -242,23 +242,24 @@ def mkDir (path : FilePath) : IO Unit := do
 Given a path to a Lean file, concatenates the paths to its build files.
 Each build file also has a `Bool` indicating whether that file is required for caching to proceed.
 -/
-def mkBuildPaths (path : FilePath) : IO $ Array (FilePath × Bool) := do
+def mkBuildPaths (path : FilePath) : IO $ List (FilePath × Bool) := do
   let packageDir ← getPackageDir path
-  return #[
+  return [
     (packageDir / LIBDIR / path.withExtension "trace", true),
     (packageDir / LIBDIR / path.withExtension "olean", true),
     (packageDir / LIBDIR / path.withExtension "ilean", true),
     (packageDir / IRDIR  / path.withExtension "c", true),
     (packageDir / LIBDIR / path.withExtension "extra", false)]
 
 /-- Check that all required build files exist. -/
-def allExist (paths : Array (FilePath × Bool)) : IO Bool := do
+def allExist (paths : List (FilePath × Bool)) : IO Bool := do
   for (path, required) in paths do
     if required then if !(← path.pathExists) then return false
   pure true
 
 /-- Compresses build files into the local cache and returns an array with the compressed files -/
-def packCache (hashMap : HashMap) (overwrite : Bool) : IO $ Array String := do
+def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String := none) :
+    IO $ Array String := do
   mkDir CACHEDIR
   IO.println "Compressing cache"
   let mut acc := #[]
@@ -270,8 +271,10 @@ def packCache (hashMap : HashMap) (overwrite : Bool) : IO $ Array String := do
     if ← allExist buildPaths then
       if overwrite || !(← zipPath.pathExists) then
         tasks := tasks.push <| ← IO.asTask do
-          runCmd (← getLeanTar) $ #[zipPath.toString] ++
-            ((← buildPaths.filterM (·.1.pathExists)) |>.map (·.1.toString))
+          let trace :: args := (← buildPaths.filterM (·.1.pathExists)) |>.map (·.1.toString)
+            | unreachable!
+          runCmd (← getLeanTar) $ #[zipPath.toString, trace] ++
+            (if let some c := comment then #["-c", s!"git=mathlib4@{c}"] else #[]) ++ args
       acc := acc.push zip
   for task in tasks do
     _ ← IO.ofExcept task.get

Cache/Main.lean

@@ -82,16 +82,16 @@ def main (args : List String) : IO Unit := do
     getFiles (← hashMemo.filterByFilePaths (toPaths args)) true true goodCurl true
   | "get-" :: args =>
     getFiles (← hashMemo.filterByFilePaths (toPaths args)) false false goodCurl false
-  | ["pack"] => discard $ packCache hashMap false
-  | ["pack!"] => discard $ packCache hashMap true
+  | ["pack"] => discard $ packCache hashMap false (← getGitCommitHash)
+  | ["pack!"] => discard $ packCache hashMap true (← getGitCommitHash)
   | ["unpack"] => unpackCache hashMap false
   | ["unpack!"] => unpackCache hashMap true
   | ["clean"] =>
     cleanCache $ hashMap.fold (fun acc _ hash => acc.insert $ CACHEDIR / hash.asLTar) .empty
   | ["clean!"] => cleanCache
   -- We allow arguments for `put` and `put!` so they can be added to the `roots`.
-  | "put" :: _ => putFiles (← packCache hashMap false) false (← getToken)
-  | "put!" :: _ => putFiles (← packCache hashMap false) true (← getToken)
+  | "put" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) false (← getToken)
+  | "put!" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) true (← getToken)
   | ["commit"] =>
     if !(← isGitStatusClean) then IO.println "Please commit your changes first" return else
     commit hashMap false (← getToken)

Cache/Requests.lean

@@ -168,11 +168,7 @@ section Commit
 def isGitStatusClean : IO Bool :=
   return (← IO.runCmd "git" #["status", "--porcelain"]).isEmpty
 
-def getGitCommitHash : IO String := do
-  let ret := (← IO.runCmd "git" #["log", "-1"]).replace "\n" " "
-  match ret.splitOn " " with
-  | "commit" :: hash :: _ => return hash
-  | _ => throw $ IO.userError "Invalid format for the return of `git log -1`"
+def getGitCommitHash : IO String := return (← IO.runCmd "git" #["rev-parse", "HEAD"]).trimRight
 
 /--
 Sends a commit file to the server, containing the hashes of the respective committed files.