From e2407589ff8355e06ea3d62773c5a04e2629554e Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 17 Feb 2026 14:06:37 -0500
Subject: [PATCH] fix: lake: `cache clean` should succeed w/ no cache dir
 (#12532)

This PR fixes a bug with `cache clean` where it would fail if the cache
directory does not exist.

This introduces a `removeDirAllIfExists` utility which is also now used
in `lake clean`. While `lake clean` did previously check for a
nonexistent build directory, this version should be more robust to
racing runs of `lake clean` as well.
---
 src/lake/Lake/CLI/Main.lean       |  2 +-
 src/lake/Lake/Config/Package.lean |  4 ++--
 src/lake/Lake/Util/IO.lean        | 32 +++++++++++++++++++++++++++----
 tests/lake/tests/cache/test.sh    |  4 ++++
 4 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index db10c07b8e..da30085cdf 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -549,7 +549,7 @@ protected def clean : CliM PUnit := do
       return cache.dir
     else
       error "no cache to delete; no workspace configuration found and no system cache detected"
-  IO.FS.removeDirAll dir
+  removeDirAllIfExists dir
 
 protected def help : CliM PUnit := do
   IO.println <| helpCache <| ← takeArgD ""
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index dffed4dbeb..d11acf23a2 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -16,6 +16,7 @@ public import Lake.Util.OrdHashSet
 public import Lake.Util.Name
 meta import all Lake.Util.OpaqueType
 import Lake.Util.OpaqueType
+import Lake.Util.IO
 
 open System Lean
 
@@ -407,5 +408,4 @@ public def isBuildableModule (mod : Name) (self : Package) : Bool :=
 
 /-- Remove the package's build outputs (i.e., delete its build directory). -/
 public def clean (self : Package) : IO PUnit := do
-  if (← self.buildDir.pathExists) then
-    IO.FS.removeDirAll self.buildDir
+  removeDirAllIfExists self.buildDir
diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean
index 65214e61f5..46a0bf2aaa 100644
--- a/src/lake/Lake/Util/IO.lean
+++ b/src/lake/Lake/Util/IO.lean
@@ -10,24 +10,48 @@ public import Init.System.IO
 
 open System
 
+set_option doc.verso true
+
 namespace Lake
 
-/-- Creates any missing parent directories of `path`. -/
+/-- Creates any missing parent directories of {lean}`path`. -/
 public def createParentDirs (path : FilePath) : IO Unit := do
   if let some dir := path.parent then IO.FS.createDirAll dir
 
-/-- Remove the file at `path` if it exists. -/
+/-- Remove the file at {lean}`path` if it exists. -/
 public def removeFileIfExists (path : FilePath) : IO Unit := do
   try IO.FS.removeFile path catch
     | .noFileOrDirectory .. => pure ()
     | e => throw e
 
-/-- Copy a file from `src` to `dst`. -/
+/--
+Remove a directory and all its contents.
+Like {lean}`IO.FS.removeDirAll`, but does not fail if {lean}`path` does not exist
+or if a file is first deleted by a racing process.
+-/
+public partial def removeDirAllIfExists (path : FilePath) : IO Unit := do
+  let ents ← try path.readDir catch
+    | .noFileOrDirectory .. => return -- path did not exist or something else was faster
+    | e => throw e
+  for ent in ents do
+    -- Do not follow symlinks
+    let mdata ← try ent.path.symlinkMetadata catch
+      | .noFileOrDirectory .. => continue -- something else was faster
+      | e => throw e
+    if mdata.type == .dir then
+      removeDirAllIfExists ent.path
+    else
+      removeFileIfExists ent.path
+  try IO.FS.removeDir path catch
+    | .noFileOrDirectory .. => return -- something else was faster
+    | e => throw e
+
+/-- Copy a file from {lean}`src` to {lean}`dst`. -/
 public def copyFile (src dst : FilePath) : IO Unit := do
   let contents ← IO.FS.readBinFile src
   IO.FS.writeBinFile dst contents
 
-/-- Returns the normalized real path of a file if it exists. Otherwise, returns `""`. -/
+/-- Returns the normalized real path of a file if it exists. Otherwise, returns {lean}`""`. -/
 public def resolvePath (path : FilePath) : BaseIO FilePath := do
   match (← (IO.FS.realPath path).toBaseIO) with
   | .ok path =>
diff --git a/tests/lake/tests/cache/test.sh b/tests/lake/tests/cache/test.sh
index 9fd32a1018..73124f4a4e 100755
--- a/tests/lake/tests/cache/test.sh
+++ b/tests/lake/tests/cache/test.sh
@@ -11,6 +11,10 @@ TEST_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)"
 CACHE_DIR="$(norm_path "$TEST_DIR")/.lake/cache"
 export LAKE_CACHE_DIR="$CACHE_DIR"
 
+# Verify that `lake cache clean` works without a cache directory
+test_exp ! -d "$CACHE_DIR"
+test_run cache clean
+
 # Verify packages without `enableArtifactCache` do not use the cache by default
 test_run build -f unset.toml Test:static
 test_exp ! -d "$CACHE_DIR"