From 02ee011a0ef10d591908f5148dd94702e68c6648 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 16 Jun 2022 01:31:51 -0400
Subject: [PATCH] refactor: simplify module target code + related cleanup

closes leanprover/lake#75
---
 Lake/Build/Binary.lean      |  57 ++++----
 Lake/Build/Context.lean     |   3 +
 Lake/Build/Module.lean      | 263 +++++++++++-------------------------
 Lake/Build/Package.lean     |  62 +++++----
 Lake/Build/Recursive.lean   |   5 -
 Lake/Build/TargetTypes.lean |   8 +-
 Lake/Build/Targets.lean     |   4 +-
 Lake/CLI/Build.lean         |  46 +++----
 Lake/Config.lean            |   1 +
 Lake/Config/Module.lean     |  66 +++++++++
 Lake/Config/Monad.lean      |   8 +-
 Lake/Config/Package.lean    |  47 +------
 Lake/Config/Resolve.lean    |   4 +-
 Lake/Config/Targets.lean    |   4 +-
 Lake/Config/Workspace.lean  |  13 +-
 examples/targets/test.sh    |   6 +
 16 files changed, 266 insertions(+), 331 deletions(-)
 create mode 100644 Lake/Config/Module.lean

diff --git a/Lake/Build/Binary.lean b/Lake/Build/Binary.lean
index 4c4a6434b1..69692e549c 100644
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Binary.lean
@@ -13,21 +13,21 @@ namespace Lake
 
 -- # Build Package .o Files
 
-def Package.oFileTargetOf
-(mod : Name) (target : ActiveOleanAndCTarget) (self : Package) : FileTarget :=
-  let oFile := self.modToO mod
-  let cTarget := Target.active <| ActiveOleanAndCTarget.cTarget target
-  leanOFileTarget oFile cTarget self.moreLeancArgs
-
 def Package.oFileTargetsOf
-(targetMap : NameMap ActiveOleanAndCTarget) (self : Package) : Array FileTarget :=
-  targetMap.fold (fun arr k v => arr.push (k, v)) #[] |>.filterMap fun (mod, target) =>
-    if self.isLocalModule mod then self.oFileTargetOf mod target else none
+(targetMap : ModuleMap ActiveOpaqueTarget) (self : Package) : Array FileTarget :=
+  targetMap.fold (fun arr k v => arr.push (k, v)) #[] |>.filterMap fun (key, target) =>
+    if key.facet == `lean.c && self.isLocalModule key.module then
+      let mod : Module := ⟨self, key.module⟩
+      let target := Target.active <| target.withInfo mod.cFile
+      leanOFileTarget mod.oFile target self.moreLeancArgs
+    else
+      none
 
-def Package.moduleOTarget (mod : Name) (self : Package) : FileTarget :=
-  let oFile := self.modToO mod
-  let cTarget := self.moduleOleanAndCTarget mod |>.cTarget
-  leanOFileTarget oFile cTarget self.moreLeancArgs
+def Module.mkOTarget (modTarget : OpaqueTarget) (self : Module) : FileTarget :=
+  leanOFileTarget self.oFile (self.mkCTarget modTarget) self.leancArgs
+
+def Module.oTarget (self : Module) : FileTarget :=
+  self.mkOTarget <| self.leanBinTarget (c := true)
 
 -- # Build Package Static Lib
 
@@ -35,9 +35,9 @@ def Package.mkStaticLibTarget (self : Package) (lib : LeanLibConfig) : FileTarge
   let libFile := self.libDir / lib.staticLibFileName
   BuildTarget.mk' libFile do
     let depTarget ← self.buildExtraDepsTarget
-    let infos := (← lib.getModuleArray self.srcDir).map (Module.mk self)
-    let moduleTargetMap ← buildModuleMap infos $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let mods ← self.getLibModuleArray lib
+    let moduleTargetMap ← buildModuleMap mods $
+      recBuildModuleTargetWithDeps depTarget (c := true)
     let oFileTargets := self.oFileTargetsOf moduleTargetMap
     staticLibTarget libFile oFileTargets |>.materializeAsync
 
@@ -47,13 +47,13 @@ protected def Package.staticLibTarget (self : Package) : FileTarget :=
 -- # Build Package Shared Lib
 
 def Package.linkTargetsOf
-(targetMap : NameMap ActiveOleanAndCTarget) (self : Package) : LakeM (Array FileTarget) := do
+(targetMap : ModuleMap ActiveOpaqueTarget) (self : Package) : LakeM (Array FileTarget) := do
   let collect dep recurse := do
-      let pkg := (← getPackageByName? dep.name).get!
+      let pkg := (← findPackage? dep.name).get!
       pkg.dependencies.forM fun dep => discard <| recurse dep
       return pkg.oFileTargetsOf targetMap ++ pkg.externLibTargets
-  let ⟨x, map⟩ ← RBTopT.run <| self.dependencies.forM fun dep =>
-    discard <| buildRBTop (cmp := Name.quickCmp) collect Dependency.name dep
+  let ⟨x, map⟩ ← RBTopT.run (cmp := Name.quickCmp) <| self.dependencies.forM fun dep =>
+    discard <| buildTop collect Dependency.name dep
   match x with
   | Except.ok _ =>
     let ts := map.fold (fun acc _ vs => acc ++ vs) #[]
@@ -64,9 +64,9 @@ def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarge
   let libFile := self.libDir / lib.sharedLibFileName
   BuildTarget.mk' libFile do
     let depTarget ← self.buildExtraDepsTarget
-    let infos := (← lib.getModuleArray self.srcDir).map (Module.mk self)
-    let moduleTargetMap ← buildModuleMap infos $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let mods ← self.getLibModuleArray lib
+    let moduleTargetMap ← buildModuleMap mods $
+      recBuildModuleTargetWithDeps depTarget (c := true)
     let linkTargets ← self.linkTargetsOf moduleTargetMap
     let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
     target.materializeAsync
@@ -79,18 +79,19 @@ protected def Package.sharedLibTarget (self : Package) : FileTarget :=
 def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
   let exeFile := self.binDir / exe.fileName
   BuildTarget.mk' exeFile do
+    let root : Module := ⟨self, exe.root⟩
     let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleMap #[⟨self, exe.root⟩] $
-      recBuildModuleOleanAndCTargetWithLocalImports depTarget
+    let moduleTargetMap ← buildModuleMap #[root] $
+      recBuildModuleTargetWithDeps depTarget (c := true)
     let pkgLinkTargets ← self.linkTargetsOf moduleTargetMap
     let linkTargets :=
       if self.isLocalModule exe.root then
         pkgLinkTargets
       else
-        let rootTarget := moduleTargetMap.find? exe.root |>.get!
-        let rootLinkTarget := self.oFileTargetOf exe.root rootTarget
+        let rootTarget := moduleTargetMap.find? (root.key `lean) |>.get!
+        let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
         #[rootLinkTarget] ++ pkgLinkTargets
-    let target := leanBinTarget exeFile linkTargets exe.linkArgs
+    let target := leanExeTarget exeFile linkTargets exe.linkArgs
     target.materializeAsync
 
 protected def Package.exeTarget (self : Package) : FileTarget :=
diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean
index 7efacd48fd..c8a8086a2a 100644
--- a/Lake/Build/Context.lean
+++ b/Lake/Build/Context.lean
@@ -29,6 +29,9 @@ abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO
 /-- The `Task` monad for Lake builds. -/
 abbrev BuildTask := OptionIOTask
 
+/-- A Lake build job. -/
+abbrev Job := BuildTask BuildTrace
+
 instance : MonadError BuildM := ⟨MonadLog.error⟩
 instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩
 
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index b2512940da..5677f5fa72 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -9,224 +9,120 @@ import Lake.Build.Target
 import Lake.Build.Actions
 import Lake.Build.Recursive
 import Lake.Build.TargetTypes
-import Lake.Config.Package
+import Lake.Config.Module
 
 open System
 open Lean hiding SearchPath
 
 namespace Lake
 
--- # Info
+-- # Build Key
 
-structure Module where
-  pkg : Package
-  name : Name
-  deriving Inhabited
+structure ModuleBuildKey where
+  module : Name
+  facet : Name
+  deriving Inhabited, Repr, BEq, Hashable
 
-namespace Module
+namespace ModuleBuildKey
 
-@[inline] def srcFile (self : Module) : FilePath :=
-  self.pkg.modToSrc self.name
+def quickCmp (lhs rhs : ModuleBuildKey) :=
+  match lhs.module.quickCmp rhs.module with
+  | .eq => lhs.facet.quickCmp rhs.facet
+  | ord => ord
 
-@[inline] def oleanFile (self : Module) : FilePath :=
-  self.pkg.modToOlean self.name
+protected def toString (self : ModuleBuildKey) :=
+  s!"{self.module}:{self.facet}"
 
-@[inline] def ileanFile (self : Module) : FilePath :=
-  self.pkg.modToIlean self.name
+instance : ToString ModuleBuildKey := ⟨(·.toString)⟩
 
-@[inline] def cFile (self : Module) : FilePath :=
-  self.pkg.modToC self.name
+end ModuleBuildKey
 
-@[inline] def traceFile (self : Module) : FilePath :=
-  self.pkg.modToTraceFile self.name
+def Module.key (facet : Name) (self : Module) : ModuleBuildKey :=
+  ⟨self.name, facet⟩
 
-end Module
+-- # Single Module Target
 
--- # Targets
-
-structure OleanAndC where
-  oleanFile : FilePath
-  cFile : FilePath
-  deriving Inhabited, Repr
-
-namespace OleanAndC
-
-protected def getMTime (self : OleanAndC) : IO MTime := do
-  return mixTrace (← getMTime self.oleanFile) (← getMTime self.cFile)
-
-instance : GetMTime OleanAndC := ⟨OleanAndC.getMTime⟩
-
-protected def computeHash (self : OleanAndC) : IO Hash := do
-  return mixTrace (← computeHash self.oleanFile) (← computeHash self.cFile)
-
-instance : ComputeHash OleanAndC IO := ⟨OleanAndC.computeHash⟩
-
-protected def checkExists (self : OleanAndC) : BaseIO Bool := do
-  return (← checkExists self.oleanFile) && (← checkExists self.cFile)
-
-instance : CheckExists OleanAndC := ⟨OleanAndC.checkExists⟩
-
-end OleanAndC
-
-abbrev OleanAndCTarget := BuildTarget OleanAndC
-
-namespace OleanAndCTarget
-
-abbrev oleanFile (self : OleanAndCTarget) := self.info.oleanFile
-def oleanTarget (self : OleanAndCTarget) : FileTarget :=
-  Target.mk self.oleanFile do self.bindSync fun i _ => computeTrace i.oleanFile
-
-abbrev cFile (self : OleanAndCTarget) := self.info.cFile
-def cTarget (self : OleanAndCTarget) : FileTarget :=
-  Target.mk self.cFile do self.bindSync fun i _ => computeTrace i.cFile
-
-end OleanAndCTarget
-
-structure ActiveOleanAndCTargets where
-  oleanTarget : ActiveFileTarget
-  cTarget : ActiveFileTarget
-  deriving Inhabited
-
-namespace ActiveOleanAndCTargets
-abbrev oleanFile (self : ActiveOleanAndCTargets) := self.oleanTarget.info
-abbrev cFile (self : ActiveOleanAndCTargets) := self.cTarget.info
-end ActiveOleanAndCTargets
-
-/--
-An active module `.olean` and `.c` target consists of a single task that
-builds both with two dependent targets that compute their individual traces.
--/
-abbrev ActiveOleanAndCTarget := ActiveBuildTarget ActiveOleanAndCTargets
-
-namespace ActiveOleanAndCTarget
-
-abbrev oleanFile (self : ActiveOleanAndCTarget) := self.info.oleanFile
-abbrev oleanTarget (self : ActiveOleanAndCTarget) := self.info.oleanTarget
-
-abbrev cFile (self : ActiveOleanAndCTarget) := self.info.cFile
-abbrev cTarget (self : ActiveOleanAndCTarget) := self.info.cTarget
-
-end ActiveOleanAndCTarget
-
-def OleanAndCTarget.activate (self : OleanAndCTarget) : SchedulerM ActiveOleanAndCTarget := do
-  let t ← BuildTarget.activate self
-  let oleanTask ← t.bindSync fun info depTrace => do
-    return mixTrace (← computeTrace info.oleanFile) depTrace
-  let cTask ← t.bindSync fun info _ => do
-    return mixTrace (← computeTrace info.cFile) (← getLeanTrace)
-  return t.withInfo {
-    oleanTarget := ActiveTarget.mk self.oleanFile oleanTask
-    cTarget := ActiveTarget.mk self.cFile cTask
-  }
-
--- # Module Builders
-
-def moduleTarget
-[CheckExists i] [GetMTime i] [ComputeHash i m] [MonadLiftT m BuildM] (info : i)
-(leanFile traceFile : FilePath) (contents : String) (depTarget : BuildTarget x)
-(argTrace : BuildTrace) (build : BuildM PUnit) : BuildTarget i :=
-  Target.mk info <| depTarget.bindOpaqueSync fun depTrace => do
-    let srcTrace : BuildTrace := ⟨Hash.ofString contents, ← getMTime leanFile⟩
-    let fullTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-    let upToDate ← fullTrace.checkAgainstFile info traceFile
-    unless upToDate do
-      build
-    fullTrace.writeToFile traceFile
+def moduleTarget (mod : Module)
+(depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
+  Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
+    let argTrace : BuildTrace := pureHash mod.leanArgs
+    let srcTrace : BuildTrace ← computeTrace mod.leanFile
+    let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
+    let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
+    if c then
+      let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
+      unless modUpToDate && cUpToDate do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
+          (← getOleanPath) mod.pkg.rootDir mod.leanArgs (← getLean)
+      modTrace.writeToFile mod.cTraceFile
+    else
+      unless modUpToDate do
+        compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
+          (← getOleanPath) mod.pkg.rootDir mod.leanArgs (← getLean)
+    modTrace.writeToFile mod.traceFile
     return depTrace
 
-def moduleOleanAndCTarget
-(leanFile cFile oleanFile traceFile : FilePath)
-(contents : String)  (depTarget : BuildTarget x)
-(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : OleanAndCTarget :=
-  let info := OleanAndC.mk oleanFile cFile
-  let ileanFile := oleanFile.withExtension "ilean"
-  moduleTarget info leanFile traceFile contents depTarget (pureHash leanArgs) do
-    compileLeanModule leanFile oleanFile ileanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
-
-def moduleOleanTarget
-(leanFile oleanFile traceFile : FilePath)
-(contents : String) (depTarget : BuildTarget x)
-(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : FileTarget :=
-  let ileanFile := oleanFile.withExtension "ilean"
-  let target := moduleTarget oleanFile leanFile traceFile contents depTarget (pureHash leanArgs) do
-    compileLeanModule leanFile oleanFile ileanFile none (← getOleanPath) rootDir leanArgs (← getLean)
-  target.withTask do target.bindSync fun oleanFile depTrace => do
-    return mixTrace (← computeTrace oleanFile) depTrace
-
-protected def Package.moduleOleanAndCTargetOnly (self : Package)
-(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
-  let cFile := self.modToC mod
-  let oleanFile := self.modToOlean mod
-  let traceFile := self.modToTraceFile mod
-  moduleOleanAndCTarget leanFile cFile oleanFile traceFile contents
-    depTarget self.rootDir self.moreLeanArgs
-
-protected def Package.moduleOleanTargetOnly (self : Package)
-(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
-  let oleanFile := self.modToOlean mod
-  let traceFile := self.modToTraceFile mod
-  moduleOleanTarget leanFile oleanFile traceFile contents depTarget
-    self.rootDir self.moreLeanArgs
-
 -- # Recursive Building
 
-/-
-Produces a recursive module target builder that
-builds the target module after recursively building its local imports
+/--
+Produces a recursive module target builder that builds the target module
+with the `build` function after recursively building its local imports
 (relative to the workspace).
 -/
-def recBuildModuleWithLocalImports
-[Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m]
-(build : Package → Name → FilePath → String → List α → BuildM α)
-: RecBuild Module α m := fun info recurse => do
+def recBuildModuleWithLocalImports [Monad m] [MonadLiftT BuildM m]
+(build : Module → List α → m α) : RecBuild Module α m := fun mod recurse => do
   have : MonadLift BuildM m := ⟨liftM⟩
-  have : MonadFunctor BuildM m := ⟨fun f => monadMap (m := BuildM) f⟩
-  let contents ← IO.FS.readFile info.srcFile
-  let (imports, _, _) ← Elab.parseImports contents info.srcFile.toString
+  let contents ← IO.FS.readFile mod.leanFile
+  let (imports, _, _) ← Elab.parseImports contents mod.leanFile.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
-    recurse ⟨pkg, mod⟩
-  build info.pkg info.name info.srcFile contents importTargets
+    recurse <| ← OptionT.mk <| findModule? imp.module
+  build mod importTargets
 
-def recBuildModuleOleanAndCTargetWithLocalImports
-[Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Module ActiveOleanAndCTarget m :=
-  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
-    let importTarget ← ActiveTarget.collectOpaqueList <| importTargets.map (·.oleanTarget)
-    let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.activate
-
-def recBuildModuleOleanTargetWithLocalImports
-[Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
-: RecBuild Module ActiveFileTarget m :=
-  recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
+/--
+Produces a recursive module target builder that builds the
+`olean`, `ilean`, and (optionally) `c` files of a module and its local imports
+after `extraDepTarget` finishes building.
+-/
+def recBuildModuleTargetWithDeps
+[Monad m] [MonadLiftT BuildM m] [MonadStore ModuleBuildKey ActiveOpaqueTarget m]
+(extraDepTarget : ActiveBuildTarget x) (c := true) : RecBuild Module ActiveOpaqueTarget m :=
+  recBuildModuleWithLocalImports fun mod importTargets => do
+    have : MonadLift BuildM m := ⟨liftM⟩
     let importTarget ← ActiveTarget.collectOpaqueList importTargets
-    let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.activate
+    let allDepsTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync importTarget
+    let modTarget := (← moduleTarget mod allDepsTarget c |>.activate).withoutInfo
+    if c then
+      let cTarget ← liftM (m := SchedulerM) do
+        return ActiveTarget.opaque <| ← modTarget.bindOpaqueSync (m := BuildM) fun _ => do
+          return mixTrace (← computeTrace mod.cFile) (← getLeanTrace)
+      store (mod.key `lean.c) cTarget
+    return modTarget
 
 -- ## Definitions
 
+abbrev ModuleMap (α) :=
+  Std.RBMap ModuleBuildKey α ModuleBuildKey.quickCmp
+
 abbrev ModuleBuildM (α) :=
-  -- equivalent to `RBTopT (cmp := Name.quickCmp) Name α BuildM`.
-  -- phrased this way to use `NameMap`
-  EStateT (List Name) (NameMap α) BuildM
+  -- equivalent to `RBTopT ModuleBuildKey α BuildM ModuleBuildKey.quickCmp`
+  -- phrased this way to use `ModuleMap`
+  EStateT (List ModuleBuildKey) (ModuleMap α) BuildM
 
 abbrev RecModuleBuild (o) :=
   RecBuild Module o (ModuleBuildM o)
 
-abbrev RecModuleTargetBuild (i) :=
-  RecModuleBuild (ActiveBuildTarget i)
+abbrev RecModuleTargetBuild :=
+  RecModuleBuild ActiveOpaqueTarget
 
--- ## Builders
+-- ## Multi-Module Builders
 
 /-- Build a single module using the recursive module build function `build`. -/
 def buildModule (mod : Module)
 [Inhabited o] (build : RecModuleBuild o) : BuildM o := do
   failOnBuildCycle <| ← RBTopT.run' do
-    buildRBTop (cmp := Name.quickCmp) build Module.name mod
+    buildTop build (·.key `lean) mod
 
 /--
 Build each module using the recursive module function `build`,
@@ -235,16 +131,15 @@ constructing an `Array`  of the results.
 def buildModuleArray (mods : Array Module)
 [Inhabited o] (build : RecModuleBuild o) : BuildM (Array o) := do
   failOnBuildCycle <| ← RBTopT.run' <| mods.mapM <|
-    buildRBTop (cmp := Name.quickCmp) build Module.name
+    buildTop build (·.key `lean)
 
 /--
 Build each module using the recursive module function `build`,
 constructing a module-target `NameMap`  of the results.
 -/
-def buildModuleMap [Inhabited o]
-(infos : Array Module) (build : RecModuleBuild o)
-: BuildM (NameMap o) := do
-  let (x, objMap) ← RBTopT.run do
-    infos.forM fun info => discard <| buildRBTop build Module.name info
+def buildModuleMap  (mods : Array Module)
+[Inhabited o] (build : RecModuleBuild o) : BuildM (ModuleMap o) := do
+  let (x, map) ← RBTopT.run <| mods.forM fun mod =>
+    discard <| buildTop build (·.key `lean) mod
   failOnBuildCycle x
-  return objMap
+  return map
diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index 9fd59b2ac1..aa45bbe624 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -3,9 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 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.Elab.Import
-import Lake.Config.Package
 import Lake.Build.Module
 
 open System
@@ -22,11 +19,11 @@ protected def Package.buildExtraDepsTarget (self : Package) : SchedulerM ActiveO
     let depTarget ← ActiveTarget.collectOpaqueArray depTargets
     extraDepTarget.mixOpaqueAsync depTarget
   let build dep recurse := do
-    let pkg := (← getPackageByName? dep.name).get!
+    let pkg := (← findPackage? dep.name).get!
     let depTargets ← pkg.dependencies.mapM recurse
     liftM <| collect pkg depTargets
-  let targetsE ← RBTopT.run' <| self.dependencies.mapM fun dep =>
-    buildRBTop (cmp := Name.quickCmp) build Dependency.name dep
+  let targetsE ← RBTopT.run' (cmp := Name.quickCmp) <| self.dependencies.mapM fun dep =>
+    buildTop build Dependency.name dep
   match targetsE with
   | Except.ok targets => collect self targets
   | Except.error _ => panic! "dependency cycle emerged after resolution"
@@ -38,39 +35,49 @@ def buildExtraDepsTarget : SchedulerM ActiveOpaqueTarget := do
 
 -- # Build Package Modules
 
+def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
+  return (← lib.getModuleArray self.srcDir).map (Module.mk self)
+
 /--
 Build the `extraDepTarget` of a package and its (transitive) dependencies
 and then build the library's modules recursively using the `build` function,
 constructing a single opaque target for the whole build.
 -/
 def Package.buildLibModules (self : Package) (lib : LeanLibConfig)
-[Inhabited i] (build : ActiveOpaqueTarget → RecModuleTargetBuild i) : SchedulerM (BuildTask BuildTrace) := do
+(build : ActiveOpaqueTarget → RecModuleTargetBuild) : SchedulerM Job := do
   let depTarget ← self.buildExtraDepsTarget
   let buildMods : BuildM _ := do
-    let infos := (← lib.getModuleArray self.srcDir).map (Module.mk self)
-    let modTargets ← buildModuleArray infos (build depTarget)
+    let mods ← self.getLibModuleArray lib
+    let modTargets ← buildModuleArray mods (build depTarget)
     (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
   buildMods.catchFailure fun _ => pure <| failure
 
 def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
-  Target.opaque <| self.buildLibModules lib recBuildModuleOleanTargetWithLocalImports
+  Target.opaque <| self.buildLibModules lib
+    (recBuildModuleTargetWithDeps · (c := false))
 
 def Package.libTarget (self : Package) : OpaqueTarget :=
   self.mkLibTarget self.builtinLibConfig
 
 -- # Build Specific Modules of the Package
 
-def Package.moduleOleanTarget (mod : Name) (self : Package) : FileTarget :=
-  BuildTarget.mk' (self.modToOlean mod) do
-    let depTarget ← self.buildExtraDepsTarget
-    let build := recBuildModuleOleanTargetWithLocalImports depTarget
-    return (← buildModule ⟨self, mod⟩ build).task
+def Module.leanBinTarget (c := false) (self : Module) : OpaqueTarget :=
+  BuildTarget.mk' () do
+    let depTarget ← self.pkg.buildExtraDepsTarget
+    let build := recBuildModuleTargetWithDeps depTarget (c := c)
+    return (← buildModule self build).task
 
-def Package.moduleOleanAndCTarget (mod : Name) (self : Package) : OleanAndCTarget :=
-  BuildTarget.mk' ⟨self.modToOlean mod, self.modToC mod⟩ do
-    let depTarget ← self.buildExtraDepsTarget
-    let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-    return (← buildModule ⟨self, mod⟩ build).task
+@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
+  self.leanBinTarget false |>.withInfo self.oleanFile
+
+@[inline] def Module.ileanTarget (self : Module) : FileTarget :=
+  self.leanBinTarget false |>.withInfo self.ileanFile
+
+def Module.mkCTarget (modTarget : OpaqueTarget) (self : Module) : FileTarget :=
+  Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ => computeTrace self.cFile
+
+@[inline] def Module.cTarget (self : Module) : FileTarget :=
+  self.mkCTarget <| self.leanBinTarget (c := true)
 
 -- # Build Imports
 
@@ -82,9 +89,8 @@ def Workspace.processImportList
 (imports : List String) (self : Workspace) : Array Module := Id.run do
   let mut localImports := #[]
   for imp in imports do
-    let mod := imp.toName
-    if let some pkg := self.packageForModule? mod then
-      localImports := localImports.push ⟨pkg, mod⟩
+    if let some mod := self.findModule? imp.toName then
+      localImports := localImports.push mod
   return localImports
 
 /--
@@ -101,12 +107,12 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
     depTarget.buildOpaque
   else
     -- build local imports from list
-    let infos := (← getWorkspace).processImportList imports
+    let mods := (← getWorkspace).processImportList imports
     if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
-      let build := recBuildModuleOleanTargetWithLocalImports depTarget
-      let targets ← buildModuleArray infos build
+      let build := recBuildModuleTargetWithDeps depTarget (c := false)
+      let targets ← buildModuleArray mods build
       targets.forM (·.buildOpaque)
     else
-      let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
-      let targets ← buildModuleArray infos build
+      let build := recBuildModuleTargetWithDeps depTarget (c := true)
+      let targets ← buildModuleArray mods build
       targets.forM (·.buildOpaque)
diff --git a/Lake/Build/Recursive.lean b/Lake/Build/Recursive.lean
index 7bf90b2e23..a6b15e2bf3 100644
--- a/Lake/Build/Recursive.lean
+++ b/Lake/Build/Recursive.lean
@@ -102,8 +102,3 @@ def run' [Monad m] (self : RBTopT k o cmp m α) :=
   Functor.map (·.1) self.run
 
 end RBTopT
-
-/-- The `RBMap` version of `buildTop`. -/
-def buildRBTop {k o} {cmp} {m} [BEq k] [Inhabited o] [Monad m]
-(build : RecBuild i o (RBTopT k o cmp m)) (keyOf : i → k) (info : i) : RBTopT k o cmp m o :=
-  buildTop build keyOf info
diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean
index 14114bea91..1db9fa2825 100644
--- a/Lake/Build/TargetTypes.lean
+++ b/Lake/Build/TargetTypes.lean
@@ -21,10 +21,10 @@ abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace
 
 namespace BuildTarget
 
-abbrev mk (info : i) (task : SchedulerM (BuildTask BuildTrace)) : BuildTarget i :=
+abbrev mk (info : i) (task : SchedulerM Job) : BuildTarget i :=
   Target.mk info task
 
-abbrev mk' (info : i) (task : BuildM (BuildTask BuildTrace)) : BuildTarget i :=
+abbrev mk' (info : i) (task : BuildM Job) : BuildTarget i :=
   Target.mk info <| task.catchFailure fun _ => pure failure
 
 abbrev activate (self : BuildTarget i) : SchedulerM (ActiveBuildTarget i) :=
@@ -70,10 +70,10 @@ abbrev ActiveOpaqueTarget := ActiveBuildTarget PUnit
 
 namespace OpaqueTarget
 
-abbrev mk (task : SchedulerM (BuildTask BuildTrace)) : OpaqueTarget :=
+abbrev mk (task : SchedulerM Job) : OpaqueTarget :=
   Target.opaque task
 
-abbrev mk' (task : BuildM (BuildTask BuildTrace)) : OpaqueTarget :=
+abbrev mk' (task : BuildM Job) : OpaqueTarget :=
   Target.opaque <| task.catchFailure fun _ => pure failure
 
 abbrev async (act : BuildM BuildTrace) : OpaqueTarget :=
diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean
index b652d9dd10..ea917d4145 100644
--- a/Lake/Build/Targets.lean
+++ b/Lake/Build/Targets.lean
@@ -64,12 +64,12 @@ def leanSharedLibTarget (binFile : FilePath)
   fileTargetWithDepArray binFile linkTargets fun links => do
     compileSharedLib binFile links linkArgs (← getLeanc)
 
-def binTarget (binFile : FilePath) (linkTargets : Array FileTarget)
+def cExeTarget (binFile : FilePath) (linkTargets : Array FileTarget)
 (linkArgs : Array String := #[]) (linker : FilePath := "cc") : FileTarget :=
    fileTargetWithDepArray binFile linkTargets (extraDepTrace := computeHash linkArgs) fun links => do
     compileBin binFile links linkArgs linker
 
-def leanBinTarget (binFile : FilePath)
+def leanExeTarget (binFile : FilePath)
 (linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
   fileTargetWithDepArray binFile linkTargets
   (extraDepTrace := getLeanTrace <&> (·.mix <| pureHash linkArgs)) fun links => do
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 1bde91f853..62fdda60fc 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -22,22 +22,19 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
   if spec.isEmpty then
     return ws.root
   else
-    match ws.packageByName? spec.toName with
+    match ws.findPackage? spec.toName with
     | some pkg => return pkg
     | none => throw <| CliError.unknownPackage spec
 
-def resolveModuleTarget (pkg : Package) (mod : Name) (facet : String) : Except CliError OpaqueTarget :=
-  if pkg.hasModule mod then
-    if facet.isEmpty || facet == "olean" then
-      return pkg.moduleOleanTarget mod |>.withoutInfo
-    else if facet == "c" then
-      return pkg.moduleOleanAndCTarget mod |>.withoutInfo
-    else if facet == "o" then
-      return pkg.moduleOTarget mod |>.withoutInfo
-    else
-      throw <| CliError.unknownFacet "module" facet
+def resolveModuleTarget (mod : Module) (facet : String) : Except CliError OpaqueTarget :=
+  if facet.isEmpty || facet == "bin"  || facet == "ilean" || facet == "olean" then
+    return mod.leanBinTarget (c := false)
+  else if facet == "c" then
+    return mod.leanBinTarget (c := true)
+  else if facet == "o" then
+    return mod.oTarget.withoutInfo
   else
-    throw <| CliError.missingModule pkg.name mod
+    throw <| CliError.unknownFacet "module" facet
 
 def resolveLibTarget (pkg : Package) (lib : LeanLibConfig) (facet : String) : Except CliError OpaqueTarget :=
   if facet.isEmpty || facet == "lean" || facet == "oleans" then
@@ -65,8 +62,8 @@ def resolveTargetInPackage (pkg : Package) (target : Name) (facet : String) : Ex
       throw <| CliError.invalidFacet target facet
   else if let some lib := pkg.findLeanLib? target then
     resolveLibTarget pkg lib facet
-  else if pkg.hasModule target then
-    resolveModuleTarget pkg target facet
+  else if let some mod := pkg.findModule? target then
+    resolveModuleTarget mod facet
   else
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
@@ -92,19 +89,19 @@ def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError Opaq
     throw <| CliError.unknownFacet "package" facet
 
 def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget :=
-  if let some (pkg, exe) := ws.findLeanExe? spec then
+  if let some (pkg, exe) := ws.findLeanExe? spec.toName then
     resolveExeTarget pkg exe facet
-  else if let some (_, lib) := ws.findExternLib? spec then
+  else if let some (_, lib) := ws.findExternLib? spec.toName then
     if facet.isEmpty then
       return lib.target.withoutInfo
     else
       throw <| CliError.invalidFacet spec facet
-  else if let some (pkg, lib) := ws.findLeanLib? spec then
+  else if let some (pkg, lib) := ws.findLeanLib? spec.toName then
     resolveLibTarget pkg lib facet
-  else if let some pkg := ws.packageByName? spec then
+  else if let some pkg := ws.findPackage? spec.toName then
     resolvePackageTarget pkg facet
-  else if let some pkg := ws.packageForModule? spec then
-    resolveModuleTarget pkg spec facet
+  else if let some mod := ws.findModule? spec.toName then
+    resolveModuleTarget mod facet
   else
     throw <| CliError.unknownTarget spec
 
@@ -118,8 +115,8 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep
       resolvePackageTarget pkg facet
     else if spec.startsWith "+" then
       let mod := spec.drop 1 |>.toName
-      if let some pkg := ws.packageForModule? mod then
-        resolveModuleTarget pkg mod facet
+      if let some mod := ws.findModule? mod then
+        resolveModuleTarget mod facet
       else
         throw <| CliError.unknownModule mod
     else
@@ -129,7 +126,10 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep
     let pkg ← parsePackageSpec ws pkgSpec
     if targetSpec.startsWith "+" then
       let mod := targetSpec.drop 1 |>.toName
-      resolveModuleTarget pkg mod facet
+      if let some mod := pkg.findModule? mod then
+        resolveModuleTarget mod facet
+      else
+        throw <| CliError.unknownModule mod
     else
       resolveTargetInPackage pkg spec facet
   | _ =>
diff --git a/Lake/Config.lean b/Lake/Config.lean
index 3aeb3dfc0c..f3555bac00 100644
--- a/Lake/Config.lean
+++ b/Lake/Config.lean
@@ -8,5 +8,6 @@ import Lake.Config.InstallPath
 import Lake.Config.Workspace
 import Lake.Config.Script
 import Lake.Config.Package
+import Lake.Config.Module
 import Lake.Config.Monad
 import Lake.Config.SearchPath
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
new file mode 100644
index 0000000000..469c1bc481
--- /dev/null
+++ b/Lake/Config/Module.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Trace
+import Lake.Config.Package
+
+namespace Lake
+open System Lean
+
+/-- A buildable Lean module of a `Package`. -/
+structure Module where
+  pkg : Package
+  name : Name
+  deriving Inhabited
+
+/-- Locate the named module in the package (if it is local to it). -/
+def Package.findModule? (mod : Name) (self : Package) : Option Module :=
+  if self.isBuildableModule mod then some ⟨self, mod⟩ else none
+
+namespace Module
+
+def leanFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.srcDir self.name "lean"
+
+def oleanFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.oleanDir self.name "olean"
+
+def ileanFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.oleanDir self.name "ilean"
+
+def traceFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.oleanDir self.name "trace"
+
+def cFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.irDir self.name "c"
+
+def cTraceFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.irDir self.name "c.trace"
+
+def oFile (self : Module) : FilePath :=
+  Lean.modToFilePath self.pkg.irDir self.name "o"
+
+@[inline] def leanArgs (self : Module) : Array String :=
+  self.pkg.moreLeanArgs
+
+@[inline] def leancArgs (self : Module) : Array String :=
+  self.pkg.moreLeancArgs
+
+-- ## Trace Helpers
+
+protected def getMTime (self : Module) : IO MTime := do
+  return mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)
+
+instance : GetMTime Module := ⟨Module.getMTime⟩
+
+protected def computeHash (self : Module) : IO Hash := do
+  return mixTrace (← computeHash self.oleanFile) (← computeHash self.ileanFile)
+
+instance : ComputeHash Module IO := ⟨Module.computeHash⟩
+
+protected def checkExists (self : Module) : BaseIO Bool := do
+  return (← checkExists self.oleanFile) && (← checkExists self.ileanFile)
+
+instance : CheckExists Module := ⟨Module.checkExists⟩
diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean
index d2dd1f69e4..e5e9e07ec3 100644
--- a/Lake/Config/Monad.lean
+++ b/Lake/Config/Monad.lean
@@ -49,11 +49,11 @@ def getLeanEnv [Monad m] : m (Array (String × Option String)) := do
 
 variable [Functor m]
 
-@[inline] def getPackageByName? (name : Name) : m (Option Package) :=
-  (·.packageByName? name) <$> getWorkspace
+@[inline] def findPackage? (name : Name) : m (Option Package) :=
+  (·.findPackage? name) <$> getWorkspace
 
-@[inline] def getPackageForModule? (mod : Name) : m (Option Package) :=
-  (·.packageForModule? mod) <$> getWorkspace
+@[inline] def findModule? (mod : Name) : m (Option Module) :=
+  (·.findModule? mod) <$> getWorkspace
 
 @[inline] def getOleanPath : m SearchPath :=
   (·.oleanPath) <$> getWorkspace
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index f6ad0345eb..076d539669 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -331,10 +331,6 @@ def extraDepTarget (self : Package) : OpaqueTarget :=
 def defaultFacet (self : Package) : PackageFacet :=
    self.config.defaultFacet
 
-/-- The package's `moreLibTargets` configuration. -/
-def moreLibTargets (self : Package) : Array FileTarget :=
-  self.config.moreLibTargets
-
 /-- Get the package's library configuration with the given name. -/
 def findLeanLib? (name : Name) (self : Package) : Option LeanLibConfig :=
   self.leanLibs.find? name
@@ -349,7 +345,8 @@ def findExternLib? (name : Name) (self : Package) : Option ExternLibConfig :=
 
 /-- Get an `Array` of the package's external library targets. -/
 def externLibTargets (self : Package) : Array FileTarget :=
-  self.externLibs.fold (fun xs _ x => xs.push x.target) #[] ++ self.moreLibTargets
+  self.externLibs.fold (fun xs _ x => xs.push x.target) #[] ++
+  self.config.moreLibTargets
 
 /-- The package's `moreServerArgs` configuration. -/
 def moreServerArgs (self : Package) : Array String :=
@@ -359,14 +356,10 @@ def moreServerArgs (self : Package) : Array String :=
 def srcDir (self : Package) : FilePath :=
   self.dir / self.config.srcDir
 
-/-- The package's root directory for Lean (i.e., `srcDir`). -/
+/-- The package's root directory for `lean` (i.e., `srcDir`). -/
 def rootDir (self : Package) : FilePath :=
   self.srcDir
 
-/-- The path to a module's `.lean` source file within the package. -/
-def modToSrc (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.srcDir mod "lean"
-
 /-- The package's `dir` joined with its `buildDir` configuration. -/
 def buildDir (self : Package) : FilePath :=
   self.dir / self.config.buildDir
@@ -379,18 +372,6 @@ def oleanDir (self : Package) : FilePath :=
 def moreLeanArgs (self : Package) : Array String :=
   self.config.moreLeanArgs
 
-/-- The path to a module's `.olean` file within the package. -/
-def modToOlean (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.oleanDir mod "olean"
-
-/-- The path to a module's `.ilean` file within the package. -/
-def modToIlean (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.oleanDir mod "ilean"
-
-/-- The path to module's `.trace` file within the package. -/
-def modToTraceFile (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.oleanDir mod "trace"
-
 /- `-O3`, `-DNDEBUG`, and `moreLeancArgs` -/
 def moreLeancArgs (self : Package) : Array String :=
   #["-O3", "-DNDEBUG"] ++ self.config.moreLeancArgs
@@ -399,22 +380,6 @@ def moreLeancArgs (self : Package) : Array String :=
 def irDir (self : Package) : FilePath :=
   self.buildDir / self.config.irDir
 
-/-- To which Lake should output the package's `.c` files (.e., `irDir`). -/
-def cDir (self : Package) : FilePath :=
-  self.irDir
-
-/-- The path to a module's `.c` file within the package. -/
-def modToC (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.cDir mod "c"
-
-/-- To which Lake should output the package's `.o` files (.e., `irDir`). -/
-def oDir (self : Package) : FilePath :=
-  self.irDir
-
-/-- The path to a module's `.o` file within the package. -/
-def modToO (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.oDir mod "o"
-
 /-- The package's `buildDir` joined with its `libDir` configuration. -/
 def libDir (self : Package) : FilePath :=
   self.buildDir / self.config.libDir
@@ -441,8 +406,8 @@ def isLocalModule (mod : Name) (self : Package) : Bool :=
   self.builtinLibConfig.isLocalModule mod
 
 /-- Whether the given module is in the package (i.e., can build it). -/
-def hasModule (mod : Name) (self : Package) : Bool :=
-  self.leanLibs.any (fun _ lib => lib.hasModule mod) ||
+def isBuildableModule (mod : Name) (self : Package) : Bool :=
+  self.leanLibs.any (fun _ lib => lib.isBuildableModule mod) ||
   self.leanExes.any (fun _ exe => exe.root == mod) ||
-  self.builtinLibConfig.hasModule mod ||
+  self.builtinLibConfig.isBuildableModule mod ||
   self.config.binRoot == mod
diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean
index 3aac6877e1..da9f006fbe 100644
--- a/Lake/Config/Resolve.lean
+++ b/Lake/Config/Resolve.lean
@@ -120,8 +120,8 @@ def resolveDeps (ws : Workspace) (pkg : Package)
     let pkg ← resolveDep ws pkg dep shouldUpdate
     pkg.dependencies.forM fun dep => discard <| resolve dep
     return pkg
-  let (res, map) ← RBTopT.run <| pkg.dependencies.forM fun dep =>
-    discard <| buildRBTop (cmp := Name.quickCmp) resolve Dependency.name dep
+  let (res, map) ← RBTopT.run (cmp := Name.quickCmp) <| pkg.dependencies.forM fun dep =>
+    discard <| buildTop resolve Dependency.name dep
   match res with
   | Except.ok _ => return map
   | Except.error cycle => do
diff --git a/Lake/Config/Targets.lean b/Lake/Config/Targets.lean
index c8ff6474ad..6af0fe41ed 100644
--- a/Lake/Config/Targets.lean
+++ b/Lake/Config/Targets.lean
@@ -61,8 +61,8 @@ def isLocalModule (mod : Name) (self : LeanLibConfig) : Bool :=
   self.roots.any (fun root => root.isPrefixOf mod) ||
   self.globs.any (fun glob => glob.matches mod)
 
-/-- Whether the given module is in the library (i.e., is built as part of it). -/
-def hasModule (mod : Name) (self : LeanLibConfig) : Bool :=
+/-- Whether the given module is a buildable part of the library. -/
+def isBuildableModule (mod : Name) (self : LeanLibConfig) : Bool :=
   self.globs.any (fun glob => glob.matches mod) ||
   self.roots.any (fun root => root.isPrefixOf mod && self.globs.any (·.matches root))
 
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 02c542e88e..b399cfd0cf 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -7,6 +7,7 @@ import Lean.Util.Paths
 import Lake.Config.Opaque
 import Lake.Config.WorkspaceConfig
 import Lake.Config.Package
+import Lake.Config.Module
 
 open System
 open Lean (Name NameMap LeanPaths)
@@ -80,20 +81,16 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace :=
   {self with packageMap := self.packageMap.insert pkg.name pkg}
 
 /-- Get a package within the workspace by name. -/
-def packageByName? (pkg : Name) (self : Workspace) : Option Package :=
+def findPackage? (pkg : Name) (self : Workspace) : Option Package :=
   self.packageMap.find? pkg
 
-/-- Find a package in the workspace satisfying the given predicate (if one exists). -/
-def findPackage? (f : Package → Bool) (self : Workspace) : Option Package :=
-  self.packageArray.find? f
-
 /-- Check if the module is local to any package in the workspace. -/
 def isLocalModule (mod : Name) (self : Workspace) : Bool :=
   self.packageMap.any fun _ pkg => pkg.isLocalModule mod
 
-/-- Get the package for the module in the workspace (if it is local to one). -/
-def packageForModule? (mod : Name) (self : Workspace) : Option Package :=
-  self.findPackage? (·.isLocalModule mod)
+/-- Locate the named module in the workspace (if it is local to it). -/
+def findModule? (mod : Name) (self : Workspace) : Option Module :=
+  self.packageArray.findSome? (·.findModule? mod)
 
 /-- Get the workspace's library configuration with the given name. -/
 def findLeanLib? (name : Name) (self : Workspace) : Option (Package × LeanLibConfig) :=
diff --git a/examples/targets/test.sh b/examples/targets/test.sh
index c4299e6387..6f6c4728af 100755
--- a/examples/targets/test.sh
+++ b/examples/targets/test.sh
@@ -15,8 +15,14 @@ fi
 ./clean.sh
 
 $LAKE build +Foo.Test
+
+test -f ./build/lib/Foo/Test.olean
+test ! -f ./build/lib/Foo/Test.c
+
 $LAKE build Bar:o
 
+test -f ./build/ir/Bar.o
+
 $LAKE build
 
 ./build/bin/c