diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
index d22a7c9e23..515af31d74 100644
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@@ -25,22 +25,13 @@ def Workspace.processImportList
       localImports := localImports.push mod
   return localImports
 
-/--
-Whether the package is "lean-only".
-That is, whether it has no need to build native files (e.g. `.c`).
-A package is considered lean-only if the package does not include any executable
-targets and is not precompiled.
--/
-def Package.isLeanOnly (self : Package): Bool :=
-  self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans
-
 /--
 Builds the workspace-local modules of list of imports.
 Used by `lake print-paths` to build modules for the Lean server.
 Returns the set of module dynlibs built (so they can be loaded by the server).
 
-Builds only module `.olean` and `.ilean` files if the package is "lean-only"
-(see `isLeanOnly`). Otherwise, also build `.c` files.
+Builds only module `.olean` and `.ilean` files if the package is configured
+as "Lean-only". Otherwise, also build `.c` and `.o` files.
 -/
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
   if imports.isEmpty then
@@ -53,10 +44,10 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
     let (res, bStore) ← EStateT.run BuildStore.empty <| mods.mapM fun mod =>
       if mod.shouldPrecompile then
         buildModuleTop mod &`lean.dynlib <&> (·.withoutInfo)
-      else if self.isLeanOnly then
-        buildModuleTop mod &`lean.c <&> (·.withoutInfo)
-      else
+      else if mod.isLeanOnly then
         buildModuleTop mod &`lean
+      else
+        buildModuleTop mod &`lean.o <&> (·.withoutInfo)
     let importTargets ← failOnBuildCycle res
     let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
     importTargets.forM (·.buildOpaque)
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 85195c18bd..375ccdc15b 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -75,9 +75,15 @@ the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
   -- Compute unique imports (direct × transitive)
   |>.insert &`lean.imports (mkModuleFacetBuild (·.recParseImports))
   -- Build module (`.olean` and `.ilean`)
-  |>.insert &`lean (mkModuleFacetBuild (·.recBuildLean false))
-  |>.insert &`olean (mkModuleFacetBuild (·.recBuildFacet &`lean))
-  |>.insert &`ilean (mkModuleFacetBuild (·.recBuildFacet &`lean))
+  |>.insert &`lean (mkModuleFacetBuild (fun mod => do
+    mod.recBuildLean !mod.isLeanOnly
+  ))
+  |>.insert &`olean (mkModuleFacetBuild (fun mod => do
+    mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.oleanFile)
+  ))
+  |>.insert &`ilean (mkModuleFacetBuild (fun mod => do
+    mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.ileanFile)
+  ))
   -- Build module `.c` (and `.olean` and `.ilean`)
   |>.insert &`lean.c (mkModuleFacetBuild <| fun mod => do
     mod.recBuildLean true <&> (·.withInfo mod.cFile)
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index bcd1584807..2336204abb 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -54,10 +54,10 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 module_data lean : ActiveOpaqueTarget
 
 /-- The `olean` file produced by `lean`  -/
-module_data olean : ActiveOpaqueTarget
+module_data olean : ActiveFileTarget
 
 /-- The `ilean` file produced by `lean` -/
-module_data ilean : ActiveOpaqueTarget
+module_data ilean : ActiveFileTarget
 
 /-- The C file built from the Lean file via `lean` -/
 module_data lean.c : ActiveFileTarget
diff --git a/Lake/Build/Module1.lean b/Lake/Build/Module1.lean
index 765ff545b2..957713ffd4 100644
--- a/Lake/Build/Module1.lean
+++ b/Lake/Build/Module1.lean
@@ -82,8 +82,8 @@ optionally outputting a `.c` file as well if `c` is set to `true`.
     <| ← dynlibsTarget.mixOpaqueAsync importTarget
   let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
   store (mod.mkBuildKey &`lean) modTarget
-  store (mod.mkBuildKey &`olean) modTarget
-  store (mod.mkBuildKey &`ilean) modTarget
+  store (mod.mkBuildKey &`olean) <| modTarget.withInfo mod.oleanFile
+  store (mod.mkBuildKey &`ilean) <| modTarget.withInfo mod.ileanFile
   if c then
     let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
     store (mod.mkBuildKey &`lean.c) cTarget
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
index f0fd1b0f2f..820f74c42b 100644
--- a/Lake/Config/Module.lean
+++ b/Lake/Config/Module.lean
@@ -66,6 +66,9 @@ def dynlib (self : Module) : FilePath :=
 @[inline] def shouldPrecompile (self : Module) : Bool :=
   self.pkg.precompileModules
 
+@[inline] def isLeanOnly (self : Module) : Bool :=
+  self.pkg.isLeanOnly && !self.shouldPrecompile
+
 -- ## Trace Helpers
 
 protected def getMTime (self : Module) : IO MTime := do
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 97724092f3..53b847ec3d 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -103,6 +103,16 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   precompileModules : Bool := false
 
+  /--
+  Whether the package is "Lean-only". A Lean-only package does not produce
+  native files for modules (e.g. `.c`, `.o`).
+
+  Defaults to `false`. Setting `precompileModules` to `true` will override this
+  setting and produce native files anyway (as they are needed to build module
+  dynlibs).
+  -/
+  isLeanOnly : Bool := false
+
   /--
   Additional arguments to pass to the Lean language server
   (i.e., `lean --server`) launched by `lake server`.
@@ -326,27 +336,27 @@ def IOPackager := (pkgDir : FilePath) → (args : List String) → IO PackageCon
 namespace Package
 
 /-- The package's `dependencies` configuration. -/
-def dependencies (self : Package) : Array Dependency :=
+@[inline] def dependencies (self : Package) : Array Dependency :=
   self.config.dependencies
 
 /-- The package's `extraDepTarget` configuration. -/
-def extraDepTarget (self : Package) : OpaqueTarget :=
+@[inline] def extraDepTarget (self : Package) : OpaqueTarget :=
   self.config.extraDepTarget
 
 /-- The package's `defaultFacet` configuration. -/
-def defaultFacet (self : Package) : PackageFacet :=
+@[inline] def defaultFacet (self : Package) : PackageFacet :=
    self.config.defaultFacet
 
 /-- Get the package's library configuration with the given name. -/
-def findLeanLib? (name : Name) (self : Package) : Option LeanLibConfig :=
+@[inline] def findLeanLib? (name : Name) (self : Package) : Option LeanLibConfig :=
   self.leanLibs.find? name
 
 /-- Get the package's executable configuration with the given name. -/
-def findLeanExe? (name : Name) (self : Package) : Option LeanExeConfig :=
+@[inline] def findLeanExe? (name : Name) (self : Package) : Option LeanExeConfig :=
   self.leanExes.find? name
 
 /-- Get the package's external library target with the given name. -/
-def findExternLib? (name : Name) (self : Package) : Option ExternLibConfig :=
+@[inline] def findExternLib? (name : Name) (self : Package) : Option ExternLibConfig :=
   self.externLibs.find? name
 
 /-- Get an `Array` of the package's external library targets. -/
@@ -355,59 +365,63 @@ def externLibTargets (self : Package) : Array FileTarget :=
   self.config.moreLibTargets
 
 /-- The package's `precompileModules` configuration. -/
-def precompileModules (self : Package) : Bool :=
+@[inline] def precompileModules (self : Package) : Bool :=
   self.config.precompileModules
 
+/-- The package's `isLeanOnly` configuration. -/
+@[inline] def isLeanOnly (self : Package) : Bool :=
+  self.config.isLeanOnly
+
 /-- The package's `moreServerArgs` configuration. -/
-def moreServerArgs (self : Package) : Array String :=
+@[inline] def moreServerArgs (self : Package) : Array String :=
   self.config.moreServerArgs
 
 /-- The package's `dir` joined with its `srcDir` configuration. -/
-def srcDir (self : Package) : FilePath :=
+@[inline] def srcDir (self : Package) : FilePath :=
   self.dir / self.config.srcDir
 
 /-- The package's root directory for `lean` (i.e., `srcDir`). -/
-def rootDir (self : Package) : FilePath :=
+@[inline] def rootDir (self : Package) : FilePath :=
   self.srcDir
 
 /-- The package's `dir` joined with its `buildDir` configuration. -/
-def buildDir (self : Package) : FilePath :=
+@[inline] def buildDir (self : Package) : FilePath :=
   self.dir / self.config.buildDir
 
 /-- The package's `buildDir` joined with its `oleanDir` configuration. -/
-def oleanDir (self : Package) : FilePath :=
+@[inline] def oleanDir (self : Package) : FilePath :=
   self.buildDir / self.config.oleanDir
 
 /-- The package's `moreLeanArgs` configuration. -/
-def moreLeanArgs (self : Package) : Array String :=
+@[inline] def moreLeanArgs (self : Package) : Array String :=
   self.config.moreLeanArgs
 
 /- `-O3`, `-DNDEBUG`, and `moreLeancArgs` -/
-def moreLeancArgs (self : Package) : Array String :=
+@[inline] def moreLeancArgs (self : Package) : Array String :=
   #["-O3", "-DNDEBUG"] ++ self.config.moreLeancArgs
 
 /-- The package's `buildDir` joined with its `irDir` configuration. -/
-def irDir (self : Package) : FilePath :=
+@[inline] def irDir (self : Package) : FilePath :=
   self.buildDir / self.config.irDir
 
 /-- The package's `buildDir` joined with its `libDir` configuration. -/
-def libDir (self : Package) : FilePath :=
+@[inline] def libDir (self : Package) : FilePath :=
   self.buildDir / self.config.libDir
 
 /-- The package's `buildDir` joined with its `binDir` configuration. -/
-def binDir (self : Package) : FilePath :=
+@[inline] def binDir (self : Package) : FilePath :=
   self.buildDir / self.config.binDir
 
 /-- The library configuration built into the package configuration. -/
-def builtinLibConfig (self : Package) : LeanLibConfig :=
+@[inline] def builtinLibConfig (self : Package) : LeanLibConfig :=
   self.config.toLeanLibConfig
 
 /-- The binary executable configuration built into the package configuration. -/
-def builtinExeConfig (self : Package) : LeanExeConfig :=
+@[inline] def builtinExeConfig (self : Package) : LeanExeConfig :=
   self.config.toLeanExeConfig
 
 /-- Get an `Array` of the package's modules. -/
-def getModuleArray (self : Package) : IO (Array Name) :=
+@[inline] def getModuleArray (self : Package) : IO (Array Name) :=
   self.builtinLibConfig.getModuleArray self.srcDir
 
 /-- Whether the given module is considered local to the package. -/
diff --git a/README.md b/README.md
index e839ec9574..f2577269a4 100644
--- a/README.md
+++ b/README.md
@@ -115,7 +115,8 @@ Workspace options are shared across a package and its dependencies.
 * `libDir`: The build subdirectory to which Lake should output the package's libraries. Defaults to `lib`.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executables. Defaults to `bin`.
 * `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `Target.collectOpaqueList/collectOpaqueArray` can be used combine multiple extra targets into a single `extraDepTarget`.
-* `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
+* `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
+* `isLeanOnly`: Whether the package is "Lean-only". A Lean-only package does not produce native files for modules (e.g. `.c`, `.o`). Defaults to `false`. Setting `precompileModules` to `true` will override this setting and produce native files anyway (as they are needed to build module dynlibs).
 * `moreServerArgs`:  Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
 * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files.
 * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes `-O3` and `-DNDEBUG` automatically, but you can change this by, for example, adding `-O0` and `-UNDEBUG`.