diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 21a7315bde..c0e3b2aa1d 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -11,10 +11,10 @@ namespace Lake
 
 /-! # General Utilities -/
 
-@[inline] def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
+def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
   Job.async <| (path, ·) <$> computeTrace path
 
-@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
+@[specialize] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
 (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
   let isOldMode ← getIsOldMode
   let upToDate ←
@@ -27,7 +27,7 @@ namespace Lake
     unless isOldMode do
       depTrace.writeToFile traceFile
 
-@[inline] def buildFileUnlessUpToDate (file : FilePath)
+def buildFileUnlessUpToDate (file : FilePath)
 (depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
   buildUnlessUpToDate file depTrace traceFile build
@@ -53,13 +53,13 @@ namespace Lake
 
 /-! # Common Builds -/
 
-def buildO (name : String)
+@[inline] def buildO (name : String)
 (oFile : FilePath) (srcJob : BuildJob FilePath)
 (args : Array String := #[]) (compiler : FilePath := "cc") : SchedulerM (BuildJob FilePath) :=
   buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
-     compileO name oFile srcFile args compiler
+    compileO name oFile srcFile args compiler
 
-def buildLeanO (name : String)
+@[inline] def buildLeanO (name : String)
 (oFile : FilePath) (srcJob : BuildJob FilePath)
 (args : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
   buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index ef86b5c24e..4b815d5c54 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -54,34 +54,27 @@ abbrev Module.depsFacet := `deps
 module_data deps : BuildJob (SearchPath × Array FilePath)
 
 /--
-The core compilation / elaboration of the Lean file via `lean`,
-which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`).
+The core build facet of a Lean file.
+Elaborates the Lean file via `lean` and produces all the Lean artifacts
+of the module (i.e., `olean`, `ilean`, `c`).
 Its trace just includes its dependencies.
 -/
-abbrev Module.leanBinFacet := `bin
-module_data bin : BuildJob Unit
+abbrev Module.leanArtsFacet := `leanArts
+module_data leanArts : BuildJob Unit
 
-/--
-The `leanBinFacet` combined with the module's trace
-(i.e., the trace of its `olean` and `ilean`).
-It is the facet used for building a Lean import of a module.
--/
-abbrev Module.importBinFacet := `importBin
-module_data importBin : BuildJob Unit
-
-/-- The `olean` file produced by `lean`  -/
+/-- The `olean` file produced by `lean`. -/
 abbrev Module.oleanFacet := `olean
 module_data olean : BuildJob FilePath
 
-/-- The `ilean` file produced by `lean` -/
+/-- The `ilean` file produced by `lean`. -/
 abbrev Module.ileanFacet := `ilean
 module_data ilean : BuildJob FilePath
 
-/-- The C file built from the Lean file via `lean` -/
+/-- The C file built from the Lean file via `lean`. -/
 abbrev Module.cFacet := `c
 module_data c : BuildJob FilePath
 
-/-- The object file built from `lean.c` -/
+/-- The object file built from `c`. -/
 abbrev Module.oFacet := `o
 module_data o : BuildJob FilePath
 
@@ -97,15 +90,15 @@ package_data extraDep : BuildJob Unit
 
 /-! ## Target Facets -/
 
-/-- A Lean library's Lean libraries. -/
-abbrev LeanLib.leanFacet := `lean
-library_data lean : BuildJob Unit
+/-- A Lean library's Lean artifacts (i.e., `olean`, `ilean`, `c`). -/
+abbrev LeanLib.leanArtsFacet := `leanArts
+library_data leanArts : BuildJob Unit
 
-/-- A Lean library's static binary. -/
+/-- A Lean library's static artifact. -/
 abbrev LeanLib.staticFacet := `static
 library_data static : BuildJob FilePath
 
-/-- A Lean library's shared binary. -/
+/-- A Lean library's shared artifact. -/
 abbrev LeanLib.sharedFacet := `shared
 library_data shared : BuildJob FilePath
 
diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean
index 392b162770..ee89e7483c 100644
--- a/src/lake/Lake/Build/Imports.lean
+++ b/src/lake/Lake/Build/Imports.lean
@@ -38,7 +38,7 @@ def recBuildImports (imports : Array Module)
       precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod
     else
       precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
-    modJobs := modJobs.push <| ← mod.leanBin.fetch
+    modJobs := modJobs.push <| ← mod.leanArts.fetch
   let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
   let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
   let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index 46e5227c04..549c1d661a 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -193,11 +193,8 @@ abbrev facet (facet : Name) (self : Module) : BuildInfo :=
 @[inherit_doc depsFacet] abbrev deps  (self : Module) :=
   self.facet depsFacet
 
-@[inherit_doc leanBinFacet] abbrev leanBin  (self : Module) :=
-  self.facet leanBinFacet
-
-@[inherit_doc importBinFacet] abbrev importBin (self : Module) :=
-  self.facet importBinFacet
+@[inherit_doc leanArtsFacet] abbrev leanArts  (self : Module) :=
+  self.facet leanArtsFacet
 
 @[inherit_doc oleanFacet] abbrev olean (self : Module) :=
   self.facet oleanFacet
@@ -240,9 +237,9 @@ abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
 abbrev LeanLib.modules (self : LeanLib) : BuildInfo :=
   self.facet modulesFacet
 
-@[inherit_doc leanFacet]
-abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
-  self.facet leanFacet
+@[inherit_doc leanArtsFacet]
+abbrev LeanLib.leanArts (self : LeanLib) : BuildInfo :=
+  self.facet leanArtsFacet
 
 @[inherit_doc staticFacet]
 abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index c804a011a8..0be758e74a 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -45,10 +45,10 @@ protected def LeanLib.recBuildLean
 (self : LeanLib) : IndexBuildM (BuildJob Unit) := do
   let mods ← self.modules.fetch
   mods.foldlM (init := BuildJob.nil) fun job mod => do
-    job.mix <| ← mod.leanBin.fetch
+    job.mix <| ← mod.leanArts.fetch
 
-/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
-def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
+/-- The `LibraryFacetConfig` for the builtin `leanArtsFacet`. -/
+def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
   mkFacetJobConfigSmall LeanLib.recBuildLean
 
 protected def LeanLib.recBuildStatic
@@ -96,7 +96,7 @@ the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`).
 def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
   DNameMap.empty
   |>.insert modulesFacet modulesFacetConfig
-  |>.insert leanFacet leanFacetConfig
+  |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert staticFacet staticFacetConfig
   |>.insert sharedFacet sharedFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index a6eaa7ca04..35cafbe7ee 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -15,25 +15,6 @@ open System
 
 namespace Lake
 
-def Module.buildUnlessUpToDate (mod : Module)
-(dynlibPath : SearchPath) (dynlibs : Array FilePath)
-(depTrace : BuildTrace) : BuildM PUnit := do
-  let isOldMode ← getIsOldMode
-  let argTrace : BuildTrace := pureHash mod.leanArgs
-  let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
-  let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
-  let modUpToDate ← do
-    if isOldMode then
-      srcTrace.checkAgainstTime mod
-    else
-      modTrace.checkAgainstFile mod mod.traceFile
-  let name := mod.name.toString
-  unless modUpToDate do
-    compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
-      (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean)
-  unless isOldMode do
-    modTrace.writeToFile mod.traceFile
-
 /-- Compute library directories and build external library Jobs of the given packages. -/
 def recBuildExternDynlibs (pkgs : Array Package)
 : IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do
@@ -108,7 +89,12 @@ def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Modul
 def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
   mkFacetConfig (·.recComputePrecompileImports)
 
-/-- Recursively build a module's transitive local imports and shared library dependencies. -/
+/--
+Recursively build a module's dependencies, including:
+* Transitive local imports
+* Shared libraries (e.g., `extern_lib` targets or precompiled modules)
+* `extraDepTargets` of its library
+-/
 def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Array FilePath)) := do
   let imports ← mod.imports.fetch
   let extraDepJob ← mod.lib.extraDep.fetch
@@ -117,7 +103,7 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
   let pkgs := precompileImports.foldl (·.insert ·.pkg)
     OrdPackageSet.empty |>.insert mod.pkg |>.toArray
   let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
-  let importJob ← BuildJob.mixArray <| ← imports.mapM (·.importBin.fetch)
+  let importJob ← BuildJob.mixArray <| ← imports.mapM (·.olean.fetch)
   let externDynlibsJob ← BuildJob.collectArray externJobs
   let modDynlibsJob ← BuildJob.collectArray modJobs
 
@@ -132,7 +118,7 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
     * Unix requires the file extension of the dynlib.
     * For some reason, building from the Lean server requires full paths.
       Everything else loads fine with just the augmented library path.
-    * Linux still needs the augmented path to resolve nested dependencies in dynlibs.
+    * Linux needs the augmented path to resolve nested dependencies in dynlibs.
     -/
     let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList
     let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path)
@@ -142,38 +128,41 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
 def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
   mkFacetJobConfigSmall (·.recBuildDeps)
 
-/-- Recursively build a module and its dependencies. -/
-def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) := do
+/--
+Recursively build a Lean module.
+Fetch its dependencies and then elaborate the Lean source file, producing
+all possible artifacts (i.e., `.olean`, `ilean`, and `.c`).
+-/
+def Module.recBuildLean (mod : Module) : IndexBuildM (BuildJob Unit) := do
   (← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
-    mod.buildUnlessUpToDate dynlibPath dynlibs depTrace
+    let argTrace : BuildTrace := pureHash mod.leanArgs
+    let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
+    let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
+    buildUnlessUpToDate mod modTrace mod.traceFile do
+      compileLeanModule mod.name.toString mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
+        (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean)
     return ((), depTrace)
 
-/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
-def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
-  mkFacetJobConfig (·.recBuildLeanCore)
-
-/-- The `ModuleFacetConfig` for the builtin `importBinFacet`. -/
-def Module.importBinFacetConfig : ModuleFacetConfig importBinFacet :=
-  mkFacetJobConfigSmall fun mod => do
-    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
-      return ((), mixTrace (← computeTrace mod) depTrace)
+/-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
+def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
+  mkFacetJobConfig (·.recBuildLean)
 
 /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
 def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
   mkFacetJobConfigSmall fun mod => do
-    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
+    (← mod.leanArts.fetch).bindSync fun _ depTrace =>
       return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
 def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
   mkFacetJobConfigSmall fun mod => do
-    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
+    (← mod.leanArts.fetch).bindSync fun _ depTrace =>
       return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 def Module.cFacetConfig : ModuleFacetConfig cFacet :=
   mkFacetJobConfigSmall fun mod => do
-    (← mod.leanBin.fetch).bindSync fun _ _ =>
+    (← mod.leanArts.fetch).bindSync fun _ _ =>
       -- do content-aware hashing so that we avoid recompiling unchanged C files
       return (mod.cFile, ← computeTrace mod.cFile)
 
@@ -233,8 +222,7 @@ def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert transImportsFacet transImportsFacetConfig
   |>.insert precompileImportsFacet precompileImportsFacetConfig
   |>.insert depsFacet depsFacetConfig
-  |>.insert leanBinFacet leanBinFacetConfig
-  |>.insert importBinFacet importBinFacetConfig
+  |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert oleanFacet oleanFacetConfig
   |>.insert ileanFacet ileanFacetConfig
   |>.insert cFacet cFacetConfig
diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean
index 3ef311e873..1c1a45a24c 100644
--- a/src/lake/Lake/Build/Trace.lean
+++ b/src/lake/Lake/Build/Trace.lean
@@ -28,7 +28,7 @@ class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t :
   /--  Compute the trace of some target info using information from the monadic context. -/
   computeTrace : i → m t
 
-def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t :=
+@[inline] def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t :=
   liftM <| ComputeTrace.computeTrace info
 
 class NilTrace.{u} (t : Type u) where
@@ -45,9 +45,6 @@ class MixTrace.{u} (t : Type u) where
 
 export MixTrace (mixTrace)
 
-def mixTraceM [MixTrace t] [Pure m] (t1 t2 : t) : m t :=
-  pure <| mixTrace t1 t2
-
 section
 variable [MixTrace t] [NilTrace t]
 
@@ -59,13 +56,13 @@ def mixTraceArray (traces : Array t) : t :=
 
 variable [ComputeTrace i m t]
 
-def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t :=
-  mixTraceList <$> artifacts.mapM computeTrace
+@[specialize] def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t :=
+  artifacts.foldlM (fun ts t => return mixTrace ts (← computeTrace t)) nilTrace
 
 instance [Monad m] : ComputeTrace (List i) m t := ⟨computeListTrace⟩
 
-def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t :=
-  mixTraceArray <$> artifacts.mapM computeTrace
+@[specialize] def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t :=
+  artifacts.foldlM (fun ts t => return mixTrace ts (← computeTrace t)) nilTrace
 
 instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩
 end
@@ -84,31 +81,31 @@ structure Hash where
 
 namespace Hash
 
-def ofNat (n : Nat) :=
+@[inline] def ofNat (n : Nat) :=
   mk n.toUInt64
 
-def loadFromFile (hashFile : FilePath) : IO (Option Hash) :=
-  return (← IO.FS.readFile hashFile).toNat?.map ofNat
+def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
+  (·.toNat?.map ofNat) <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 
 def nil : Hash :=
   mk <| 1723 -- same as Name.anonymous
 
 instance : NilTrace Hash := ⟨nil⟩
 
-def mix (h1 h2 : Hash) : Hash :=
+@[inline] def mix (h1 h2 : Hash) : Hash :=
   mk <| mixHash h1.val h2.val
 
 instance : MixTrace Hash := ⟨mix⟩
 
-protected def toString (self : Hash) : String :=
+@[inline] protected def toString (self : Hash) : String :=
   toString self.val
 
 instance : ToString Hash := ⟨Hash.toString⟩
 
-def ofString (str : String) :=
+@[inline] def ofString (str : String) :=
   mix nil <| mk <| hash str -- same as Name.mkSimple
 
-def ofByteArray (bytes : ByteArray) : Hash :=
+@[inline] def ofByteArray (bytes : ByteArray) : Hash :=
   ⟨hash bytes⟩
 
 end Hash
@@ -118,10 +115,10 @@ class ComputeHash (α : Type u) (m : outParam $ Type → Type v)  where
 
 instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHash⟩
 
-def pureHash [ComputeHash α Id] (a : α) : Hash :=
+@[inline] def pureHash [ComputeHash α Id] (a : α) : Hash :=
   ComputeHash.computeHash a
 
-def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
+@[inline] def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
   liftM <| ComputeHash.computeHash a
 
 instance : ComputeHash String Id := ⟨Hash.ofString⟩
@@ -131,14 +128,8 @@ def computeFileHash (file : FilePath) : IO Hash :=
 
 instance : ComputeHash FilePath IO := ⟨computeFileHash⟩
 
-/--
-  A wrapper around `FilePath` that adjusts its `ComputeHash` implementation
-  to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/
-structure TextFilePath where
-  path : FilePath
-
 /-- This is the same as `String.replace text "\r\n" "\n"`, but more efficient. -/
-partial def crlf2lf (text : String) : String :=
+@[inline] partial def crlf2lf (text : String) : String :=
   go "" 0 0
 where
   go (acc : String) (accStop pos : String.Pos) : String :=
@@ -154,14 +145,26 @@ where
       else
         go acc accStop pos'
 
-instance : ComputeHash TextFilePath IO where
-  computeHash file := do
-    let text ← IO.FS.readFile file.path
-    let text := crlf2lf text
-    return Hash.ofString text
+def computeTextFileHash (file : FilePath) : IO Hash := do
+  let text ← IO.FS.readFile file
+  let text := crlf2lf text
+  return Hash.ofString text
 
-instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m where
-  computeHash ar := ar.foldlM (fun b a => Hash.mix b <$> computeHash a) Hash.nil
+/--
+  A wrapper around `FilePath` that adjusts its `ComputeHash` implementation
+  to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/
+structure TextFilePath where
+  path : FilePath
+
+instance : Coe TextFilePath FilePath := ⟨(·.path)⟩
+
+instance : ComputeHash TextFilePath IO where
+  computeHash file := computeTextFileHash file
+
+@[specialize] def computeArrayHash [ComputeHash α m] [Monad m] (xs : Array α) : m Hash :=
+  xs.foldlM (fun h a => return h.mix (← computeHash a)) .nil
+
+instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m := ⟨computeArrayHash⟩
 
 --------------------------------------------------------------------------------
 /-! # Modification Time (MTime) Trace -/
@@ -196,15 +199,15 @@ class GetMTime (α) where
 export GetMTime (getMTime)
 instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩
 
-def getFileMTime (file : FilePath) : IO MTime :=
+@[inline] def getFileMTime (file : FilePath) : IO MTime :=
   return (← file.metadata).modified
 
 instance : GetMTime FilePath := ⟨getFileMTime⟩
 instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩
 
 /-- Check if the info's `MTIme` is at least `depMTime`. -/
-def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
-  (do pure ((← getMTime info) >= depMTime : Bool)).catchExceptions fun _ => pure false
+@[inline] def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
+  (return (depMTime < (← getMTime info) : Bool)).catchExceptions fun _ => pure false
 
 --------------------------------------------------------------------------------
 /-! # Lake Build Trace (Hash + MTIme) -/
@@ -218,34 +221,22 @@ structure BuildTrace where
 
 namespace BuildTrace
 
-def withHash (hash : Hash) (self : BuildTrace) : BuildTrace :=
-  {self with hash}
-
-def withoutHash (self : BuildTrace) : BuildTrace :=
-  {self with hash := Hash.nil}
-
-def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace :=
-  {self with mtime}
-
-def withoutMTime (self : BuildTrace) : BuildTrace :=
-  {self with mtime := 0}
-
-def fromHash (hash : Hash) : BuildTrace :=
+@[inline] def ofHash (hash : Hash) : BuildTrace :=
   mk hash 0
 
-instance : Coe Hash BuildTrace := ⟨fromHash⟩
+instance : Coe Hash BuildTrace := ⟨ofHash⟩
 
-def fromMTime (mtime : MTime) : BuildTrace :=
+@[inline] def ofMTime (mtime : MTime) : BuildTrace :=
   mk Hash.nil mtime
 
-instance : Coe MTime BuildTrace := ⟨fromMTime⟩
+instance : Coe MTime BuildTrace := ⟨ofMTime⟩
 
 def nil : BuildTrace :=
   mk Hash.nil 0
 
 instance : NilTrace BuildTrace := ⟨nil⟩
 
-def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
+@[specialize] def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
   return mk (← computeHash info) (← getMTime info)
 
 instance [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] : ComputeTrace i IO BuildTrace := ⟨compute⟩
@@ -256,35 +247,34 @@ def mix (t1 t2 : BuildTrace) : BuildTrace :=
 instance : MixTrace BuildTrace := ⟨mix⟩
 
 /--
-Check the build trace against the given target info and hash
-to see if the target is up-to-date.
+Check if the info is up-to-date using a hash.
+That is, check that info exists and its input hash matches this trace's hash.
 -/
-def checkAgainstHash [CheckExists i]
+@[inline] def checkAgainstHash [CheckExists i]
 (info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool :=
   pure (hash == self.hash) <&&> checkExists info
 
 /--
-Check the build trace against the given target info and its modification time
-to see if the target is up-to-date.
+Check if the info is up-to-date using modification time.
+That is, check if the info is newer than this input trace's modification time.
 -/
-def checkAgainstTime [CheckExists i] [GetMTime i]
+@[inline] def checkAgainstTime [GetMTime i]
 (info : i) (self : BuildTrace) : BaseIO Bool :=
   checkIfNewer info self.mtime
 
 /--
-Check the build trace against the given target info and its trace file
-to see if the target is up-to-date.
+Check if the info is up-to-date using a trace file.
+If the file exists, match its hash to this trace's hash.
+If not, check if the info is newer than this trace's modification time.
 -/
-def checkAgainstFile [CheckExists i] [GetMTime i]
+@[inline] def checkAgainstFile [CheckExists i] [GetMTime i]
 (info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do
-  let act : IO _ := do
-    if let some hash ← Hash.loadFromFile traceFile then
-      self.checkAgainstHash info hash
-    else
-      return self.mtime < (← getMTime info)
-  act.catchExceptions fun _ => pure false
+  if let some hash ← Hash.load? traceFile then
+    self.checkAgainstHash info hash
+  else
+    self.checkAgainstTime info
 
-def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
+@[inline] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
   IO.FS.writeFile traceFile self.hash.toString
 
 end BuildTrace
diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean
index 0f57189588..1f44d45cb1 100644
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@@ -52,7 +52,7 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
 open Module in
 def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec :=
   if facet.isAnonymous then
-    return mkBuildSpec <| mod.facet leanBinFacet
+    return mkBuildSpec <| mod.facet leanArtsFacet
   else if let some config := ws.findModuleFacetConfig? facet then do
     mkConfigBuildSpec "module" (mod.facet facet) config rfl
   else
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index f94491a5c1..b87912a667 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -79,20 +79,23 @@ The optional `@` and `+` markers can be used to disambiguate packages
 and modules from other kinds of targets (i.e., executables and libraries).
 
 LIBRARY FACETS:         build the library's ...
-  lean (default)        Lean binaries (*.olean, *.ilean files)
-  static                static binary (*.a file)
-  shared                shared binary (*.so, *.dll, or *.dylib file)
+  leanArts (default)    Lean artifacts (*.olean, *.ilean, *.c files)
+  static                static artifact (*.a file)
+  shared                shared artifact (*.so, *.dll, or *.dylib file)
 
 MODULE FACETS:          build the module's ...
-  deps                  transitive local imports & shared library dependencies
-  bin (default)         Lean binaries (*.olean, *.ilean files) and *.c file
-  o                     *.o object file (of its C file)
+  deps                  dependencies (e.g., imports, shared libraries, etc.)
+  leanArts (default)    Lean artifacts (*.olean, *.ilean, *.c files)
+  olean                 OLean (binary blob of Lean data for importers)
+  ilean                 ILean (binary blob of metadata for the Lean LSP server)
+  c                     compiled C file
+  o                     compiled object file (of its C file)
   dynlib                shared library (e.g., for `--load-dynlib`)
 
 TARGET EXAMPLES:        build the ...
   a                     default facet of target `a`
   @a                    default target(s) of package `a`
-  +A                    olean and .ilean files of module `A`
+  +A                    Lean artifacts of module `A`
   a/b                   default facet of target `b` of package `a`
   a/+A:c                C file of module `A` of package `a`
   :foo                  facet `foo` of the root package
diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean
index 85425bd824..0a17c98ab6 100644
--- a/src/lake/Lake/Config/LeanLibConfig.lean
+++ b/src/lake/Lake/Config/LeanLibConfig.lean
@@ -68,7 +68,7 @@ structure LeanLibConfig extends LeanConfig where
   An `Array` of library facets to build on a bare `lake build` of the library.
   For example, `#[LeanLib.sharedLib]` will build the shared library facet.
   -/
-  defaultFacets : Array Name := #[LeanLib.leanFacet]
+  defaultFacets : Array Name := #[LeanLib.leanArtsFacet]
 
   /--
   An `Array` of module facets to build and combine into the library's static
diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean
index f0cbc95184..814d2ddb2f 100644
--- a/src/lake/Lake/Config/Module.lean
+++ b/src/lake/Lake/Config/Module.lean
@@ -119,16 +119,11 @@ abbrev pkg (self : Module) : Package :=
 /-! ## Trace Helpers -/
 
 protected def getMTime (self : Module) : IO MTime := do
-  return mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)
+  return mixTrace (mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)) (← getMTime self.cFile)
 
 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)
+  return (← checkExists self.oleanFile) && (← checkExists self.ileanFile) && (← checkExists self.cFile)
 
 instance : CheckExists Module := ⟨Module.checkExists⟩
diff --git a/src/lake/Lake/Util/Error.lean b/src/lake/Lake/Util/Error.lean
index 5e353ad2fe..127242ecea 100644
--- a/src/lake/Lake/Util/Error.lean
+++ b/src/lake/Lake/Util/Error.lean
@@ -26,7 +26,7 @@ instance : MonadError (Except String) where
 Perform an EIO action.
 If it throws an error, invoke `error` with its string representation.
 -/
-protected def MonadError.runEIO [Monad m]
+@[inline] protected def MonadError.runEIO [Monad m]
 [MonadError m] [MonadLiftT BaseIO m] [ToString ε] (x : EIO ε α) : m α := do
   match (← x.toBaseIO) with
   | Except.ok a => pure a
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index 58f4178d94..0797787e5f 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -29,10 +29,10 @@ class MonadLog (m : Type u → Type v) where
 
 export MonadLog (log getVerbosity)
 
-def getIsVerbose [Functor m] [MonadLog m] : m Bool :=
+@[inline] def getIsVerbose [Functor m] [MonadLog m] : m Bool :=
   getVerbosity <&> (· == .verbose)
 
-def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
+@[inline] def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
   getVerbosity <&> (· == .quiet)
 
 @[inline] def logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do
@@ -41,41 +41,41 @@ def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
 @[inline] def logInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do
   if !(← getIsQuiet) then log message .info
 
-abbrev logWarning [MonadLog m] (message : String) : m PUnit :=
+@[inline] def logWarning [MonadLog m] (message : String) : m PUnit :=
   log message .warning
 
-abbrev logError  [MonadLog m] (message : String) : m PUnit :=
+@[inline] def logError  [MonadLog m] (message : String) : m PUnit :=
   log message .error
 
 namespace MonadLog
 
-def nop [Pure m] : MonadLog m :=
+@[specialize] def nop [Pure m] : MonadLog m :=
   ⟨pure .normal, fun _ _ => pure ()⟩
 
 instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
 
-def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+@[specialize] def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
   getVerbosity := (pure verbosity : BaseIO _)
   log msg
     | .info => IO.println msg.trim |>.catchExceptions fun _ => pure ()
     | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
 
-def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+@[specialize] def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
   getVerbosity := (pure verbosity : BaseIO _)
   log msg
     | .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
 
-def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
+@[specialize] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
   getVerbosity := liftM <| self.getVerbosity
   log msg lv := liftM <| self.log msg lv
 
 instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
 
 /-- Log the given error message and then fail. -/
-protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
+@[inline] protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
   logError msg *> failure
 
 end MonadLog
@@ -92,11 +92,11 @@ instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
   getVerbosity := do (← read).getVerbosity
   log msg lv := do (← read).log msg lv
 
-abbrev MonadLogT.adaptMethods [Monad n]
+@[inline] def MonadLogT.adaptMethods [Monad n]
 (f : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α :=
   ReaderT.adapt f self
 
-abbrev MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
+@[inline] def  MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
   self MonadLog.nop
 
 abbrev LogIO :=
diff --git a/src/lake/Lake/Util/OptionIO.lean b/src/lake/Lake/Util/OptionIO.lean
index e1ba2d74ba..c32bb362c3 100644
--- a/src/lake/Lake/Util/OptionIO.lean
+++ b/src/lake/Lake/Util/OptionIO.lean
@@ -46,5 +46,5 @@ instance : Alternative OptionIO where
     | some a => h (some a) <&> ((a, ·))
     | none => h none *> failure
 
-def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
+@[inline] def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
   self.toBaseIO.asTask prio