diff --git a/Lake/Build/Binary.lean b/Lake/Build/Binary.lean
index d64b92ebfb..241421de8b 100644
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Binary.lean
@@ -33,9 +33,8 @@ def Package.moduleOTarget (mod : Name) (self : Package) : FileTarget :=
 
 protected def Package.staticLibTarget (self : Package) : FileTarget :=
  Target.mk self.staticLibFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap (← self.getModuleArray) $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let moduleTargetMap ← self.buildModuleMap $
+      recBuildModuleOleanAndCTargetWithLocalImports
     let oFileTargets := self.oFileTargetsOf moduleTargetMap
     staticLibTarget self.staticLibFile oFileTargets |>.materializeAsync
 
@@ -59,9 +58,8 @@ def Package.linkTargetsOf
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
   Target.mk self.sharedLibFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap (← self.getModuleArray) $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let moduleTargetMap ← self.buildModuleMap $
+      recBuildModuleOleanAndCTargetWithLocalImports
     let linkTargets ← self.linkTargetsOf moduleTargetMap
     let target := leanSharedLibTarget self.sharedLibFile linkTargets self.moreLinkArgs
     target.materializeAsync
@@ -74,7 +72,7 @@ def Package.buildSharedLib (self : Package) : BuildM FilePath :=
 protected def Package.binTarget (self : Package) : FileTarget :=
   Target.mk self.binFile do
     let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleTargetMap #[self.binRoot] $
+    let moduleTargetMap ← buildModuleMap #[⟨self, self.binRoot⟩] $
       recBuildModuleOleanAndCTargetWithLocalImports depTarget
     let pkgLinkTargets ← self.linkTargetsOf moduleTargetMap
     let linkTargets :=
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index fcc7c91175..5944b02a91 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -140,6 +140,13 @@ protected def Package.moduleOleanTargetOnly (self : Package)
 
 -- # Recursive Building
 
+structure ModuleInfo where
+  pkg : Package
+  name : Name
+
+def ModuleInfo.srcFile (self : ModuleInfo) : FilePath :=
+  self.pkg.modToSrc self.name
+
 /-
 Produces a recursive module target builder that
 builds the target module after recursively building its local imports
@@ -147,37 +154,35 @@ builds the target module after recursively building its local imports
 -/
 def recBuildModuleWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m]
-(build : Name → FilePath → String → List α → BuildM α)
-: RecBuild Name α m := fun mod recurse => do
+(build : Package → Name → FilePath → String → List α → BuildM α)
+: RecBuild ModuleInfo α m := fun info recurse => do
   have : MonadLift BuildM m := ⟨liftM⟩
   have : MonadFunctor BuildM m := ⟨fun f => monadMap (m := BuildM) f⟩
-  let pkg ← getPackage
-  let leanFile := pkg.modToSrc mod
-  let contents ← IO.FS.readFile leanFile
-  let (imports, _, _) ← Elab.parseImports contents leanFile.toString
+  let contents ← IO.FS.readFile info.srcFile
+  let (imports, _, _) ← Elab.parseImports contents info.srcFile.toString
   -- we construct the import targets even if a rebuild is not required
   -- because other build processes (ex. `.o`) rely on the map being complete
   let importTargets ← imports.filterMapM fun imp => OptionT.run do
     let mod := imp.module
     let pkg ← OptionT.mk <| getPackageForModule? mod
-    adaptPackage pkg <| recurse mod
-  build mod leanFile contents importTargets
+    adaptPackage pkg <| recurse ⟨pkg, mod⟩
+  adaptPackage info.pkg <| build info.pkg info.name info.srcFile contents importTargets
 
 def recBuildModuleOleanAndCTargetWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Name ActiveOleanAndCTarget m :=
-  recBuildModuleWithLocalImports fun mod leanFile contents importTargets => do
+: RecBuild ModuleInfo ActiveOleanAndCTarget m :=
+  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
     let importTarget ← ActiveTarget.collectOpaqueList <| importTargets.map (·.oleanTarget)
     let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    (← getPackage).moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run'
+    pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run'
 
 def recBuildModuleOleanTargetWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Name ActiveFileTarget m :=
-  recBuildModuleWithLocalImports fun mod leanFile contents importTargets => do
+: RecBuild ModuleInfo ActiveFileTarget m :=
+  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
     let importTarget ← ActiveTarget.collectOpaqueList importTargets
     let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    (← getPackage).moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run
+    pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run
 
 -- ## Definitions
 
@@ -187,19 +192,36 @@ abbrev ModuleBuildM (α) :=
   EStateT (List Name) (NameMap α) BuildM
 
 abbrev RecModuleBuild (o) :=
-  RecBuild Name o (ModuleBuildM o)
+  RecBuild ModuleInfo o (ModuleBuildM o)
 
 abbrev RecModuleTargetBuild (i) :=
   RecModuleBuild (ActiveBuildTarget i)
 
 -- ## Builders
 
-def buildModule (mod : Name)
+/-- Build a single module using the recursive module build function `build`. -/
+def buildModule (mod : ModuleInfo)
 [Inhabited o] (build : RecModuleBuild o) : BuildM o := do
   failOnBuildCycle <| ← RBTopT.run' do
-    buildRBTop (cmp := Name.quickCmp) build id mod
+    buildRBTop (cmp := Name.quickCmp) build ModuleInfo.name mod
 
-def buildModules (mods : Array Name)
+/--
+Build each module using the recursive module function `build`,
+constructing an `Array`  of the results.
+-/
+def buildModuleArray (mods : Array ModuleInfo)
 [Inhabited o] (build : RecModuleBuild o) : BuildM (Array o) := do
   failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <|
-    buildRBTop (cmp := Name.quickCmp) build id
+    buildRBTop (cmp := Name.quickCmp) build ModuleInfo.name
+
+/--
+Build each module using the recursive module function `build`,
+constructing a module-target `NameMap`  of the results.
+-/
+def buildModuleMap [Inhabited o]
+(infos : Array ModuleInfo) (build : RecModuleBuild o)
+: BuildM (NameMap o) := do
+  let (x, objMap) ← RBTopT.run do
+    infos.forM fun info => discard <| buildRBTop build ModuleInfo.name info
+  failOnBuildCycle x
+  return objMap
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index 7c511c5cb9..f14bc72093 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -34,42 +34,42 @@ def buildExtraDepsTarget : BuildM ActiveOpaqueTarget := do
   ActiveTarget.collectOpaqueArray <| ← do
     (← getWorkspace).packageArray.mapM (·.extraDepTarget.run)
 
-/--
-Build each module and using the given recursive module build function,
-constructing a module-target `NameMap`  of the results.
--/
-def buildModuleTargetMap [Inhabited i]
-(mods : Array Name) (build : RecModuleTargetBuild i)
-: BuildM (NameMap (ActiveBuildTarget i)) := do
-  let (x, targetMap) ← RBTopT.run do
-    mods.forM fun mod => discard <| buildRBTop build id mod
-  failOnBuildCycle x
-  return targetMap
-
-/--
-Build each module and using the given recursive module build function,
-constructing a single opaque target for the whole build.
--/
-def buildModulesTarget [Inhabited i] (mods : Array Name)
-(build : RecModuleTargetBuild i) : BuildM ActiveOpaqueTarget := do
-  failOnBuildCycle <| ← RBTopT.run' do
-    let targets ← mods.mapM fun mod =>
-      (·.withoutInfo) <$> buildRBTop build id mod
-    ActiveTarget.collectOpaqueArray targets
-
 -- # Build Package Modules
 
-/-- Build the `.olean` and files of package and its dependencies' modules. -/
-def Package.buildOleanTarget (self : Package) : BuildM ActiveOpaqueTarget := do
+/--
+Build the `extraDepTarget` of a package and its (transitive) dependencies
+and then build their modules recursively using the given `build` function,
+constructing a `NameMap` of the results.
+-/
+protected def Package.buildModuleMap [Inhabited o]
+(build : ActiveOpaqueTarget → RecModuleBuild o) (self : Package)
+: BuildM (NameMap o) := do
   let depTarget ← self.buildExtraDepsTarget
-  buildModulesTarget (← self.getModuleArray) <|
-    recBuildModuleOleanTargetWithLocalImports depTarget
+  let infos := (← self.getModuleArray).map fun mod => ModuleInfo.mk self mod
+  buildModuleMap infos (build depTarget)
+
+/--
+Build the `extraDepTarget` of a package and its (transitive) dependencies
+and then build their modules recursively using the given `build` function,
+constructing a single opaque target for the whole build.
+-/
+def Package.buildTarget [Inhabited i]
+(build : ActiveOpaqueTarget → RecModuleTargetBuild i) (self : Package)
+: BuildM ActiveOpaqueTarget := do
+  let depTarget ← self.buildExtraDepsTarget
+  let mods ← self.getModuleArray
+  failOnBuildCycle <| ← RBTopT.run' do
+    let targets ← mods.mapM fun mod => (·.withoutInfo) <$>
+      buildRBTop (build depTarget) ModuleInfo.name (ModuleInfo.mk self mod)
+    ActiveTarget.collectOpaqueArray targets
+
+/-- Build the `.olean` files of package and its dependencies' modules. -/
+def Package.buildOleanTarget (self : Package) : BuildM ActiveOpaqueTarget := do
+  self.buildTarget <| recBuildModuleOleanTargetWithLocalImports
 
 /-- Build the `.olean` and `.c` files of package and its dependencies' modules. -/
 def Package.buildOleanAndCTarget (self : Package) : BuildM ActiveOpaqueTarget := do
-  let depTarget ← self.buildExtraDepsTarget
-  buildModulesTarget (← self.getModuleArray) <|
-    recBuildModuleOleanAndCTargetWithLocalImports depTarget
+  self.buildTarget <| recBuildModuleOleanAndCTargetWithLocalImports
 
 def Package.buildDepOleans (self : Package) : BuildM PUnit := do
   let targets ← self.dependencies.mapM fun dep => do
@@ -88,24 +88,27 @@ def Package.moduleOleanTarget (mod : Name) (self : Package) : FileTarget :=
   Target.mk (self.modToOlean mod) do
     let depTarget ← self.buildExtraDepsTarget
     let build := recBuildModuleOleanTargetWithLocalImports depTarget
-    return (← buildModule mod build).task
+    return (← buildModule ⟨self, mod⟩ build).task
 
 def Package.moduleOleanAndCTarget (mod : Name) (self : Package) : OleanAndCTarget :=
   Target.mk ⟨self.modToOlean mod, self.modToC mod⟩ do
     let depTarget ← self.buildExtraDepsTarget
     let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-    return (← buildModule mod build).task
+    return (← buildModule ⟨self, mod⟩ build).task
 
 -- # Build Imports
 
-/-- Pick the local imports of the workspace from a list of import strings. -/
-def Workspace.filterLocalImports
-(imports : List String) (self : Workspace) : Array Name := Id.run <| do
+/--
+Construct an `Array` of `ModuleInfo`s for the workspace-local modules of
+a `List` of import strings.
+-/
+def Workspace.processImportList
+(imports : List String) (self : Workspace) : Array ModuleInfo := Id.run do
   let mut localImports := #[]
   for imp in imports do
-    let impName := imp.toName
-    if self.isLocalModule impName then
-      localImports := localImports.push impName
+    let mod := imp.toName
+    if let some pkg := self.packageForModule? mod then
+      localImports := localImports.push ⟨pkg, mod⟩
   return localImports
 
 /--
@@ -115,18 +118,19 @@ Builds only module `.olean` files if the default package facet is
 just `oleans`. Otherwise, builds both `.olean` and `.c` files.
 -/
 def buildImportsAndDeps (imports : List String := []) : BuildM PUnit := do
-  let depTarget ← buildExtraDepsTarget
+  let pkg ← getPackage
+  let depTarget ← pkg.buildExtraDepsTarget
   if imports.isEmpty then
     -- wait for deps to finish building
     depTarget.build
   else
     -- build local imports from list
-    let localImports := (← getWorkspace).filterLocalImports imports
-    if (← getPackage).defaultFacet == PackageFacet.oleans then
+    let infos := (← getWorkspace).processImportList imports
+    if pkg.defaultFacet == PackageFacet.oleans then
       let build := recBuildModuleOleanTargetWithLocalImports depTarget
-      let targets ← buildModules localImports build
+      let targets ← buildModuleArray infos build
       targets.forM (·.build)
     else
       let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-      let targets ← buildModules localImports build
+      let targets ← buildModuleArray infos build
       targets.forM (·.build)
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 7ac964d9d7..75a8869272 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -34,34 +34,34 @@ def parseTargetBaseSpec (ws : Workspace) (rootPkg : Package) (spec : String) : I
   | _ =>
     error s!"invalid target spec '{spec}' (too many '/')"
 
-def parseTargetSpec (ws : Workspace) (rootPkg : Package) (spec : String) : IO (Package × OpaqueTarget) := do
+def parseTargetSpec (ws : Workspace) (rootPkg : Package) (spec : String) : IO (BuildTarget Package) := do
   match spec.splitOn ":" with
   | [rootSpec] =>
     let (pkg, mod?) ← parseTargetBaseSpec ws rootPkg rootSpec
     if let some mod := mod? then
-      return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
+      return pkg.moduleOleanTarget mod |>.withInfo pkg
     else
-      return (pkg, pkg.defaultTarget)
+      return pkg.defaultTarget |>.withInfo pkg
   | [rootSpec, facet] =>
     let (pkg, mod?) ← parseTargetBaseSpec ws rootPkg rootSpec
     if let some mod := mod? then
       if facet == "olean" then
-        return (pkg, pkg.moduleOleanTarget mod |>.withoutInfo)
+        return pkg.moduleOleanTarget mod |>.withInfo pkg
       else if facet == "c" then
-        return (pkg, pkg.moduleOleanAndCTarget mod |>.withoutInfo)
+        return pkg.moduleOleanAndCTarget mod |>.withInfo pkg
       else if facet == "o" then
-        return (pkg, pkg.moduleOTarget mod |>.withoutInfo)
+        return pkg.moduleOTarget mod |>.withInfo pkg
       else
         error s!"unknown module facet '{facet}'"
     else
       if facet == "bin" then
-        return (pkg, pkg.binTarget.withoutInfo)
+        return pkg.binTarget.withInfo pkg
       else if facet == "staticLib" then
-        return (pkg, pkg.staticLibTarget.withoutInfo)
+        return pkg.staticLibTarget.withInfo pkg
       else if facet == "sharedLib" then
-        return (pkg, pkg.sharedLibTarget.withoutInfo)
+        return pkg.sharedLibTarget.withInfo pkg
       else if facet == "oleans" then
-        return (pkg, pkg.oleanTarget.withoutInfo)
+        return pkg.oleanTarget.withInfo pkg
       else
         error s!"unknown package facet '{facet}'"
   | _ =>
@@ -73,4 +73,4 @@ def build (targetSpecs : List String) : BuildM PUnit := do
   if targets.isEmpty then
     pkg.defaultTarget.build
   else
-    targets.forM fun (pkg, t) => adaptPackage pkg <| t.build
+    targets.forM fun t => adaptPackage t.info <| discard <| t.build