feat: warn rather than error if lake.lock disappears

src/lake/Lake/Build/Monad.lean

@@ -73,7 +73,15 @@ where
 
 /-- Busy wait to acquire the lock of `lockFile`, run `act`, and then release the lock. -/
 @[inline] def withLockFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (lockFile : FilePath) (act : m α) : m α := do
-  try busyAcquireLockFile lockFile; act finally IO.FS.removeFile lockFile
+  try
+    busyAcquireLockFile lockFile; act
+  finally show IO _ from do
+    try
+      IO.FS.removeFile lockFile
+    catch
+      | .noFileOrDirectory .. => IO.eprintln <|
+        s!"warning: `{lockFile}` was deleted before the lock was released"
+      | e => throw e
 
 /-- The name of the Lake build lock file name (i.e., `lake.lock`). -/
 @[noinline] def lockFileName : String :=

src/lake/test/lock/Wait.lean

@@ -0,0 +1,8 @@
+import Lake.Build.Monad
+
+partial def busyWaitFile (file : System.FilePath) : BaseIO PUnit := do
+  if (← file.pathExists) then
+    IO.sleep (ms := 300)
+    busyWaitFile file
+
+#eval busyWaitFile <| "build" / Lake.lockFileName

src/lake/test/lock/lakefile.lean

@@ -4,5 +4,6 @@ open Lake DSL
 package «lock»
 
 lean_lib Loop
-lean_lib Test
+lean_lib Nop
 lean_lib Error
+lean_lib Wait

src/lake/test/lock/test.sh

@@ -23,7 +23,7 @@ kill $test1_pid
 # Test build waits when lock file present
 touch test2.log
 touch build/lake.lock
-$LAKE build Test 2> test2.log &
+$LAKE build Nop 2> test2.log &
 test2_pid=$!
 grep -q "waiting" < <($TAIL --pid=$$ -f test2.log)
 # Test build resumes on lock file removal
@@ -35,3 +35,12 @@ test ! -f build/lake.lock
 # Test build error still deletes lock file
 ! $LAKE build Error
 test ! -f build/lake.lock
+
+# Test that removing the lock during build does not cause it to fail
+touch test3.log
+$LAKE build Wait > test3.log 2>&1 &
+test3_pid=$!
+grep -q "Building" < <($TAIL --pid=$$ -f test3.log)
+rm build/lake.lock
+wait $test3_pid
+cat test3.log | grep "deleted before the lock"