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