Skip to content

Commit

Permalink
feat(Cache): add success message to lake exe cache get (#13395)
Browse files Browse the repository at this point in the history
closes #13276 


Co-authored-by: Rida Hamadani <[email protected]>
Co-authored-by: Michael Rothgang <[email protected]>
  • Loading branch information
3 people committed Jun 1, 2024
1 parent fda847e commit de56413
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 2 deletions.
3 changes: 2 additions & 1 deletion Cache/IO.lean
Original file line number Diff line number Diff line change
Expand Up @@ -367,7 +367,8 @@ def unpackCache (hashMap : HashMap) (force : Bool) : CacheM Unit := do
stdin.putStr <| Lean.Json.compress <| .arr config
let exitCode ← child.wait
if exitCode != 0 then throw <| IO.userError s!"leantar failed with error code {exitCode}"
IO.println s!"unpacked in {(← IO.monoMsNow) - now} ms"
IO.println s!"Unpacked in {(← IO.monoMsNow) - now} ms"
IO.println "Completed successfully!"
else IO.println "No cache files to decompress"

instance : Ord FilePath where
Expand Down
7 changes: 6 additions & 1 deletion Cache/Requests.lean
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,8 @@ def downloadFile (hash : UInt64) : IO Bool := do
IO.FS.removeFile partPath
pure false

/-- Calls `curl` to download files from the server to `CACHEDIR` (`.cache`) -/
/-- Call `curl` to download files from the server to `CACHEDIR` (`.cache`).
Exit the process with exit code 1 if any files failed to download. -/
def downloadFiles (hashMap : IO.HashMap) (forceDownload : Bool) (parallel : Bool) : IO Unit := do
let hashMap ← if forceDownload then pure hashMap else hashMap.filterExists false
let size := hashMap.size
Expand Down Expand Up @@ -139,6 +140,8 @@ def downloadFiles (hashMap : IO.HashMap) (forceDownload : Bool) (parallel : Bool
IO.Process.exit 1
else IO.println "No files to download"

/-- Check if the project's `lean-toolchain` file matches mathlib's.
Print and error and exit the process with error code 1 otherwise. -/
def checkForToolchainMismatch : IO.CacheM Unit := do
let mathlibToolchainFile := (← IO.mathlibDepPath) / "lean-toolchain"
let downstreamToolchain ← IO.FS.readFile "lean-toolchain"
Expand Down Expand Up @@ -166,6 +169,8 @@ def getFiles (hashMap : IO.HashMap) (forceDownload forceUnpack parallel decompre
downloadFiles hashMap forceDownload parallel
if decompress then
IO.unpackCache hashMap forceUnpack
else
IO.println "Downloaded all files successfully!"

end Get

Expand Down

0 comments on commit de56413

Please sign in to comment.