feat: add 'cache get-' flag that does not decompress (leanprover-community#3179)

Perhaps a big obscure for end-users, but useful if you would like to make sure something is in the cache, for later.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Cache/Main.lean

@@ -13,6 +13,7 @@ Commands:
   # No priviledge required
   get  [ARGS]  Download linked files missing on the local cache and decompress
   get! [ARGS]  Download all linked files and decompress
+  get- [ARGS]  Download linked files missing to the local cache, but do no compress
   pack         Compress non-compressed build files into the local cache
   pack!        Compress build files into the local cache (no skipping)
   unpack       Decompress linked already downloaded files
@@ -50,18 +51,20 @@ def toPaths (args : List String) : List FilePath :=
   args.map (FilePath.mk · |>.normalize)
 
 def curlArgs : List String :=
-  ["get", "get!", "put", "put!", "commit", "commit!"]
+  ["get", "get!", "get-", "put", "put!", "commit", "commit!"]
 
 open Cache IO Hashing Requests in
 def main (args : List String) : IO Unit := do
   let hashMemo ← getHashMemo
   let hashMap := hashMemo.hashMap
   let goodCurl := !(curlArgs.contains (args.headD "") && !(← validateCurl))
   match args with
-  | ["get"] => getFiles hashMap false goodCurl
-  | ["get!"] => getFiles hashMap true goodCurl
-  | "get"  :: args => getFiles (← hashMemo.filterByFilePaths (toPaths args)) false goodCurl
-  | "get!" :: args => getFiles (← hashMemo.filterByFilePaths (toPaths args)) true goodCurl
+  | ["get"] => getFiles hashMap false goodCurl true
+  | ["get!"] => getFiles hashMap true goodCurl true
+  | ["get-"] => getFiles hashMap false goodCurl false
+  | "get"  :: args => getFiles (← hashMemo.filterByFilePaths (toPaths args)) false goodCurl true
+  | "get!" :: args => getFiles (← hashMemo.filterByFilePaths (toPaths args)) true goodCurl true
+  | "get-"  :: args => getFiles (← hashMemo.filterByFilePaths (toPaths args)) false goodCurl false
   | ["pack"] => discard $ packCache hashMap false
   | ["pack!"] => discard $ packCache hashMap true
   | ["unpack"] => unpackCache hashMap

Cache/Requests.lean

@@ -81,9 +81,11 @@ def downloadFiles (hashMap : IO.HashMap) (forceDownload : Bool) (parallel : Bool
   else IO.println "No files to download"
 
 /-- Downloads missing files, and unpacks files. -/
-def getFiles (hashMap : IO.HashMap) (forceDownload : Bool) (parallel : Bool) : IO Unit := do
+def getFiles (hashMap : IO.HashMap) (forceDownload : Bool) (parallel : Bool) (decompress : Bool) :
+    IO Unit := do
   downloadFiles hashMap forceDownload parallel
-  IO.unpackCache hashMap
+  if decompress then
+    IO.unpackCache hashMap
 
 end Get