diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 6edc0024a946a..05de78e516dbd 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/src/lake/Lake/Build/Actions.lean @@ -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 diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index 4e54ebbf4b875..46d0115e93cea 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/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] def logStep (message : String) : LogIO Unit := do + logVerbose message diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index e6b94e3fa3ccd..81eedbdfd0114 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/src/lake/Lake/Build/Fetch.lean @@ -55,6 +55,9 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m /-- The top-level monad for Lake build functions. -/ abbrev FetchM := IndexT RecBuildM +/-- Verifies 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 diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 00617dcf59370..ffdc2613eb241 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -66,7 +66,7 @@ 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. -/ abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO instance [Pure m] : MonadLift LakeM (BuildT m) where @@ -94,16 +94,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 α