feat: --keep-local

Author: tydeu

src/lake/Lake/CLI/Main.lean

@@ -65,6 +65,7 @@ public structure LakeOptions where
   outFormat : OutFormat := .text
   offline : Bool := false
   outputsFile? : Option FilePath := none
+  overwriteInputs : Bool := true
   forceDownload : Bool := false
   mappingsOnly : Bool := false
   service? : Option String := none
@@ -285,6 +286,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--offline"     => modifyThe LakeOptions ({· with offline := true})
 | "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
 | "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
+| "--keep-local"  => modifyThe LakeOptions ({· with overwriteInputs := false})
 | "--force-download" => modifyThe LakeOptions ({· with forceDownload := true})
 | "--download-arts" => modifyThe LakeOptions ({· with mappingsOnly := false})
 | "--mappings-only" => modifyThe LakeOptions ({· with mappingsOnly := true})
@@ -485,7 +487,7 @@ protected def get : CliM PUnit := do
       else
         return ws.defaultCacheService
     let map ← CacheMap.load file
-    cache.writeMap ws.root.cacheScope map service.name? (some remoteScope)
+    cache.writeMap ws.root.cacheScope map service.name? (some remoteScope) opts.overwriteInputs
     let descrs ← map.collectOutputDescrs
     service.downloadArtifacts descrs cache remoteScope opts.forceDownload
   else
@@ -530,7 +532,7 @@ protected def get : CliM PUnit := do
           return map
         else
           findOutputs cache service pkg remoteScope opts platform toolchain
-      cache.writeMap pkg.cacheScope map service.name? (some remoteScope)
+      cache.writeMap pkg.cacheScope map service.name? (some remoteScope) opts.overwriteInputs
       unless opts.mappingsOnly do
         let descrs ← map.collectOutputDescrs
         service.downloadArtifacts descrs cache remoteScope opts.forceDownload
@@ -544,7 +546,7 @@ protected def get : CliM PUnit := do
         let toolchain := cacheToolchain pkg toolchain
         try
           let map ← findOutputs cache service pkg remoteScope opts platform toolchain
-          cache.writeMap pkg.cacheScope map service.name? (some remoteScope)
+          cache.writeMap pkg.cacheScope map service.name? (some remoteScope) opts.overwriteInputs
           unless opts.mappingsOnly do
             let descrs ← map.collectOutputDescrs
             service.downloadArtifacts descrs cache remoteScope opts.forceDownload
@@ -677,7 +679,7 @@ protected def add : CliM PUnit := do
       error (serviceNotFound service ws.lakeConfig.config.cache.services)
     return some (.ofString service)
   let map ← CacheMap.load file
-  ws.lakeCache.writeMap localScope map service? opts.scope?
+  ws.lakeCache.writeMap localScope map service? opts.scope? opts.overwriteInputs
 
 private def stagingOutputsFile := "outputs.jsonl"
 
@@ -754,7 +756,7 @@ protected def unstage : CliM PUnit := do
   unless ok do
     logError "failed to copy all outputs to the staging directory"
     exit 1
-  ws.lakeCache.writeMap localScope map service? opts.scope?
+  ws.lakeCache.writeMap localScope map service? opts.scope? opts.overwriteInputs
 
 protected def putStaged : CliM PUnit := do
   processOptions lakeOption

src/lake/Lake/Config/Cache.lean

@@ -434,22 +434,28 @@ public def getArtifact (cache : Cache) (descr : ArtifactDescr) : EIO String Arti
 def writeOutputsCore
   (cache : Cache) (scope : String) (inputHash : Hash) (out : Json)
   (service? : Option CacheServiceName) (remoteScope? : Option CacheServiceScope)
+  (overwrite : Bool)
 : IO Unit := do
   let file := cache.outputsFile scope inputHash
   createParentDirs file
   let out := {service?, scope? := remoteScope?, data := out : CacheOutput}
-  IO.FS.writeFile file (toJson out).pretty
+  let contents := (toJson out).pretty
+  if overwrite then
+    IO.FS.writeFile file contents
+  else
+    writeFileIfNew file contents
 
 /-- Cache the outputs corresponding to the given input for the package.  -/
 @[inline] public def writeOutputs
-  [ToJson α] (cache : Cache) (scope : String) (inputHash : Hash) (outputs : α)
-: IO Unit := cache.writeOutputsCore scope inputHash (toJson outputs) none none
+  [ToJson α] (cache : Cache) (scope : String) (inputHash : Hash) (outputs : α) (update := true)
+: IO Unit := cache.writeOutputsCore scope inputHash (toJson outputs) none none update
 
 /-- Cache the input-to-outputs mappings from a `CacheMap`.  -/
 public def writeMap
   (cache : Cache) (scope : String) (map : CacheMap)
   (service? : Option CacheServiceName := none) (remoteScope? : Option CacheServiceScope := none)
-: IO Unit := map.forM fun i e => cache.writeOutputsCore scope i e.out service? remoteScope?
+  (overwrite := true)
+: IO Unit := map.forM fun i e => cache.writeOutputsCore scope i e.out service? remoteScope? overwrite
 
 /-- Retrieve the cached outputs corresponding to the given input for the package (if any). -/
 public def readOutputs? (cache : Cache) (scope : String) (inputHash : Hash) : LogIO (Option CacheOutput) := do

tests/lake/tests/ltar/test.sh

@@ -54,6 +54,15 @@ test_run -f restoreAll.toml build +Test -v --wfail -o .lake/outputs.jsonl
 test_cmd ls .lake/cache/artifacts/*.ltar
 test_exp -f .lake/build/ir/Test.ltar
 
+# Test that the cache input-to-output mapping is overwritten without
+# `--keep-local`. Since the build mapping includes module outputs and the
+# tracked mapping only includes the `ltar`, the tracking mapping should
+# require an unpack, whereas the build mapping should not.
+test_run cache add .lake/outputs.jsonl --keep-local
+LAKE_ARTIFACT_CACHE=true test_not_out "leantar" build +Test --no-build -v
+test_run cache add .lake/outputs.jsonl
+LAKE_ARTIFACT_CACHE=true test_out "leantar" build +Test --no-build -v
+
 # Test producing an `ltar` without already restored artifacts
 rm -rf .lake/cache .lake/build
 LAKE_ARTIFACT_CACHE=true test_run build +Test -v