From de5641307008d5b7008c3eac51a5130f1c9acbe0 Mon Sep 17 00:00:00 2001 From: Rida Hamadani Date: Sat, 1 Jun 2024 12:34:26 +0000 Subject: [PATCH] feat(Cache): add success message to `lake exe cache get` (#13395) closes #13276 Co-authored-by: Rida Hamadani <106540880+Rida-Hamadani@users.noreply.github.com> Co-authored-by: Michael Rothgang --- Cache/IO.lean | 3 ++- Cache/Requests.lean | 7 ++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/Cache/IO.lean b/Cache/IO.lean index 1dcf6db24b7dd..f7bd11c8c0001 100644 --- a/Cache/IO.lean +++ b/Cache/IO.lean @@ -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 diff --git a/Cache/Requests.lean b/Cache/Requests.lean index 27549970d4715..3e022f97e0853 100644 --- a/Cache/Requests.lean +++ b/Cache/Requests.lean @@ -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 @@ -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" @@ -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