From 216d2460e0adec8317fdeeb6f2543cb7442564fd Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 23 Aug 2023 00:52:48 -0400 Subject: [PATCH] doc: explanation for `lake.lock` disabling Co-authored-by: Scott Morrison --- src/lake/Lake/Build/Monad.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/Build/Monad.lean b/src/lake/Lake/Build/Monad.lean index 93938403a1..ab335aece2 100644 --- a/src/lake/Lake/Build/Monad.lean +++ b/src/lake/Lake/Build/Monad.lean @@ -94,7 +94,13 @@ where /-- 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 - --withLockFile ws.lockFile do + /- + TODO: + The lock file has been temporarily disabled (by lean4#2445) + until we have an API for catching `Ctrl-C` during a build. + Absent this, the lock file was too disruptive for users. + -/ + -- withLockFile ws.lockFile do build.run ctx /-- Run the given build function in the Lake monad's workspace. -/