diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 6edc0024a946..44be2002ea2b 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/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 diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index 4e54ebbf4b87..ec257525d562 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, inline] def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do + logVerbose message diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index e6b94e3fa3cc..8b6ea6d2687f 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/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 diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 00617dcf5937..dea138ce9717 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/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 α diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 461b6b57c4b7..43e841a2f67a 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/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 diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean new file mode 100644 index 000000000000..e67ec54aa735 --- /dev/null +++ b/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