chore: fix removeFile on Windows

Author: tydeu

src/lake/Lake/Build/Module.lean

@@ -561,23 +561,29 @@ public def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
 
 /-- Remove all existing artifacts produced by the Lean build of the module. -/
 public def Module.clearOutputArtifacts (mod : Module) : IO PUnit := do
-  removeFileIfExists mod.oleanFile
-  removeFileIfExists mod.oleanServerFile
-  removeFileIfExists mod.oleanPrivateFile
-  removeFileIfExists mod.ileanFile
-  removeFileIfExists mod.irFile
-  removeFileIfExists mod.cFile
-  removeFileIfExists mod.bcFile
+  try
+    removeFileIfExists mod.oleanFile
+    removeFileIfExists mod.oleanServerFile
+    removeFileIfExists mod.oleanPrivateFile
+    removeFileIfExists mod.ileanFile
+    removeFileIfExists mod.irFile
+    removeFileIfExists mod.cFile
+    removeFileIfExists mod.bcFile
+  catch e =>
+    error s!"failed to remove output artifacts: {e}"
 
 /-- Remove any cached file hashes of the module build outputs (in `.hash` files). -/
 public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
-  clearFileHash mod.oleanFile
-  clearFileHash mod.oleanServerFile
-  clearFileHash mod.oleanPrivateFile
-  clearFileHash mod.ileanFile
-  clearFileHash mod.irFile
-  clearFileHash mod.cFile
-  clearFileHash mod.bcFile
+  try
+    clearFileHash mod.oleanFile
+    clearFileHash mod.oleanServerFile
+    clearFileHash mod.oleanPrivateFile
+    clearFileHash mod.ileanFile
+    clearFileHash mod.irFile
+    clearFileHash mod.cFile
+    clearFileHash mod.bcFile
+  catch e =>
+    error s!"failed to remove output hashes: {e}"
 
 /-- Cache the file hashes of the module build outputs in `.hash` files. -/
 public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do

src/lake/Lake/Util/IO.lean

@@ -16,9 +16,23 @@ namespace Lake
 public def createParentDirs (path : FilePath) : IO Unit := do
   if let some dir := path.parent then IO.FS.createDirAll dir
 
+/--
+Remove the file at `path`.
+Also removes read-only files on Windows, unlike `IO.FS.removeFile`.
+-/
+def removeFile (path : FilePath) : IO Unit := do
+  try IO.FS.removeFile path catch
+    | e@(.permissionDenied ..) =>
+      if Platform.isWindows then
+        let rw := {read := true, write := true}
+        IO.setAccessRights path ⟨rw, rw, rw⟩
+        IO.FS.removeFile path
+      else throw e
+    | e => throw e
+
 /-- Remove the file at `path` if it exists. -/
 public def removeFileIfExists (path : FilePath) : IO Unit := do
-  try IO.FS.removeFile path catch
+  try removeFile path catch
     | .noFileOrDirectory .. => pure ()
     | e => throw e
 

tests/lake/tests/cache/test.sh

@@ -7,7 +7,7 @@ source ../common.sh
 
 # Store Lake cache in a local directory
 TEST_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)"
-CACHE_DIR="$TEST_DIR/.lake/cache"
+CACHE_DIR="$(norm_path "$TEST_DIR")/.lake/cache"
 export LAKE_CACHE_DIR="$CACHE_DIR"
 
 # Verify packages without `enableArtifactCache` do not use the cache by default

tests/lake/tests/common.sh

@@ -40,10 +40,9 @@ else
 fi
 
 if [ "$OS" = Windows_NT ]; then
-  norm_dirname() { cygpath -u "$(dirname -- "$1")";  }
-else
-  norm_dirname() { dirname -- "$1"; }
+  norm_path() { cygpath -u "$1";  }
 fi
+norm_dirname() { norm_path "$(dirname -- "$1")";  }
 
 init_git() {
   echo "# initialize test repository"