diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index e83b69828d..4be6e4e179 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/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 := ".") diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean index dc10a84932..8885a9957a 100644 --- a/src/lake/Lake/Build/Context.lean +++ b/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 diff --git a/src/lake/Lake/Build/Monad.lean b/src/lake/Lake/Build/Monad.lean index ab94ee1f38..7c7bd10114 100644 --- a/src/lake/Lake/Build/Monad.lean +++ b/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 diff --git a/src/lake/Lake/Util/OptionIO.lean b/src/lake/Lake/Util/OptionIO.lean index 426df68749..26fd29c1f2 100644 --- a/src/lake/Lake/Util/OptionIO.lean +++ b/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 diff --git a/src/lake/test/lock/.gitignore b/src/lake/test/lock/.gitignore new file mode 100644 index 0000000000..8c9e2cd294 --- /dev/null +++ b/src/lake/test/lock/.gitignore @@ -0,0 +1,3 @@ +/build +/lake-packages/* +test.log diff --git a/src/lake/test/lock/Loop.lean b/src/lake/test/lock/Loop.lean new file mode 100644 index 0000000000..ab3d0aa828 --- /dev/null +++ b/src/lake/test/lock/Loop.lean @@ -0,0 +1 @@ +#eval do repeat IO.sleep 300 diff --git a/src/lake/test/lock/Test.lean b/src/lake/test/lock/Test.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/lake/test/lock/clean.sh b/src/lake/test/lock/clean.sh new file mode 100755 index 0000000000..f8555e9cf3 --- /dev/null +++ b/src/lake/test/lock/clean.sh @@ -0,0 +1,2 @@ +rm -rf build +rm -f test.log diff --git a/src/lake/test/lock/lakefile.lean b/src/lake/test/lock/lakefile.lean new file mode 100644 index 0000000000..a5d5122de5 --- /dev/null +++ b/src/lake/test/lock/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package «lock» + +lean_lib Loop +lean_lib Test diff --git a/src/lake/test/lock/test.sh b/src/lake/test/lock/test.sh new file mode 100755 index 0000000000..6daa9ab68e --- /dev/null +++ b/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"