diff --git a/Lake.lean b/Lake.lean
index f43d7a2371..01b5c45bf3 100644
--- a/Lake.lean
+++ b/Lake.lean
@@ -5,8 +5,6 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Cli
 import Lake.SearchPath
--- API file not imported elsewhere; imported here to force build
-import Lake.BuildTargets
 
 def main (args : List String) : IO UInt32 := do
   try
diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean
index c16c1bbfa0..a184e45ae4 100644
--- a/Lake/BuildBin.lean
+++ b/Lake/BuildBin.lean
@@ -49,7 +49,7 @@ protected def ActivePackageTarget.binTarget
 def Package.binTarget (self : Package) : FileTarget :=
   Target.mk self.binFile do
     let depTargets ← self.buildDepTargets
-    let pkgTarget ← self.buildTargetWithDepTargets depTargets
+    let pkgTarget ← self.buildOleanAndCTargetsWithDepTargets depTargets
     pkgTarget.binTarget depTargets >>= (·.materializeAsync)
 
 def buildBin (pkg : Package) : IO PUnit :=
diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean
index d16faab4f2..fcbce8b683 100644
--- a/Lake/BuildModule.lean
+++ b/Lake/BuildModule.lean
@@ -18,40 +18,38 @@ namespace Lake
 
 -- # Targets
 
-abbrev OleanTarget := ActiveFileTarget
-
-structure ModuleTargetInfo where
+structure OleanAndC where
   oleanFile : FilePath
   cFile : FilePath
   deriving Inhabited
 
-namespace ModuleArtifact
+namespace OleanAndC
 
-protected def getMTime (self : ModuleTargetInfo) : IO MTime := do
+protected def getMTime (self : OleanAndC) : IO MTime := do
   return mixTrace (← getMTime self.oleanFile) (← getMTime self.cFile)
 
-instance : GetMTime ModuleTargetInfo := ⟨ModuleArtifact.getMTime⟩
+instance : GetMTime OleanAndC := ⟨OleanAndC.getMTime⟩
 
-protected def computeHash (self : ModuleTargetInfo) : IO Hash := do
+protected def computeHash (self : OleanAndC) : IO Hash := do
   return mixTrace (← computeHash self.oleanFile) (← computeHash self.cFile)
 
-instance : ComputeHash ModuleTargetInfo := ⟨ModuleArtifact.computeHash⟩
+instance : ComputeHash OleanAndC := ⟨OleanAndC.computeHash⟩
 
-end ModuleArtifact
+end OleanAndC
 
-abbrev ActiveModuleTarget := ActiveBuildTarget ModuleTargetInfo
+abbrev ActiveOleanAndCTarget := ActiveBuildTarget OleanAndC
 
-namespace ActiveModuleTarget
+namespace ActiveOleanAndCTarget
 
-def oleanFile (self : ActiveModuleTarget) := self.info.oleanFile
-def oleanTarget (self : ActiveModuleTarget) : ActiveFileTarget :=
+def oleanFile (self : ActiveOleanAndCTarget) := self.info.oleanFile
+def oleanTarget (self : ActiveOleanAndCTarget) : ActiveFileTarget :=
   self.withInfo self.oleanFile
 
-def cFile (self : ActiveModuleTarget) := self.info.cFile
-def cTarget (self : ActiveModuleTarget) : ActiveFileTarget :=
+def cFile (self : ActiveOleanAndCTarget) := self.info.cFile
+def cTarget (self : ActiveOleanAndCTarget) : ActiveFileTarget :=
   self.withInfo self.cFile
 
-end ActiveModuleTarget
+end ActiveOleanAndCTarget
 
 -- # Trace Checking
 
@@ -72,38 +70,51 @@ def checkModuleTrace [GetMTime i] (info : i)
 
 -- # Module Builders
 
-def mkModuleTarget [GetMTime i] [ComputeHash i] (info : i)
-(leanFile hashFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
-(build : BuildM PUnit) : BuildM (ActiveBuildTarget i) := do
-  ActiveTarget.mk info <| ← depTarget.mapOpaqueAsync fun depTrace => do
+def moduleTarget [GetMTime i] [ComputeHash i] (info : i)
+(leanFile hashFile : FilePath) (contents : String) (depTarget : BuildTarget x)
+(build : BuildM PUnit) : BuildTarget i :=
+  Target.mk info <| depTarget.mapOpaqueAsync fun depTrace => do
     let (upToDate, trace) ← checkModuleTrace info leanFile hashFile contents depTrace
     if upToDate then
       BuildTrace.fromHash <| (← computeHash info).mix depTrace.hash
     else
       build
       IO.FS.writeFile hashFile trace.hash.toString
-       let newTrace : BuildTrace ← liftM <| computeTrace info
+      let newTrace : BuildTrace ← liftM <| computeTrace info
       newTrace.mix depTrace
 
-def fetchModuleTarget (pkg : Package) (moreOleanDirs : List FilePath)
-(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
-: BuildM ActiveModuleTarget := do
-  let cFile := pkg.modToC mod
-  let oleanFile := pkg.modToOlean mod
-  let info := ModuleTargetInfo.mk oleanFile cFile
-  let hashFile := pkg.modToHashFile mod
-  let oleanDirs :=  pkg.oleanDir :: moreOleanDirs
-  mkModuleTarget  info leanFile hashFile contents depTarget <|
-    compileOleanAndC leanFile oleanFile cFile oleanDirs pkg.rootDir pkg.leanArgs
+def moduleOleanAndCTarget
+(leanFile cFile oleanFile hashFile : FilePath)
+(oleanDirs : List FilePath) (contents : String)  (depTarget : BuildTarget x)
+(rootDir : FilePath := ".") (leanArgs : Array String := #[]) :=
+  moduleTarget (OleanAndC.mk oleanFile cFile) leanFile hashFile contents depTarget <|
+    compileOleanAndC leanFile oleanFile cFile oleanDirs rootDir leanArgs
 
-def fetchModuleOleanTarget (pkg : Package) (moreOleanDirs : List FilePath)
-(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
-: BuildM OleanTarget := do
-  let oleanFile := pkg.modToOlean mod
-  let hashFile := pkg.modToHashFile mod
-  let oleanDirs := pkg.oleanDir :: moreOleanDirs
-  mkModuleTarget oleanFile leanFile hashFile contents depTarget <|
-    compileOlean leanFile oleanFile oleanDirs pkg.rootDir pkg.leanArgs
+def moduleOleanTarget
+(leanFile oleanFile hashFile : FilePath)
+(oleanDirs : List FilePath) (contents : String) (depTarget : BuildTarget x)
+(rootDir : FilePath := ".") (leanArgs : Array String := #[]) :=
+  moduleTarget oleanFile leanFile hashFile contents depTarget <|
+    compileOlean leanFile oleanFile oleanDirs rootDir leanArgs
+
+protected def Package.moduleOleanAndCTarget
+(self : Package) (moreOleanDirs : List FilePath) (mod : Name)
+(leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
+  let cFile := self.modToC mod
+  let oleanFile := self.modToOlean mod
+  let hashFile := self.modToHashFile mod
+  let oleanDirs :=  self.oleanDir :: moreOleanDirs
+  moduleOleanAndCTarget leanFile cFile oleanFile hashFile oleanDirs contents
+    depTarget self.rootDir self.leanArgs
+
+protected def Package.moduleOleanTarget
+(self : Package) (moreOleanDirs : List FilePath) (mod : Name)
+(leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
+  let oleanFile := self.modToOlean mod
+  let hashFile := self.modToHashFile mod
+  let oleanDirs := self.oleanDir :: moreOleanDirs
+  moduleOleanTarget leanFile oleanFile hashFile oleanDirs contents depTarget
+    self.rootDir self.leanArgs
 
 -- # Recursive Fetching
 
@@ -126,32 +137,34 @@ def recFetchModuleWithLocalImports (pkg : Package)
   let importTargets ← imports.mapM fetch
   build mod leanFile contents importTargets
 
-def recFetchModuleTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
-(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
-: RecFetch Name ActiveModuleTarget m :=
-  recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do
-    let allDepsTarget ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
-    fetchModuleTarget pkg moreOleanDirs mod leanFile contents allDepsTarget
+def Package.recFetchModuleOleanAndCTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
+(self : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
+: RecFetch Name ActiveOleanAndCTarget m :=
+  recFetchModuleWithLocalImports self fun mod leanFile contents importTargets => do
+    let allDepsTarget := Target.active <| ←
+      depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
+    self.moduleOleanAndCTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run
 
-def recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
-(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
-: RecFetch Name OleanTarget m :=
-  recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do
-    let allDepsTarget ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
-    fetchModuleOleanTarget pkg moreOleanDirs mod leanFile contents allDepsTarget
+def  Package.recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
+(self : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
+: RecFetch Name ActiveFileTarget m :=
+  recFetchModuleWithLocalImports self fun mod leanFile contents importTargets => do
+    let allDepsTarget := Target.active <| ←
+      depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
+    self.moduleOleanTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run
 
 -- ## Definitions
 
 abbrev ModuleFetchM (α) :=
-  -- equivalent to `RBTopT (cmp := Name.quickCmp) Name ActiveModuleTarget BuildM`.
+  -- equivalent to `RBTopT (cmp := Name.quickCmp) Name α BuildM`.
   -- phrased this way to use `NameMap`
   EStateT (List Name) (NameMap α) BuildM
 
 abbrev ModuleFetch (α) :=
   RecFetch Name α (ModuleFetchM α)
 
-abbrev OleanTargetFetch := ModuleFetch OleanTarget
-abbrev ModuleTargetFetch := ModuleFetch ActiveModuleTarget
+abbrev OleanTargetFetch := ModuleFetch ActiveFileTarget
+abbrev OleanAndCTargetFetch := ModuleFetch ActiveOleanAndCTarget
 
-abbrev OleanTargetMap := NameMap OleanTarget
-abbrev ModuleTargetMap := NameMap ActiveModuleTarget
+abbrev OleanTargetMap := NameMap ActiveFileTarget
+abbrev OleanAndCTargetMap := NameMap ActiveOleanAndCTarget
diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean
index e7b78eabb5..0879c57c92 100644
--- a/Lake/BuildPackage.lean
+++ b/Lake/BuildPackage.lean
@@ -17,65 +17,65 @@ namespace Lake
 
 -- # Build Target
 
-abbrev ActivePackageTarget := ActiveBuildTarget (Package × ModuleTargetMap)
+abbrev ActivePackageTarget := ActiveBuildTarget (Package × NameMap ActiveOleanAndCTarget)
 
 namespace ActivePackageTarget
 
 def package (self : ActivePackageTarget) :=
   self.info.1
 
-def moduleTargetMap (self : ActivePackageTarget) : ModuleTargetMap :=
+def moduleTargetMap (self : ActivePackageTarget) : NameMap ActiveOleanAndCTarget :=
   self.info.2
 
-def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveModuleTarget) :=
+def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCTarget) :=
   self.moduleTargetMap.fold (fun arr k v => arr.push (k, v)) #[]
 
 end ActivePackageTarget
 
 -- # Build Modules
 
-def Package.buildModuleTargetDAGFor
-(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
-(self : Package) : BuildM (ActiveModuleTarget × ModuleTargetMap) := do
-  let fetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget
+def Package.buildModuleOleanAndCTargetDAG
+(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
+(self : Package) : BuildM (ActiveOleanAndCTarget × OleanAndCTargetMap) := do
+  let fetch := self.recFetchModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
   failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
 
-def Package.buildOleanTargetDAGFor
-(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
-(self : Package) : BuildM (OleanTarget × OleanTargetMap) := do
+def Package.buildModuleOleanTargetDAG
+(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
+(self : Package) : BuildM (ActiveFileTarget × OleanTargetMap) := do
   let fetch := recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget
   failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
 
-def Package.buildModuleTargetDAG
-(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
-  self.buildModuleTargetDAGFor self.moduleRoot moreOleanDirs depTarget
+def Package.buildOleanAndCTargetDAG
+(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
+  self.buildModuleOleanAndCTargetDAG self.moduleRoot moreOleanDirs depTarget
 
 def Package.buildOleanTargetDAG
-(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
-  self.buildOleanTargetDAGFor self.moduleRoot moreOleanDirs depTarget
+(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
+  self.buildModuleOleanTargetDAG self.moduleRoot moreOleanDirs depTarget
 
-def Package.buildModuleTargets
+def Package.buildOleanAndCTargets
 (mods : List Name) (moreOleanDirs : List FilePath)
-(depTarget : ActiveOpaqueTarget) (self : Package)
-: BuildM (List ActiveModuleTarget) := do
-  let fetch : ModuleTargetFetch :=
-    recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget
+(depTarget : ActiveBuildTarget x) (self : Package)
+: BuildM (List ActiveOleanAndCTarget) := do
+  let fetch : OleanAndCTargetFetch :=
+    self.recFetchModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
   failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
 
 def Package.buildOleanTargets
 (mods : List Name) (moreOleanDirs : List FilePath)
-(depTarget : ActiveOpaqueTarget) (self : Package)
-: BuildM (List OleanTarget) := do
+(depTarget : ActiveBuildTarget x) (self : Package)
+: BuildM (List ActiveFileTarget) := do
   let fetch : OleanTargetFetch :=
-    recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget
+    self.recFetchModuleOleanTargetWithLocalImports moreOleanDirs depTarget
   failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
 
-def Package.buildRootModuleTarget
-(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
-  self.buildModuleTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
+def Package.buildRootOleanAndCTarget
+(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
+  self.buildOleanAndCTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
 
 def Package.buildRootOleanTarget
-(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
+(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
   self.buildOleanTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
 
 -- # Configure/Build Packages
@@ -86,24 +86,30 @@ def Package.buildDepTargetWith
   let depTarget ← ActiveTarget.collectOpaqueList depTargets
   extraDepTarget.mixOpaqueAsync depTarget
 
-def Package.buildTargetWithDepTargetsFor
+def Package.buildModuleOleanAndCTargetWithDepTargets
 (mod : Name) (depTargets : List ActivePackageTarget) (self : Package)
 : BuildM ActivePackageTarget := do
   let depTarget ← self.buildDepTargetWith depTargets
   let moreOleanDirs := depTargets.map (·.package.oleanDir)
-  let (target, targetMap) ← self.buildModuleTargetDAGFor mod moreOleanDirs depTarget
+  let (target, targetMap) ← self.buildModuleOleanAndCTargetDAG mod moreOleanDirs depTarget
   return target.withInfo ⟨self, targetMap⟩
 
-def Package.buildTargetWithDepTargets
+def Package.buildOleanAndCTargetsWithDepTargets
 (depTargets : List ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget :=
-  self.buildTargetWithDepTargetsFor self.moduleRoot depTargets
+  self.buildModuleOleanAndCTargetWithDepTargets self.moduleRoot depTargets
 
+/--
+  The main package build function.
+
+  It resolves the package's dependencies and recursively builds them.
+  For each package, it compiles its modules into `.olean` and `.c` files.
+-/
 partial def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
   let deps ← solveDeps self
   -- build dependencies recursively
   -- TODO: share build of common dependencies
   let depTargets ← deps.mapM (·.buildTarget)
-  self.buildTargetWithDepTargets depTargets
+  self.buildOleanAndCTargetsWithDepTargets depTargets
 
 def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do
   let deps ← solveDeps self
@@ -130,22 +136,22 @@ def build (pkg : Package) : IO PUnit :=
 
 -- # Print Paths
 
-def Package.buildOleanTargetsWithDeps
+def Package.buildModuleOleanTargetsWithDeps
 (deps : List Package) (mods : List Name) (self : Package)
-: BuildM (List OleanTarget) := do
+: BuildM (List ActiveFileTarget) := do
   let moreOleanDirs := deps.map (·.oleanDir)
   let depTarget ← self.buildDepTargetWith <| ← deps.mapM (·.buildTarget)
   self.buildOleanTargets mods moreOleanDirs depTarget
 
-def Package.buildOleansWithDeps
+def Package.buildModuleOleansWithDeps
 (deps : List Package) (mods : List Name)  (self : Package) :=
-  self.buildOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
+  self.buildModuleOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
 
 def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
   let deps ← solveDeps pkg
   unless imports.isEmpty do
     let imports := imports.map (·.toName)
     let localImports := imports.filter (·.getRoot == pkg.moduleRoot)
-    runBuild <| pkg.buildOleansWithDeps deps localImports
+    runBuild <| pkg.buildModuleOleansWithDeps deps localImports
   IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
   IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir)
diff --git a/Lake/Target.lean b/Lake/Target.lean
index cf2da0e24a..ccdd148376 100644
--- a/Lake/Target.lean
+++ b/Lake/Target.lean
@@ -49,12 +49,15 @@ protected def bindAsync [BindAsync m n] (self : ActiveTarget i n α) (f : i →
 protected def bindOpaqueAsync [BindAsync m n] (self : ActiveTarget i n α) (f : α → m (n β)) : m (n β) :=
   bindAsync self.task f
 
+def materializeAsync [Pure m] (self : ActiveTarget i n t) : m (n t) :=
+  pure self.task
+
 def materialize [Await n m] (self : ActiveTarget i n t) : m t :=
   await self.task
 
 def mixOpaqueAsync
 [MixTrace t] [Monad m] [Pure n] [BindAsync m n]
-(t1 t2 : ActiveTarget i n t) : m (ActiveTarget PUnit n t) := do
+(t1 : ActiveTarget α n t) (t2 : ActiveTarget β n t) : m (ActiveTarget PUnit n t) := do
   ActiveTarget.opaque <| ←
     t1.bindOpaqueAsync fun tr1 =>
     t2.bindOpaqueAsync fun tr2 =>
@@ -135,7 +138,7 @@ def build  [Await n m] [Functor m] [Bind m] (self : Target i m n t) : m i := do
 
 def mixOpaqueAsync
 [MixTrace t] [Monad m] [Pure n] [BindAsync m n]
-(t1 t2 :  Target i m n t) : Target PUnit m n t :=
+(t1 :  Target α m n t) (t2 :  Target β m n t) : Target PUnit m n t :=
   Target.opaque do
     let tk1 ← t1.materializeAsync
     let tk2 ← t2.materializeAsync