refactor: move build execution into CLI

Lake/BuildBin.lean

@@ -31,8 +31,8 @@ def Package.staticLibTarget (self : Package) : FileTarget :=
  Target.mk self.staticLibFile do
     (← self.buildTarget).staticLibTarget.materializeAsync
 
-def buildLib (pkg : Package) : IO PUnit :=
-  pkg.staticLibTarget.build.run'
+def Package.buildLib (pkg : Package) : BuildM FilePath :=
+  pkg.staticLibTarget.build
 
 -- # Build Package Bin
 
@@ -51,5 +51,5 @@ def Package.binTarget (self : Package) : FileTarget :=
     let pkgTarget ← self.buildModuleOleanAndCTargetsWithDepTargets #[self.binRoot] depTargets
     pkgTarget.binTarget depTargets >>= (·.materializeAsync)
 
-def buildBin (pkg : Package) : IO PUnit :=
-  pkg.binTarget.build.run'
+def Package.buildBin (pkg : Package) : BuildM FilePath :=
+  pkg.binTarget.build

Lake/BuildMonad.lean

@@ -56,18 +56,6 @@ namespace BuildContext
 
 deriving instance Inhabited for BuildContext
 
-def io : BuildContext where
-  methodsRef := BuildMethodsRef.mk {
-    logInfo  := fun msg => IO.println msg
-    logError := fun msg => IO.eprintln msg
-  }
-
-def ioErr : BuildContext where
-  methodsRef := BuildMethodsRef.mk {
-    logInfo  := fun msg => IO.eprintln msg
-    logError := fun msg => IO.eprintln msg
-  }
-
 def methods (self : BuildContext) : BuildMethods :=
   self.methodsRef.get
 
@@ -97,16 +85,7 @@ def convErrors (self : BuildM α) : BuildM α := do
     throw <| IO.userError "build failed"
 
 def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
-  self ctx
-
-def run (self : BuildM α) : IO α :=
-  (convErrors self).runIn BuildContext.io
-
-def runErr (self : BuildM α) : IO α :=
-  (convErrors self).runIn BuildContext.ioErr
-
-def run' (self : BuildM α) : IO PUnit :=
-  discard self.run
+  (convErrors self) ctx
 
 end BuildM
 

Lake/BuildPackage.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lean.Data.Name
-import Lean.Data.Json
 import Lean.Elab.Import
 import Lake.Target
 import Lake.BuildModule
@@ -146,9 +145,6 @@ def Package.buildDeps (self : Package) : BuildM (Array Package) := do
   let targets ← self.buildDepTargets
   targets.mapM fun target => Functor.mapConst target.info.1 target.materialize
 
-def configure (pkg : Package) : IO Unit :=
-  pkg.buildDeps.run'
-
 def Package.build (self : Package) : BuildM PUnit := do
   let depTargets ← self.buildDepTargets
   let depTarget ← self.buildDepTargetWith depTargets
@@ -156,13 +152,11 @@ def Package.build (self : Package) : BuildM PUnit := do
   let targets ← self.buildOleanTargets moreOleanDirs depTarget
   discard <| ActiveTarget.materializeArray targets
 
-def build (pkg : Package) : IO PUnit :=
-  pkg.build.run
-
--- # Print Paths
+-- # Build Imports
 
 /-- Pick the local imports of the package from a list of import strings. -/
-def Package.filterLocalImports (imports : List String) (self : Package) : Array Name := do
+def Package.filterLocalImports
+(imports : List String) (self : Package) : Array Name := do
   let mut localImports := #[]
   for imp in imports do
     let impName := imp.toName
@@ -170,20 +164,17 @@ def Package.filterLocalImports (imports : List String) (self : Package) : Array
       localImports := localImports.push impName
   return localImports
 
-def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
-  let deps ← BuildM.runErr do
-    -- resolve and build deps
-    let depTargets ← pkg.buildDepTargets
-    let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) []
-    -- build any additional imports
-    unless imports.isEmpty do
-      let moreOleanDirs := depPkgs.map (·.oleanDir)
-      let depTarget ← pkg.buildDepTargetWith depTargets
-      let localImports := pkg.filterLocalImports imports
-      let oleanTargets ← pkg.buildModuleOleanTargets localImports moreOleanDirs depTarget
-      oleanTargets.forM (discard ·.materialize)
-    pure depPkgs
-  IO.println <| Json.compress <| Json.mkObj [
-    ("LEAN_PATH", SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)),
-    ("LEAN_SRC_PATH", SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir))
-  ]
+/-- Build the packages dependencies and a list of imports, returning the list of packages built. -/
+def Package.buildImportsAndDeps
+(imports : List String := []) (self : Package) : BuildM (List Package) := do
+  -- resolve and build deps
+  let depTargets ← self.buildDepTargets
+  let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) []
+  -- build any additional imports
+  unless imports.isEmpty do
+    let moreOleanDirs := depPkgs.map (·.oleanDir)
+    let depTarget ← self.buildDepTargetWith depTargets
+    let localImports := self.filterLocalImports imports
+    let oleanTargets ← self.buildModuleOleanTargets localImports moreOleanDirs depTarget
+    oleanTargets.forM (discard ·.materialize)
+  pure depPkgs

Lake/Cli.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Data.Json
 import Lake.Init
 import Lake.Help
 import Lake.BuildBin
@@ -12,6 +13,8 @@ import Lake.InstallPath
 import Lake.CliT
 
 open System
+open Lean (Json)
+
 namespace Lake
 
 -- # Utilities
@@ -126,6 +129,18 @@ def output (msg : String) : CliM UInt32 := do
 def execIO (x : IO α) : CliM UInt32 := do
   try Functor.mapConst 0 x catch e => error (toString e)
 
+/--
+  Perform the given build action and then return code 0.
+  If it throws an error, invoke `error` with the the error's message.
+-/
+def execBuild (x : BuildM α) : CliM UInt32 := do
+  execIO <| x.runIn {
+    methodsRef := BuildMethodsRef.mk {
+      logInfo  := fun msg => IO.println msg
+      logError := fun msg => IO.eprintln msg
+    }
+  }
+
 /-- Run the given script from the given package with the given arguments. -/
 def script (pkg : Package) (name : String) (args : List String) :  CliM UInt32 := do
   if let some script := pkg.scripts.find? name then
@@ -160,15 +175,28 @@ def verifyInstall : CliM UInt32 := do
   IO.println s!"Lake:\n{repr <| ← getLakeInstall?}"
   verifyLeanVersion
 
+def printPaths (pkg : Package) (imports : List String := []) : CliM UInt32 :=
+  execIO do
+    let deps ← pkg.buildImportsAndDeps imports |>.runIn {
+      methodsRef := BuildMethodsRef.mk {
+        logInfo  := fun msg => IO.eprintln msg
+        logError := fun msg => IO.eprintln msg
+      }
+    }
+    IO.println <| Json.compress <| Json.mkObj [
+      ("LEAN_PATH", SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)),
+      ("LEAN_SRC_PATH", SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir))
+    ]
+
 def command : (cmd : String) → CliM UInt32
 | "new"         => do noArgsRem <| execIO <| new (← takeArg)
 | "init"        => do noArgsRem <| execIO <| init (← takeArg)
 | "run"         => do noArgsRem <| script (← loadPkg []) (← takeArg) (← getSubArgs)
-| "configure"   => do noArgsRem <| execIO <| configure (← loadPkg (← getSubArgs))
-| "print-paths" => do noArgsRem <| execIO <| printPaths (← loadPkg (← getSubArgs)) (← takeArgs)
-| "build"       => do noArgsRem <| execIO <| build (← loadPkg (← getSubArgs))
-| "build-lib"   => do noArgsRem <| execIO <| buildLib (← loadPkg (← getSubArgs))
-| "build-bin"   => do noArgsRem <| execIO <| buildBin (← loadPkg (← getSubArgs))
+| "configure"   => do noArgsRem <| execBuild (← loadPkg (← getSubArgs)).buildDeps
+| "print-paths" => do noArgsRem <| printPaths (← loadPkg (← getSubArgs)) (← takeArgs)
+| "build"       => do noArgsRem <| execBuild (← loadPkg (← getSubArgs)).build
+| "build-lib"   => do noArgsRem <| execBuild (← loadPkg (← getSubArgs)).buildLib
+| "build-bin"   => do noArgsRem <| execBuild (← loadPkg (← getSubArgs)).buildBin
 | "clean"       => do noArgsRem <| execIO <| (← loadPkg (← getSubArgs)).clean
 | "help"        => do output <| help (← takeArg?)
 | "self-check"  => noArgsRem <| verifyInstall