From 0196cbe6a36615c67a314e11369d6592c58a3aaa Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 6 Oct 2021 16:27:49 -0400 Subject: [PATCH] refactor: move build execution into CLI --- Lake/BuildBin.lean | 8 ++++---- Lake/BuildMonad.lean | 23 +--------------------- Lake/BuildPackage.lean | 43 +++++++++++++++++------------------------- Lake/Cli.lean | 38 ++++++++++++++++++++++++++++++++----- 4 files changed, 55 insertions(+), 57 deletions(-) diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 6cbcc6d5b1..845fc56848 100644 --- a/Lake/BuildBin.lean +++ b/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 diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index efb0c1bbf4..552ce61822 100644 --- a/Lake/BuildMonad.lean +++ b/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 diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index c938c51db8..a619aa49e1 100644 --- a/Lake/BuildPackage.lean +++ b/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 diff --git a/Lake/Cli.lean b/Lake/Cli.lean index c46b40ba60..85ecbafc19 100644 --- a/Lake/Cli.lean +++ b/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