fix: lake: do not cache files already in the cache

Author: tydeu

src/lake/Lake/Build/Common.lean

@@ -453,13 +453,14 @@ public def Cache.saveArtifact
     let hash := Hash.ofString normalized
     let descr := artifactWithExt hash ext
     let cacheFile := cache.artifactDir / descr.relPath
-    createParentDirs cacheFile
     -- make the local file unwritable where possible to discourage users from
     -- writing to such paths as this can corrupt the cache if the file was hard linked
     let r := {read := true, write := false, execution := false}
     IO.setAccessRights file ⟨r, r, r⟩
-    IO.FS.writeFile cacheFile normalized
-    IO.setAccessRights cacheFile ⟨r, r, r⟩
+    unless (← cacheFile.pathExists) do
+      createParentDirs cacheFile
+      IO.FS.writeFile cacheFile normalized
+      IO.setAccessRights cacheFile ⟨r, r, r⟩
     writeFileHash file hash
     let mtime := (← getMTime cacheFile |>.toBaseIO).toOption.getD 0
     let path := if useLocalFile then file else cacheFile
@@ -469,14 +470,15 @@ public def Cache.saveArtifact
     let hash := Hash.ofByteArray contents
     let descr := artifactWithExt hash ext
     let cacheFile := cache.artifactDir / descr.relPath
-    createParentDirs cacheFile
     -- make the local file unwritable where possible to discourage users from
     -- writing to such paths as this can corrupt the cache if the file is hard linked
     let r := {read := true, write := false, execution := exe}
     IO.setAccessRights file ⟨r, r, r⟩
-    if let .error _ ← (IO.FS.hardLink file cacheFile).toBaseIO then
-      IO.FS.writeBinFile cacheFile contents
-      IO.setAccessRights cacheFile ⟨r, r, r⟩
+    unless (← cacheFile.pathExists) do
+      createParentDirs cacheFile
+      if let .error _ ← (IO.FS.hardLink file cacheFile).toBaseIO then
+        IO.FS.writeBinFile cacheFile contents
+        IO.setAccessRights cacheFile ⟨r, r, r⟩
     writeFileHash file hash
     let mtime := (← getMTime cacheFile |>.toBaseIO).toOption.getD 0
     let path := if useLocalFile then file else cacheFile

tests/lake/tests/cache/test.sh

@@ -90,7 +90,6 @@ test_run exe test
 # The `Test` module's artifacts are more carefully managed throught this test
 touch Ignored.lean
 test_run -v build +Ignored
-test_cmd rm -f .lake/build/lib/lean/Ignored.trace
 
 # Verify that fetching from the cache can be disabled
 test_cmd rm -f .lake/build/lib/lean/Ignored.trace
@@ -159,6 +158,10 @@ test_out "Fetched Test:c.o" build +Test:o -v --no-build
 test_cmd rm -rf "$CACHE_DIR/outputs" .lake/build/ir/Test.c
 test_run -v build +Test:c --no-build
 
+# Verify that Lake does not attempt overwrite an existing artifact
+test_cmd rm -rf "$CACHE_DIR/outputs" .lake/build/lib/lean/Ignored.trace
+test_run -v build +Ignored
+
 # Verify that the olean does not need to be present in the build directory
 test_cmd rm -f .lake/build/lib/lean/Test.olean .lake/build/lib/lean/Test/Imported.olean
 test_run -v build +Test.Imported --no-build --wfail