max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: split Lake context from BuildContext and also use it in scripts

Browse source
This commit is contained in:
tydeu 2021-12-22 00:39:36 -05:00
parent 1b96c466ca
commit d4e7e33652
11 changed files with 175 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
Lake/Build/MonadBasic.lean → Lake/Build/Context.lean
View file

@ -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}"

63
Lake/Build/Monad.lean
View file

@ -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}"

2
Lake/Build/TargetTypes.lean
View file

@ -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

48
Lake/CLI/Main.lean
View file

@ -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)

1
Lake/Config.lean
View file

@ -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

28
Lake/Config/Context.lean Normal file
View file

@ -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

2
Lake/Config/Load.lean
View file

@ -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

86
Lake/Config/Monad.lean Normal file
View file

@ -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

20
Lake/Config/Script.lean
View file

@ -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 <key> [-- <args>]`.
-/
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

2
Lake/Config/Util.lean
View file

@ -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

2
README.md
View file

@ -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 <script> [-- <args>]`. For example, given the following `lakefile.lean`:
A configuration file can also contain a number of `scripts` declaration. A script is an arbitrary `(args : List String) → ScriptIO UInt32` definition that can be run by `lake run <script> [-- <args>]`. For example, given the following `lakefile.lean`:
```lean
import Lake