diff --git a/Lake/Build/MonadBasic.lean b/Lake/Build/Context.lean similarity index 55% rename from Lake/Build/MonadBasic.lean rename to Lake/Build/Context.lean index c9873be374..dd59156a3f 100644 --- a/Lake/Build/MonadBasic.lean +++ b/Lake/Build/Context.lean @@ -6,30 +6,22 @@ Authors: Mac Malone import Lake.Util.Task import Lake.Config.Opaque import Lake.Config.InstallPath +import Lake.Config.Context import Lake.Build.Trace import Lake.Build.IO open System namespace Lake -structure BuildContext where - lean : LeanInstall - lake : LakeInstall - workspace : OpaqueWorkspace +/-- A Lake context with some additional caching for builds. -/ +structure BuildContext extends Context where leanTrace : BuildTrace -abbrev BuildM := - ReaderT BuildContext BuildIO +/-- The monad for Lake builds. -/ +abbrev BuildM := ReaderT BuildContext BuildIO /-- `Task` type for `BuildM`/`BuildIO`. -/ -abbrev BuildTask := - OptionIOTask +abbrev BuildTask := OptionIOTask def BuildM.run (logMethods : LogMethods BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α := self ctx |>.run logMethods - -def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α -| Except.ok a => a -| Except.error cycle => do - let cycle := cycle.map (s!" {·}") - error s!"build cycle detected:\n{"\n".intercalate cycle}" diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean index d0a843e7b4..9ebc54418c 100644 --- a/Lake/Build/Monad.lean +++ b/Lake/Build/Monad.lean @@ -3,69 +3,34 @@ 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.Config.Package -import Lake.Config.Workspace -import Lake.Build.MonadBasic +import Lake.Config.Monad +import Lake.Build.Context open System open Lean (Name) namespace Lake +deriving instance Inhabited for BuildContext + def mkBuildContext (ws : Workspace) (lean : LeanInstall) (lake : LakeInstall) : IO BuildContext := do let leanTrace := if lean.githash.isEmpty then mixTrace (← computeTrace lean.lean) (← computeTrace lean.sharedLib) else Hash.ofString lean.githash - return {workspace := ws, lean, lake, leanTrace} + return {opaqueWs := ws, lean, lake, leanTrace} -deriving instance Inhabited for BuildContext - -@[inline] def getWorkspace : BuildM Workspace := - (·.workspace.get) <$> read - -@[inline] def getPackageByName? (name : Name) : BuildM (Option Package) := - (·.packageByName? name) <$> getWorkspace - -@[inline] def getPackageForModule? (mod : Name) : BuildM (Option Package) := - (·.packageForModule? mod) <$> getWorkspace - -@[inline] def getOleanPath : BuildM SearchPath := - (·.oleanPath) <$> getWorkspace - -@[inline] def getLeanInstall : BuildM LeanInstall := - (·.lean) <$> read - -@[inline] def getLeanSysroot : BuildM FilePath := - (·.sysroot) <$> getLeanInstall - -@[inline] def getLeanLibDir : BuildM FilePath := - (·.libDir) <$> getLeanInstall - -@[inline] def getLeanOleanDir : BuildM FilePath := - (·.oleanDir) <$> getLeanInstall - -@[inline] def getLeanIncludeDir : BuildM FilePath := - (·.includeDir) <$> getLeanInstall - -@[inline] def getLean : BuildM FilePath := - (·.lean) <$> getLeanInstall +instance : MonadLake BuildM where + getLeanInstall := (·.lean) <$> read + getLakeInstall := (·.lake) <$> read + getWorkspace := (·.workspace) <$> read @[inline] def getLeanTrace : BuildM BuildTrace := (·.leanTrace) <$> read -@[inline] def getLeanc : BuildM FilePath := - (·.leanc) <$> getLeanInstall - -@[inline] def getLeanAr : BuildM FilePath := - (·.ar) <$> getLeanInstall - -@[inline] def getLeanCc : BuildM FilePath := - (·.cc) <$> getLeanInstall - -@[inline] def getLakeInstall : BuildM LakeInstall := - (·.lake) <$> read - -@[inline] def getLakeOleanDir : BuildM FilePath := - (·.oleanDir) <$> getLakeInstall +def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α +| Except.ok a => a +| Except.error cycle => do + let cycle := cycle.map (s!" {·}") + error s!"build cycle detected:\n{"\n".intercalate cycle}" diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index a6a5b6b479..5b2c723d24 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Build.Target -import Lake.Build.MonadBasic +import Lake.Build.Context open System namespace Lake diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 14d17dd17e..03ad8b543d 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -84,12 +84,12 @@ def getLakeInstall? : CliM (Option LakeInstall) := -- ## Complex Actions -def loadPkg (args : List String) : CliM Package := do +def loadPkg (args : List String := []) : CliM Package := do let dir ← getRootDir; let file ← getConfigFile setupLeanSearchPath (← getLeanInstall?) (← getLakeInstall?) Package.load dir args (dir / file) -def loadConfig (args : List String) : CliM (Workspace × Package) := do +def loadConfig (args : List String := []) : CliM (Workspace × Package) := do let pkg ← loadPkg args let ws ← Workspace.ofPackage pkg let packageMap ← resolveDeps ws pkg |>.run LogMethods.eio (m := IO) @@ -175,16 +175,24 @@ def longOptionOrEq (optStr : String) : CliM PUnit := -- ## Commands +def withPackage [MonadLiftT m CliM] (x : Package → LakeT m α) : CliM α := do + let (ws, pkg) ← loadConfig + let (lean, lake) ← getInstall + liftM <| x pkg |>.run {lean, lake, opaqueWs := ws} + +def withContext [MonadLiftT m CliM] (x : LakeT m α) : CliM α := + withPackage fun _ => x + /-- Run the given script from the given package with the given arguments. -/ def script (pkg : Package) (name : String) (args : List String) : CliM PUnit := do if let some script := pkg.scripts.find? name then if (← getWantsHelp) then - if let some doc := script.doc? then - IO.print doc + if let some help := script.help? then + IO.print help else error s!"no documentation provided for `{name}`" else - exit (← script.run args) + exit <| ← withContext <| script.run args else pkg.scripts.forM (m := CliM) fun name _ => do IO.println <| name.toString (escape := false) @@ -224,34 +232,18 @@ def printPaths (imports : List String := []) : CliM PUnit := do else exit noConfigFileCode -def serve (lean : LeanInstall) -(pkg : Package) (args : List String) : CliM PUnit := do - let child ← IO.Process.spawn { - cmd := lean.lean.toString, - args := #["--server"] ++ pkg.moreServerArgs ++ args - } - exit (← child.wait) +def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do + IO.Process.spawn {cmd, args, env := ← getLeanEnv} >>= (·.wait) -def env (lean : LeanInstall) (ws : Workspace) -(cmd : String) (args : Array String) : CliM PUnit := do - let child ← IO.Process.spawn { - cmd, args, - env := #[ - ("LEAN_SYSROOT", lean.sysroot.toString), - ("LEAN_AR", lean.ar.toString), - ("LEAN_CC", lean.cc.toString), - ("LEAN_PATH", ws.oleanPath.toString), - ("LEAN_SRC_PATH", ws.leanSrcPath.toString) - ] - } - exit (← child.wait) +def serve (pkg : Package) (args : Array String := #[]) : LakeT IO UInt32 := do + env (← getLean).toString <| #["--server"] ++ pkg.moreServerArgs ++ args def command : (cmd : String) → CliM PUnit | "new" => do processOptions; noArgsRem <| new (← takeArg "missing package name") | "init" => do processOptions; noArgsRem <| init (← takeArg "missing package name") -| "run" => do processOptions; noArgsRem <| script (← loadPkg []) (← takeArg "missing script") (← getSubArgs) -| "env" => do env (← getLeanInstall) (← loadConfig []).1 (← takeArg "missing command") (← takeArgs).toArray -| "serve" => do processOptions; noArgsRem <| serve (← getLeanInstall) (← loadPkg []) (← getSubArgs) +| "run" => do processOptions; noArgsRem <| script (← loadPkg) (← takeArg "missing script") (← getSubArgs) +| "env" => do exit <| ← withContext <| env (← takeArg "missing command") (← takeArgs).toArray +| "serve" => do processOptions; let args ← getSubArgs; exit <| ← noArgsRem <| withPackage fun pkg => serve pkg args.toArray | "configure" => do processOptions; let (ws, pkg) ← loadConfig (← getSubArgs); noArgsRem <| runBuildM ws pkg.buildDepOleans | "print-paths" => do processOptions; printPaths (← takeArgs) | "build" => do processOptions; let (ws, pkg) ← loadConfig (← getSubArgs); runBuildM ws <| build pkg (← takeArgs) diff --git a/Lake/Config.lean b/Lake/Config.lean index b59632f980..3d4966752f 100644 --- a/Lake/Config.lean +++ b/Lake/Config.lean @@ -8,6 +8,7 @@ import Lake.Config.InstallPath import Lake.Config.Workspace import Lake.Config.Script import Lake.Config.Package +import Lake.Config.Monad import Lake.Config.SearchPath import Lake.Config.Resolve import Lake.Config.Load diff --git a/Lake/Config/Context.lean b/Lake/Config/Context.lean new file mode 100644 index 0000000000..1b2fb6f8ab --- /dev/null +++ b/Lake/Config/Context.lean @@ -0,0 +1,28 @@ +/- +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.Task +import Lake.Config.Opaque +import Lake.Config.InstallPath +import Lake.Build.Trace +import Lake.Build.IO + +open System +namespace Lake + +/-- A Lake configuration. -/ +structure Context where + lean : LeanInstall + lake : LakeInstall + opaqueWs : OpaqueWorkspace + +/-- A transformer to equip a monad with a `Lake.Context`. -/ +abbrev LakeT := ReaderT Context + +/-- A monad equipped with a `Lake.Context`. -/ +abbrev LakeM := LakeT Id + +def LakeM.run (ctx : Context) (self : LakeM α) : α := + ReaderT.run self ctx |>.run diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index ab25db274c..319b1af2bc 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -37,7 +37,7 @@ unsafe def evalScriptDecl (env : Environment) (declName : Name) (leanOpts := Options.empty) : IO Script := do let fn ← IO.ofExcept <| Id.run <| ExceptT.run <| env.evalConstCheck ScriptFn leanOpts ``ScriptFn declName - return {fn, doc? := (← findDocString? env declName)} + return {fn, help? := (← findDocString? env declName)} namespace Package diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean new file mode 100644 index 0000000000..d2dd1f69e4 --- /dev/null +++ b/Lake/Config/Monad.lean @@ -0,0 +1,86 @@ +/- +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.Config.Context +import Lake.Config.InstallPath +import Lake.Config.Workspace + +open System +open Lean (Name) + +namespace Lake + +deriving instance Inhabited for Context + +class MonadLake (m : Type → Type u) where + getLeanInstall : m LeanInstall + getLakeInstall : m LakeInstall + getWorkspace : m Workspace + +export MonadLake (getLeanInstall getLakeInstall getWorkspace) + +instance [MonadLift m n] [MonadLake m] : MonadLake n where + getLeanInstall := liftM (m := m) <| getLeanInstall + getLakeInstall := liftM (m := m) <| getLakeInstall + getWorkspace := liftM (m := m) <| getWorkspace + +@[inline] def Context.workspace (self : Context) := + self.opaqueWs.get + +instance [Monad m] : MonadLake (LakeT m) where + getLeanInstall := (·.lean) <$> read + getLakeInstall := (·.lake) <$> read + getWorkspace := (·.workspace) <$> read + +variable [MonadLake m] + +def getLeanEnv [Monad m] : m (Array (String × Option String)) := do + let ws ← getWorkspace + let lean ← getLeanInstall + return #[ + ("LEAN_SYSROOT", lean.sysroot.toString), + ("LEAN_AR", lean.ar.toString), + ("LEAN_CC", lean.cc.toString), + ("LEAN_PATH", ws.oleanPath.toString), + ("LEAN_SRC_PATH", ws.leanSrcPath.toString) + ] + +variable [Functor m] + +@[inline] def getPackageByName? (name : Name) : m (Option Package) := + (·.packageByName? name) <$> getWorkspace + +@[inline] def getPackageForModule? (mod : Name) : m (Option Package) := + (·.packageForModule? mod) <$> getWorkspace + +@[inline] def getOleanPath : m SearchPath := + (·.oleanPath) <$> getWorkspace + +@[inline] def getLeanSysroot : m FilePath := + (·.sysroot) <$> getLeanInstall + +@[inline] def getLeanLibDir : m FilePath := + (·.libDir) <$> getLeanInstall + +@[inline] def getLeanOleanDir : m FilePath := + (·.oleanDir) <$> getLeanInstall + +@[inline] def getLeanIncludeDir : m FilePath := + (·.includeDir) <$> getLeanInstall + +@[inline] def getLean : m FilePath := + (·.lean) <$> getLeanInstall + +@[inline] def getLeanc : m FilePath := + (·.leanc) <$> getLeanInstall + +@[inline] def getLeanAr : m FilePath := + (·.ar) <$> getLeanInstall + +@[inline] def getLeanCc : m FilePath := + (·.cc) <$> getLeanInstall + +@[inline] def getLakeOleanDir : m FilePath := + (·.oleanDir) <$> getLakeInstall diff --git a/Lake/Config/Script.lean b/Lake/Config/Script.lean index a2ebb2d276..5bd39e1b80 100644 --- a/Lake/Config/Script.lean +++ b/Lake/Config/Script.lean @@ -3,10 +3,22 @@ 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.Config.Context + namespace Lake -/-- The type of a `Script`'s function. Same as that of a `main` function. -/ -abbrev ScriptFn := (args : List String) → IO UInt32 +/-- +The type of a `Script`'s monad. +`IO` equipped information about the Lake configuration. +-/ +abbrev ScriptIO := LakeT IO + +/-- +The type of a `Script`'s function. +Similar to the `main` function's signature, except that its monad is +also equipped with information about the Lake configuration. +-/ +abbrev ScriptFn := (args : List String) → ScriptIO UInt32 /-- A package `Script` is a `ScriptFn` definition that is @@ -14,8 +26,8 @@ indexed by a `String` key and can be be run by `lake run [-- ]`. -/ structure Script where fn : ScriptFn - doc? : Option String + help? : Option String deriving Inhabited -def Script.run (args : List String) (self : Script) : IO UInt32 := +def Script.run (args : List String) (self : Script) : ScriptIO UInt32 := self.fn args diff --git a/Lake/Config/Util.lean b/Lake/Config/Util.lean index e7700d5be7..6ccbf0b2dd 100644 --- a/Lake/Config/Util.lean +++ b/Lake/Config/Util.lean @@ -7,7 +7,7 @@ import Lake.Build namespace Lake -def Package.run (script : String) (args : List String) (self : Package) : IO UInt32 := +def Package.run (script : String) (args : List String) (self : Package) : ScriptIO UInt32 := if let some script := self.scripts.find? script then script.run args else do diff --git a/README.md b/README.md index cad4a7bb14..8878e3c644 100644 --- a/README.md +++ b/README.md @@ -120,7 +120,7 @@ Workspace options are shared across a package and its dependencies. ## Scripts -A configuration file can also contain a number of `scripts` declaration. A script is an arbitrary `(args : List String) → IO UInt32` definition that can be run by `lake run