refactor: lake: ensure job actions can be lifted to FetchM (#4273)

In `v4.8.0-rc2`, due to additional build refactor changes, `JobM` no
longer cleanly lifts in `FetchM`. Generally, a `JobM` action should not
be run `FetchM` directly but spawned asynchronously as job (e.g., via
`Job.async`). However, there may be some edge cases were this is
necessary and it is a backwards compatibility break, so this change adds
back the lift. This change also includes an `example` definition to
ensure the lift works in order to prevent similar accidental breakages
in the future.

This breakage was first reported by Mario on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/v4.2E8.2E0-rc2.20discussion/near/440407037).

src/lake/Lake/Build/Actions.lean

@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 import Lake.Util.Proc
 import Lake.Util.NativeLib
-import Lake.Build.Job
+import Lake.Util.IO
 
 /-! # Common Build Actions
 Low level actions to build common Lean artifacts via the Lean toolchain.
@@ -22,7 +22,7 @@ def compileLeanModule
   (leanPath : SearchPath := []) (rootDir : FilePath := ".")
   (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
   (leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: JobM Unit := do
+: LogIO Unit := do
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -70,7 +70,7 @@ def compileLeanModule
 def compileO
   (oFile srcFile : FilePath)
   (moreArgs : Array String := #[]) (compiler : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs oFile
   proc {
     cmd := compiler.toString
@@ -80,7 +80,7 @@ def compileO
 def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)
   (ar : FilePath := "ar")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs libFile
   proc {
     cmd := ar.toString
@@ -90,7 +90,7 @@ def compileStaticLib
 def compileSharedLib
   (libFile : FilePath) (linkArgs : Array String)
   (linker : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs libFile
   proc {
     cmd := linker.toString
@@ -100,7 +100,7 @@ def compileSharedLib
 def compileExe
   (binFile : FilePath) (linkFiles : Array FilePath)
   (linkArgs : Array String := #[]) (linker : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs binFile
   proc {
     cmd := linker.toString

src/lake/Lake/Build/Basic.lean

@@ -95,3 +95,13 @@ abbrev MonadBuild (m : Type → Type u) :=
 
 /-- The internal core monad of Lake builds.  Not intended for user use. -/
 abbrev CoreBuildM := BuildT LogIO
+
+/--
+Logs a build step with `message`.
+
+**Deprecated:**  Build steps are now managed by a top-level build monitor.
+As a result, this no longer functions the way it used to. It now just logs the
+`message` via `logVerbose`.
+-/
+@[deprecated, inline] def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do
+  logVerbose message

src/lake/Lake/Build/Fetch.lean

@@ -25,6 +25,19 @@ abbrev RecBuildM :=
 
 instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
 
+/--
+Run a `JobM` action in `RecBuildM` (and thus `FetchM`).
+
+Generally, this should not be done, and instead a job action
+should be run asynchronously in a Job (e.g., via `Job.async`).
+-/
+@[inline] def RecBuildM.runJobM (x : JobM α) : RecBuildM α := fun _ ctx log store => do
+  match (← x ctx {log}) with
+  | .ok a s => return (.ok a s.log, store)
+  | .error e s => return (.error e s.log, store)
+
+instance : MonadLift JobM RecBuildM := ⟨RecBuildM.runJobM⟩
+
 /-- Run a recursive build. -/
 @[inline] def RecBuildM.run
   (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
@@ -55,6 +68,12 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 /-- The top-level monad for Lake build functions. -/
 abbrev FetchM := IndexT RecBuildM
 
+/-- Ensures that `JobM` lifts into `FetchM`. -/
+example : MonadLiftT JobM FetchM := inferInstance
+
+/-- Ensures that `SpawnM` lifts into `FetchM`. -/
+example : MonadLiftT SpawnM FetchM := inferInstance
+
 /-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
 @[deprecated FetchM] abbrev IndexBuildM := FetchM
 

src/lake/Lake/Build/Job.lean

@@ -66,7 +66,13 @@ abbrev JobResult α := EResult Log.Pos JobState α
 /-- The `Task` of a Lake job. -/
 abbrev JobTask α := BaseIOTask (JobResult α)
 
-/-- The monad of asynchronous Lake jobs. Lifts into `FetchM`. -/
+/--
+The monad of asynchronous Lake jobs.
+
+While this can be lifted into `FetchM`, job action should generally
+be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
+run directly in `FetchM`.
+-/
 abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO
 
 instance [Pure m] : MonadLift LakeM (BuildT m) where
@@ -94,16 +100,6 @@ abbrev SpawnM := BuildT BaseIO
 /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
 @[deprecated SpawnM] abbrev SchedulerM := SpawnM
 
-/--
-Logs a build step with `message`.
-
-**Deprecated:**  Build steps are now managed by a top-level build monitor.
-As a result, this no longer functions the way it used to. It now just logs the
-`message` via `logVerbose`.
--/
-@[deprecated] def logStep (message : String) : JobM Unit := do
-  logVerbose message
-
 /-- A Lake job. -/
 structure Job (α : Type u)  where
   task : JobTask α

src/lake/Lake/Build/Trace.lean

@@ -3,18 +3,16 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.IO
 
 open System
+
 namespace Lake
 
 --------------------------------------------------------------------------------
 /-! # Utilities -/
 --------------------------------------------------------------------------------
 
-/-- Creates any missing parent directories of `path`. -/
-@[inline] def createParentDirs (path : FilePath) : IO Unit := do
-  if let some dir := path.parent then IO.FS.createDirAll dir
-
 class CheckExists.{u} (i : Type u) where
   /-- Check whether there already exists an artifact for the given target info. -/
   checkExists : i → BaseIO Bool

src/lake/Lake/Util/IO.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+/-- Creates any missing parent directories of `path`. -/
+@[inline] def createParentDirs (path : System.FilePath) : IO Unit := do
+  if let some dir := path.parent then IO.FS.createDirAll dir