feat: store current Package in BuildM

Lake/Build/Monad.lean

@@ -3,30 +3,30 @@ 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.Build.Trace
-import Lake.Util.LogT
-import Lake.Config.InstallPath
+import Lake.Config.Package
+import Lake.Build.MonadBasic
 
 open System
 namespace Lake
 
---------------------------------------------------------------------------------
--- # Build Monad Definition
---------------------------------------------------------------------------------
+deriving instance Inhabited for BuildContext
 
-structure BuildContext where
-  leanTrace : BuildTrace
-  leanInstall : LeanInstall
-  lakeInstall : LakeInstall
-  deriving Inhabited
+def BuildM.adaptPackage (pkg : Package) (self : BuildM α) : BuildM α :=
+  self.adapt fun r => {r with package := pkg}
 
-abbrev BuildCoreM := LogMethodsT BaseIO <| EIO PUnit
-abbrev BuildM := ReaderT BuildContext BuildCoreM
+export BuildM (adaptPackage)
 
---------------------------------------------------------------------------------
--- # Build Monad Utilities
---------------------------------------------------------------------------------
+def getPackage : BuildM Package :=
+  (·.package.get) <$> read
+
+def getWorkspace : BuildM Workspace :=
+  (·.workspace) <$> getPackage
+
+def getBuildDir : BuildM FilePath :=
+  (·.buildDir) <$> getPackage
+
+def getOleanDir : BuildM FilePath :=
+  (·.oleanDir) <$> getPackage
 
 def getLeanInstall : BuildM LeanInstall :=
   (·.leanInstall) <$> read
@@ -45,48 +45,3 @@ def getLeanc : BuildM FilePath :=
 
 def getLakeInstall : BuildM LakeInstall :=
   (·.lakeInstall) <$> read
-
-namespace BuildCoreM
-
-def run (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : IO α :=
-  ReaderT.run self logMethods |>.toIO fun _ => IO.userError "build failed"
-
-def runWith (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : EIO PUnit α :=
-  ReaderT.run self logMethods
-
-protected def failure : BuildCoreM α :=
-  throw ()
-
-protected def orElse (self : BuildCoreM α) (f : Unit → BuildCoreM α) : BuildCoreM α :=
-  tryCatch self f
-
-instance : Alternative BuildCoreM where
-  failure := BuildCoreM.failure
-  orElse := BuildCoreM.orElse
-
-def runIO (x : IO α) : BuildCoreM α := do
-  match (← x.toBaseIO) with
-  | Except.ok a => pure a
-  | Except.error e => do
-    logError (toString e)
-    failure
-
-instance : MonadLift IO BuildCoreM := ⟨runIO⟩
-
-instance : MonadLift (LogT IO) BuildCoreM where
-  monadLift x := fun meths => runIO (x.run meths.lift) meths
-
-end BuildCoreM
-
-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!"  {·}")
-  logError s!"build cycle detected:\n{"\n".intercalate cycle}"
-  failure
-
-/-- `Task` type for `BuildM`/`BuildCoreM`. -/
-abbrev BuildTask := EIOTask PUnit

Lake/Build/MonadBasic.lean

@@ -0,0 +1,36 @@
+/-
+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.Build.Trace
+import Lake.Build.MonadCore
+import Lake.Config.InstallPath
+import Lake.Config.OpaquePackage
+
+open System
+namespace Lake
+
+structure BuildContext where
+  leanTrace : BuildTrace
+  leanInstall : LeanInstall
+  lakeInstall : LakeInstall
+  package : OpaquePackage
+
+abbrev BuildM :=
+  ReaderT BuildContext BuildCoreM
+
+/-- `Task` type for `BuildM`/`BuildCoreM`. -/
+abbrev BuildTask :=
+  EIOTask PUnit
+
+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!"  {·}")
+  logError s!"build cycle detected:\n{"\n".intercalate cycle}"
+  failure

Lake/Build/MonadCore.lean

@@ -0,0 +1,41 @@
+/-
+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.LogT
+
+namespace Lake
+
+abbrev BuildCoreM :=
+  LogMethodsT BaseIO <| EIO PUnit
+
+namespace BuildCoreM
+
+def run (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : IO α :=
+  ReaderT.run self logMethods |>.toIO fun _ => IO.userError "build failed"
+
+def runWith (logMethods : LogMethods BaseIO) (self : BuildCoreM α) : EIO PUnit α :=
+  ReaderT.run self logMethods
+
+protected def failure : BuildCoreM α :=
+  throw ()
+
+protected def orElse (self : BuildCoreM α) (f : Unit → BuildCoreM α) : BuildCoreM α :=
+  tryCatch self f
+
+instance : Alternative BuildCoreM where
+  failure := BuildCoreM.failure
+  orElse := BuildCoreM.orElse
+
+def runIO (x : IO α) : BuildCoreM α := do
+  match (← x.toBaseIO) with
+  | Except.ok a => pure a
+  | Except.error e => do
+    logError (toString e)
+    failure
+
+instance : MonadLift IO BuildCoreM := ⟨runIO⟩
+
+instance : MonadLift (LogT IO) BuildCoreM where
+  monadLift x := fun meths => runIO (x.run meths.lift) meths

Lake/Build/Package.lean

@@ -73,7 +73,7 @@ def recBuildPackageWithDeps
         let depPkg ← liftM (m := BuildM) <| resolveDep pkg dep
         buildPkg depPkg
     depTargets := depTargets ++ targets
-  let pkgTarget ← build depTargets pkg
+  let pkgTarget ← adaptPackage pkg <| build depTargets pkg
   depTargets.push pkgTarget
 
 /--

Lake/Build/TargetTypes.lean

@@ -3,8 +3,8 @@ 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.Build.Monad
 import Lake.Build.Target
+import Lake.Build.MonadBasic
 
 open System
 namespace Lake

Lake/CLI/Main.lean

@@ -133,14 +133,14 @@ def getInstall : CliM (LeanInstall × LakeInstall) := do
   return (← getLeanInstall, ← getLakeInstall)
 
 /-- Perform the given build action using information from CLI. -/
-def runBuildM (x : BuildM α) : CliM α := do
+def runBuildM (pkg : Package) (x : BuildM α) : CliM α := do
   let (leanInstall, lakeInstall) ← getInstall
   let leanTrace ← computeTrace leanInstall.lean
-  x.run LogMethods.io {leanTrace, leanInstall, lakeInstall}
+  x.run LogMethods.io {leanTrace, leanInstall, lakeInstall, package := pkg}
 
 /-- Variant of `runBuildM` that discards the build monad's output. -/
-def runBuildM_ (x : BuildM α) : CliM PUnit :=
-  discard <| runBuildM x
+def runBuildM_  (pkg : Package) (x : BuildM α) : CliM PUnit :=
+  discard <| runBuildM pkg x
 
 -- ## Argument Parsing
 
@@ -251,7 +251,7 @@ def printPaths (imports : List String := []) : CliM PUnit := do
     let pkg ← loadPkg (← getSubArgs)
     let leanTrace ← computeTrace leanInstall.lean
     let pkgs ← pkg.buildImportsAndDeps imports |>.run LogMethods.eio {
-      leanTrace, leanInstall, lakeInstall
+      leanTrace, leanInstall, lakeInstall, package := pkg
     }
     IO.println <| Json.compress <| toJson {
       oleanPath := pkgs.map (·.oleanDir),
@@ -285,34 +285,34 @@ def parseTargetBaseSpec (rootPkg : Package) (spec : String) : CliM (Package × O
   | _ =>
     error s!"invalid target spec '{spec}' (too many '/')"
 
-partial def parseTargetSpec (rootPkg : Package) (spec : String) : CliM OpaqueTarget := do
+partial def parseTargetSpec (rootPkg : Package) (spec : String) : CliM (Package × OpaqueTarget) := do
   match spec.splitOn ":" with
   | [rootSpec] =>
     let (pkg, mod?) ← parseTargetBaseSpec rootPkg rootSpec
     if let some mod := mod? then
-      return pkg.moduleOleanTarget mod |>.withoutInfo
+      return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
     else
-      return pkg.defaultTarget
+      return (pkg, pkg.defaultTarget)
   | [rootSpec, facet] =>
     let (pkg, mod?) ← parseTargetBaseSpec rootPkg rootSpec
     if let some mod := mod? then
       if facet == "olean" then
-        return pkg.moduleOleanTarget mod |>.withoutInfo
+        return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
       else if facet == "c" then
-        return pkg.moduleOleanAndCTarget mod |>.withoutInfo
+        return (pkg, pkg.moduleOleanAndCTarget mod |>.withoutInfo)
       else if facet == "o" then
-        return pkg.moduleOTarget mod |>.withoutInfo
+        return (pkg, pkg.moduleOTarget mod |>.withoutInfo)
       else
         error s!"unknown module facet '{facet}'"
     else
       if facet == "bin" then
-        return pkg.binTarget.withoutInfo
+        return (pkg, pkg.binTarget.withoutInfo)
       else if facet == "staticLib" then
-        return pkg.staticLibTarget.withoutInfo
+        return (pkg, pkg.staticLibTarget.withoutInfo)
       else if facet == "sharedLib" then
-        return pkg.sharedLibTarget.withoutInfo
+        return (pkg, pkg.sharedLibTarget.withoutInfo)
       else if facet == "oleans" then
-        return pkg.oleanTarget.withoutInfo
+        return (pkg, pkg.oleanTarget.withoutInfo)
       else
         error s!"unknown package facet '{facet}'"
   | _ =>
@@ -321,9 +321,9 @@ partial def parseTargetSpec (rootPkg : Package) (spec : String) : CliM OpaqueTar
 def build (rootPkg : Package) (targetSpecs : List String) : CliM PUnit := do
   let targets ← targetSpecs.mapM (parseTargetSpec rootPkg)
   if targets.isEmpty then
-    runBuildM rootPkg.defaultTarget.build
+    runBuildM rootPkg rootPkg.defaultTarget.build
   else
-    runBuildM <| targets.forM (·.build)
+    runBuildM rootPkg <| targets.forM fun (pkg, t) => adaptPackage pkg <| t.build
 
 def server (leanInstall : LeanInstall) (pkg : Package) (args : List String) : CliM PUnit := do
   let child ← IO.Process.spawn {
@@ -332,12 +332,15 @@ def server (leanInstall : LeanInstall) (pkg : Package) (args : List String) : Cl
   }
   exit (← child.wait)
 
+def configure (pkg : Package) : CliM PUnit := do
+  runBuildM pkg pkg.buildDepOleans
+
 def command : (cmd : String) → CliM PUnit
 | "new"         => do noArgsRem <| new (← takeArg)
 | "init"        => do noArgsRem <| init (← takeArg)
 | "run"         => do noArgsRem <| script (← loadPkg []) (← takeArg) (← getSubArgs)
 | "server"      => do noArgsRem <| server (← getLeanInstall) (← loadPkg []) (← getSubArgs)
-| "configure"   => do noArgsRem <| runBuildM (← loadPkg (← getSubArgs)).buildDepOleans
+| "configure"   => do noArgsRem <| configure (← loadPkg (← getSubArgs))
 | "print-paths" => do printPaths (← takeArgs)
 | "build"       => do build (← loadPkg (← getSubArgs)) (← takeArgs)
 | "clean"       => do noArgsRem <| (← loadPkg (← getSubArgs)).clean

Lake/Config/OpaquePackage.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
+
+constant OpaquePackagePointed : PointedType.{0}
+
+/-- Opaque reference to a `Package` used for forward declaration. -/
+def OpaquePackage : Type := OpaquePackagePointed.type

Lake/Config/Package.lean

@@ -9,6 +9,7 @@ import Std.Data.HashMap
 import Lake.LeanVersion
 import Lake.Build.TargetTypes
 import Lake.Config.Glob
+import Lake.Config.OpaquePackage
 import Lake.Config.Workspace
 import Lake.Config.Script
 
@@ -295,6 +296,28 @@ structure Package where
   scripts : NameMap Script := {}
   deriving Inhabited
 
+namespace OpaquePackage
+
+unsafe def unsafeMk (pkg : Package) : OpaquePackage :=
+  unsafeCast pkg
+
+@[implementedBy unsafeMk] constant mk (pkg : Package) : OpaquePackage :=
+  OpaquePackagePointed.val
+
+instance : Coe Package OpaquePackage := ⟨mk⟩
+instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
+
+unsafe def unsafeGet (self : OpaquePackage) : Package :=
+  unsafeCast self
+
+@[implementedBy unsafeGet] constant get (self : OpaquePackage) : Package
+
+instance : Coe OpaquePackage Package := ⟨get⟩
+
+@[simp] axiom get_mk {pkg : Package} : get (mk pkg) = pkg
+
+end OpaquePackage
+
 /--
   An alternate signature for package configurations
   that permits more dynamic configurations, but is still pure.