feat: lake.lock file for builds

src/lake/Lake/Build/Actions.lean

@@ -10,9 +10,6 @@ import Lake.Build.Context
 namespace Lake
 open System
 
-def createParentDirs (path : FilePath) : IO Unit := do
-  if let some dir := path.parent then IO.FS.createDirAll dir
-
 def compileLeanModule (name : String) (leanFile : FilePath)
 (oleanFile? ileanFile? cFile? : Option FilePath)
 (leanPath : SearchPath := []) (rootDir : FilePath := ".")

src/lake/Lake/Build/Context.lean

@@ -56,3 +56,6 @@ def logStep (message : String) : BuildM Unit := do
   let done ← (← read).finishedBuilds.get
   let started ← (← read).startedBuilds.get
   logInfo s!"[{done}/{started}] {message}"
+
+def createParentDirs (path : FilePath) : IO Unit := do
+  if let some dir := path.parent then IO.FS.createDirAll dir

src/lake/Lake/Build/Monad.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
+Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 -/
 import Lake.Config.Monad
 import Lake.Build.Context
@@ -47,10 +47,46 @@ If a cycle is encountered, log it and then fail.
 @[inline] def RecBuildM.run (build : RecBuildM α) : BuildM α := do
   (·.1) <$> build.runIn {}
 
+/--
+Busy waits to acquire the lock represented by the `lockFile`.
+Prints a warning if on the first time it has to wait.
+-/
+@[inline] partial def busyAcquireLockFile (lockFile : FilePath) : IO PUnit := do
+  busyLoop true
+where
+  busyLoop firstTime :=
+    try
+      -- Remark: fail if already exists
+      -- (not part of POSIX, but supported on all our platforms)
+      createParentDirs lockFile
+      let h ← IO.FS.Handle.mk lockFile .writeNew
+      h.putStrLn <| toString <| ← IO.Process.getPID
+    catch
+      | .alreadyExists .. => do
+        if firstTime then
+          let stderr ← IO.getStderr
+          stderr.putStrLn s!"warning: waiting for prior `lake build` invocation to finish... (remove '{lockFile}' if stuck)"
+          stderr.flush
+        IO.sleep (ms := 300)
+        busyLoop false
+      | e => throw e
+
+/-- 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
+
+/-- The name of the Lake build lock file name (i.e., `lake.lock`). -/
+@[noinline] def lockFileName : String :=
+  "lake.lock"
+
+/-- The workspace's build lock file. -/
+@[inline] def Workspace.lockFile (self : Workspace) : FilePath :=
+  self.root.buildDir / lockFileName
+
 /-- Run the given build function in the Workspace's context. -/
 @[inline] def Workspace.runBuild (ws : Workspace) (build : BuildM α) (oldMode := false) : LogIO α := do
   let ctx ← mkBuildContext ws oldMode
-  build.run ctx
+  withLockFile ws.lockFile do build.run ctx
 
 /-- Run the given build function in the Lake monad's workspace. -/
 @[inline] def runBuild (build : BuildM α) (oldMode := false) : LakeT LogIO α := do

src/lake/Lake/Util/OptionIO.lean

@@ -30,15 +30,21 @@ namespace OptionIO
 @[inline] def catchFailure (f : Unit → BaseIO α) (self : OptionIO α) : BaseIO α :=
   self.toEIO.catchExceptions f
 
-protected def failure : OptionIO α :=
+@[inline] protected def failure : OptionIO α :=
   mk <| throw ()
 
-protected def orElse (self : OptionIO α) (f : Unit → OptionIO α) : OptionIO α :=
+@[inline] protected def orElse (self : OptionIO α) (f : Unit → OptionIO α) : OptionIO α :=
   mk <| tryCatch self.toEIO f
 
 instance : Alternative OptionIO where
   failure := OptionIO.failure
   orElse := OptionIO.orElse
 
+@[always_inline] instance OptionIO.finally : MonadFinally OptionIO where
+  tryFinally' := fun x h => do
+    match (← x.toBaseIO) with
+    | some a => return (a, ← h (some a))
+    | none => failure
+
 def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
   self.toBaseIO.asTask prio

src/lake/test/lock/.gitignore

@@ -0,0 +1,3 @@
+/build
+/lake-packages/*
+test.log

src/lake/test/lock/Loop.lean

@@ -0,0 +1 @@
+#eval do repeat IO.sleep 300

src/lake/test/lock/clean.sh

@@ -0,0 +1,2 @@
+rm -rf build
+rm -f test.log

src/lake/test/lock/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package «lock»
+
+lean_lib Loop
+lean_lib Test

src/lake/test/lock/test.sh

@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+set -mexo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+if [ "`uname`" = Darwin ]; then
+  TAIL=gtail
+else
+  TAIL=tail
+fi
+
+./clean.sh
+
+# Test lock file creation on build
+$LAKE build Loop 2>&1 > test.log &
+grep -q "Building" < <($TAIL --pid=$$ -f test.log)
+kill %%
+test -f build/lake.lock
+
+# Test build waits when lock file present
+$LAKE build Test 2>&1 | tee test.log &
+grep -q "waiting" < <($TAIL --pid=$$ -f test.log)
+# Test build resumes on lock file removal
+rm build/lake.lock
+fg
+echo "done"