diff --git a/src/lake/Lake/Build/Monad.lean b/src/lake/Lake/Build/Monad.lean index 7c7bd10114..1500232831 100644 --- a/src/lake/Lake/Build/Monad.lean +++ b/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 := diff --git a/src/lake/test/lock/Test.lean b/src/lake/test/lock/Nop.lean similarity index 100% rename from src/lake/test/lock/Test.lean rename to src/lake/test/lock/Nop.lean diff --git a/src/lake/test/lock/Wait.lean b/src/lake/test/lock/Wait.lean new file mode 100644 index 0000000000..29591b9045 --- /dev/null +++ b/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 diff --git a/src/lake/test/lock/lakefile.lean b/src/lake/test/lock/lakefile.lean index be76b56f90..cdc964be56 100644 --- a/src/lake/test/lock/lakefile.lean +++ b/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 diff --git a/src/lake/test/lock/test.sh b/src/lake/test/lock/test.sh index 4c59dbcdf4..87069f3ed5 100755 --- a/src/lake/test/lock/test.sh +++ b/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"