diff --git a/Lake/Build.lean b/Lake/Build.lean
index 69b98bfd26..9ca64b2667 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -33,17 +33,17 @@ abbrev ModuleTarget := LeanTarget ModuleArtifact
 namespace ModuleTarget
 
 def mk (olean c : FilePath) (hash : Hash) (mtime : IO.FS.SystemTime) (task : BuildTask) : ModuleTarget :=
-  BuildTarget.mk ⟨olean, c⟩ ⟨hash, mtime⟩ task
+  ActiveBuildTarget.mk ⟨olean, c⟩ ⟨hash, mtime⟩ task
 
 def pure (olean c : FilePath) (hash : Hash) (mtime : IO.FS.SystemTime) : ModuleTarget :=
-  BuildTarget.pure ⟨olean, c⟩ ⟨hash, mtime⟩
+  ActiveBuildTarget.pure ⟨olean, c⟩ ⟨hash, mtime⟩
 
 def oleanFile (self : ModuleTarget) := self.artifact.oleanFile
-def oleanTarget (self : ModuleTarget) : FileTarget :=
+def oleanTarget (self : ModuleTarget) : ActiveFileTarget :=
   {self with artifact := self.oleanFile, trace := self.mtime}
 
 def cFile (self : ModuleTarget) := self.artifact.cFile
-def cTarget (self : ModuleTarget) : FileTarget :=
+def cTarget (self : ModuleTarget) : ActiveFileTarget :=
   {self with artifact := self.cFile, trace := self.mtime}
 
 end ModuleTarget
@@ -85,8 +85,8 @@ def skipIf [Pure m] (cond : Bool) (build : m BuildTask) : m BuildTask := do
 def skipIfNewer [GetMTime a]
 (artifact : a) (depMTime : MTime)
 {m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m]
-(build : m BuildTask) : m (MTimeBuildTarget a) := do
-  MTimeBuildTarget.mk artifact depMTime <| ←
+(build : m BuildTask) : m (ActiveBuildTarget MTime a) := do
+  ActiveBuildTarget.mk artifact depMTime <| ←
     skipIf (← checkIfNewer artifact depMTime) build
 
 -- # Build Modules
@@ -126,7 +126,7 @@ def fetchAfterDirectLocalImports
     let cFile := pkg.modToC mod
     let oleanFile := pkg.modToOlean mod
     let importTasks := importTargets.map (·.buildTask)
-    BuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
+    ActiveBuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
       skipIf sameHash <| afterTaskList (depsTarget.buildTask :: importTasks) do
         compileOleanAndC leanFile oleanFile cFile leanPath pkg.dir pkg.leanArgs
         IO.FS.writeFile hashFile (toString fullHash)
diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean
index aea75b76e7..78aa195be3 100644
--- a/Lake/BuildBin.lean
+++ b/Lake/BuildBin.lean
@@ -11,17 +11,17 @@ namespace Lake
 -- # Build `.o` Files
 
 def buildLeanO (oFile : FilePath)
-(cTarget : BuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask :=
+(cTarget : ActiveBuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask :=
   afterTarget cTarget <| compileLeanO oFile cTarget.artifact leancArgs
 
 def fetchLeanOFileTarget (oFile : FilePath)
-(cTarget : FileTarget) (leancArgs : Array String := #[]) : IO FileTarget :=
+(cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO ActiveFileTarget :=
   skipIfNewer oFile cTarget.mtime <| buildLeanO oFile cTarget leancArgs
 
 -- # Build Package Lib
 
 def PackageTarget.fetchOFileTargets
-(self : PackageTarget) : IO (List FileTarget) := do
+(self : PackageTarget) : IO (List ActiveFileTarget) := do
   self.moduleTargets.toList.mapM fun (mod, target) => do
     let oFile := self.package.modToO mod
     fetchLeanOFileTarget (oFile) target.cTarget self.package.leancArgs
@@ -32,10 +32,10 @@ def PackageTarget.buildStaticLib
   let oFiles := oFileTargets.map (·.artifact) |>.toArray
   oFileTargets >> compileStaticLib self.package.staticLibFile oFiles
 
-def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO FileTarget := do
+def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO ActiveFileTarget := do
   skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib
 
-def Package.fetchStaticLibTarget (self : Package) : IO FileTarget := do
+def Package.fetchStaticLibTarget (self : Package) : IO ActiveFileTarget := do
   (← self.buildTarget).fetchStaticLibTarget
 
 def Package.fetchStaticLib (self : Package) : IO FilePath := do
@@ -60,10 +60,10 @@ def PackageTarget.buildBin
   linkTargets >> compileLeanBin self.package.binFile linkFiles self.package.linkArgs
 
 def PackageTarget.fetchBinTarget
-(depTargets : List PackageTarget) (self : PackageTarget) : IO FileTarget :=
+(depTargets : List PackageTarget) (self : PackageTarget) : IO ActiveFileTarget :=
   skipIfNewer self.package.binFile self.mtime <| self.buildBin depTargets
 
-def Package.fetchBinTarget (self : Package) : IO FileTarget := do
+def Package.fetchBinTarget (self : Package) : IO ActiveFileTarget := do
   let depTargets ← self.buildDepTargets
   let pkgTarget ← self.buildTargetWithDepTargets depTargets
   pkgTarget.fetchBinTarget depTargets
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index c62d8d6802..95b3469bc8 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -8,104 +8,79 @@ import Lake.BuildTrace
 
 namespace Lake
 
--- # Build Target
+-- # Active Build Target
 
-structure BuildTarget (t : Type) (a : Type) where
+structure ActiveBuildTarget (t : Type) (a : Type) where
   artifact    : a
   trace       : t
   buildTask   : BuildTask
 
 -- manually derive `Inhabited` instance because automatic deriving fails
-instance [Inhabited t] [Inhabited a] : Inhabited (BuildTarget t a) :=
+instance [Inhabited t] [Inhabited a] : Inhabited (ActiveBuildTarget t a) :=
   ⟨Inhabited.default, Inhabited.default, BuildTask.nop⟩
 
-namespace BuildTarget
+namespace ActiveBuildTarget
 
-def nil [Inhabited t] : BuildTarget t PUnit :=
+def nil [Inhabited t] : ActiveBuildTarget t PUnit :=
   ⟨(), Inhabited.default, BuildTask.nop⟩
 
-def pure (artifact : a) (trace : t) : BuildTarget t a :=
-  {artifact, trace, buildTask := BuildTask.nop}
+def pure (artifact : a) (trace : t) : ActiveBuildTarget t a :=
+  ⟨artifact, trace, BuildTask.nop⟩
 
-def opaque (trace : t) (task : BuildTask) : BuildTarget t PUnit :=
+def opaque (trace : t) (task : BuildTask) : ActiveBuildTarget t PUnit :=
   ⟨(), trace, task⟩
 
-def withTrace (trace : t) (self : BuildTarget r a) : BuildTarget t a :=
+def withTrace (trace : t) (self : ActiveBuildTarget r a) : ActiveBuildTarget t a :=
   {self with trace := trace}
 
-def discardTrace (self : BuildTarget t a) : BuildTarget PUnit a :=
+def discardTrace (self : ActiveBuildTarget t a) : ActiveBuildTarget PUnit a :=
   self.withTrace ()
 
-def withArtifact (artifact : a) (self : BuildTarget t b) : BuildTarget t a :=
-  {self with artifact := artifact}
-
-def discardArtifact (self : BuildTarget t α) : BuildTarget t PUnit :=
-  self.withArtifact ()
-
-def materialize (self : BuildTarget t α) : IO PUnit :=
-  self.buildTask.await
-
-end BuildTarget
-
-def afterTarget (target : BuildTarget t a) (act : IO PUnit)  : IO BuildTask :=
-  afterTask target.buildTask act
-
-def afterTargetList (targets : List (BuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
-  afterTaskList (targets.map (·.buildTask)) act
-
-instance : HAndThen (BuildTarget t a) (IO PUnit) (IO BuildTask) :=
-  ⟨afterTarget⟩
-
-instance : HAndThen (List (BuildTarget t a)) (IO PUnit) (IO BuildTask) :=
-  ⟨afterTargetList⟩
-
--- # MTIme Build Target
-
-abbrev MTimeBuildTarget := BuildTarget MTime
-
-namespace MTimeBuildTarget
-
-def mtime (self : MTimeBuildTarget a) :=
+def mtime (self : ActiveBuildTarget MTime a) : MTime :=
   self.trace
 
-def mk (artifact : a) (mtime : MTime := 0) (buildTask : BuildTask) : MTimeBuildTarget a :=
-  {artifact, trace := mtime, buildTask}
+def withArtifact (artifact : a) (self : ActiveBuildTarget t b) : ActiveBuildTarget t a :=
+  {self with artifact := artifact}
 
-def pure (artifact : a) (mtime : MTime := 0) : MTimeBuildTarget a :=
-  {artifact, trace := mtime, buildTask := BuildTask.nop}
+def discardArtifact (self : ActiveBuildTarget t α) : ActiveBuildTarget t PUnit :=
+  self.withArtifact ()
 
-def all (targets : List (MTimeBuildTarget a)) : IO (MTimeBuildTarget PUnit) := do
-  let depsMTime := MTime.listMax <| targets.map (·.mtime)
-  let task ← BuildTask.all <| targets.map (·.buildTask)
-  return MTimeBuildTarget.mk () depsMTime task
+def materialize (self : ActiveBuildTarget t α) : IO PUnit :=
+  self.buildTask.await
 
-def collectAll (targets : List (MTimeBuildTarget a)) : IO (MTimeBuildTarget (List a)) := do
-  let artifacts := targets.map (·.artifact)
-  let depsMTime := MTime.listMax <|  targets.map (·.mtime)
-  let task ← BuildTask.all <| targets.map (·.buildTask)
-  return MTimeBuildTarget.mk artifacts depsMTime task
+end ActiveBuildTarget
 
-end MTimeBuildTarget
+def afterTarget (target : ActiveBuildTarget t a) (act : IO PUnit)  : IO BuildTask :=
+  afterTask target.buildTask act
+
+def afterTargetList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
+  afterTaskList (targets.map (·.buildTask)) act
+
+instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTarget⟩
+
+instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTargetList⟩
 
 -- # File Target
 
 open System
 
-abbrev FileTarget := MTimeBuildTarget FilePath
+abbrev ActiveFileTarget := ActiveBuildTarget MTime FilePath
 
-namespace FileTarget
+namespace ActiveFileTarget
 
-def mk (file : FilePath) (maxMTime : MTime) (task : BuildTask) :=
-  BuildTarget.mk file maxMTime task
+def mk (file : FilePath) (depMTime : MTime) (task : BuildTask) :=
+  ActiveBuildTarget.mk file depMTime task
 
-def pure (file : FilePath) (maxMTime : MTime) :=
-  BuildTarget.pure file maxMTime
+def pure (file : FilePath) (depMTime : MTime) :=
+  ActiveBuildTarget.pure file depMTime
 
-end FileTarget
+end ActiveFileTarget
 
 -- # Lean Target
 
-abbrev LeanTarget a := BuildTarget LeanTrace a
+abbrev LeanTarget a := ActiveBuildTarget LeanTrace a
 
 namespace LeanTarget
 
@@ -116,9 +91,9 @@ def all (targets : List (LeanTarget a)) : IO (LeanTarget PUnit) := do
   let hash := Hash.foldList 0 <| targets.map (·.hash)
   let mtime := MTime.listMax <| targets.map (·.mtime)
   let task ← BuildTask.all <| targets.map (·.buildTask)
-  return BuildTarget.mk () ⟨hash, mtime⟩ task
+  return ActiveBuildTarget.mk () ⟨hash, mtime⟩ task
 
-def fromMTimeTarget (target : MTimeBuildTarget a) : LeanTarget a :=
-  {target with trace := LeanTrace.fromMTime target.mtime}
+def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a :=
+  {target with trace := LeanTrace.fromMTime target.trace}
 
 end LeanTarget
diff --git a/Lake/Package.lean b/Lake/Package.lean
index e05435a9a7..3ff00093c7 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -49,7 +49,7 @@ structure PackageConfig where
   libName : String := moduleRoot.toString (escape := false)
   depsDir : FilePath := defaultDepsDir
   dependencies : List Dependency := []
-  buildMoreDepsTarget : IO (BuildTarget LeanTrace PUnit) := BuildTarget.nil
+  buildMoreDepsTarget : IO (ActiveBuildTarget LeanTrace PUnit) := ActiveBuildTarget.nil
   scripts : HashMap String Script := HashMap.empty
   deriving Inhabited
 
@@ -83,7 +83,7 @@ def moduleRootName (self : Package) : String :=
 def dependencies (self : Package) : List Dependency :=
   self.config.dependencies
 
-def buildMoreDepsTarget (self : Package) : IO (BuildTarget LeanTrace PUnit) :=
+def buildMoreDepsTarget (self : Package) : IO (ActiveBuildTarget LeanTrace PUnit) :=
   self.config.buildMoreDepsTarget
 
 def leanArgs (self : Package) : Array String :=
diff --git a/examples/ext/package.lean b/examples/ext/package.lean
index dc2a865249..7c2131661f 100644
--- a/examples/ext/package.lean
+++ b/examples/ext/package.lean
@@ -9,11 +9,11 @@ def buildDir := defaultBuildDir
 def addO := buildDir / extDir / "add.o"
 def extLib := buildDir / extDir / "libext.a"
 
-def fetchAddOTarget : IO FileTarget := do
+def fetchAddOTarget : IO ActiveFileTarget := do
   skipIfNewer addO (← getMTime addSrc) <|
     BuildTask.spawn <| compileO addO addSrc (cmd := "c++")
 
-def fetchExtLibTarget : IO FileTarget := do
+def fetchExtLibTarget : IO ActiveFileTarget := do
   let oTarget ← fetchAddOTarget
   skipIfNewer extLib oTarget.mtime <|
     oTarget >> compileStaticLib extLib #[addO]