diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index df7bcf23bf..3b54130339 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -25,6 +25,7 @@ OPTIONS:
   --old                 only rebuild modified modules (ignore transitive deps)
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update, -U          update manifest before building
+  --reconfigure, -R     elaborate configuration files instead of using OLeans
 
 COMMANDS:
   new <name> <temp>     create a Lean package in a new directory
diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean
index 037f04d249..e4015d401a 100644
--- a/src/lake/Lake/CLI/Init.lean
+++ b/src/lake/Lake/CLI/Init.lean
@@ -22,6 +22,7 @@ def toolchainFileName : FilePath :=
 
 def gitignoreContents :=
 s!"/{defaultBuildDir}
+/{defaultConfigFile.withExtension "olean"}
 /{defaultPackagesDir}/*
 "
 
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 5f03d65e19..548f60774e 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -34,6 +34,7 @@ structure LakeOptions where
   wantsHelp : Bool := false
   verbosity : Verbosity := .normal
   updateDeps : Bool := false
+  reconfigure : Bool := false
   oldMode : Bool := false
   trustHash : Bool := true
 
@@ -65,6 +66,7 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
     configFile := opts.rootDir / opts.configFile
     configOpts := opts.configOpts
     leanOpts := Lean.Options.empty
+    reconfigure := opts.reconfigure
   }
 
 /-- Make a `BuildConfig` from a `LakeOptions`. -/
@@ -139,22 +141,24 @@ def lakeShortOption : (opt : Char) → CliM PUnit
 | 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
 | 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
 | 'U' => modifyThe LakeOptions ({· with updateDeps := true})
+| 'R' => modifyThe LakeOptions ({· with reconfigure := true})
 | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
 | 'H' => modifyThe LakeOptions ({· with trustHash := false})
 | opt => throw <| CliError.unknownShortOption opt
 
 def lakeLongOption : (opt : String) → CliM PUnit
-| "--quiet"   => modifyThe LakeOptions ({· with verbosity := .quiet})
-| "--verbose" => modifyThe LakeOptions ({· with verbosity := .verbose})
-| "--update"  => modifyThe LakeOptions ({· with updateDeps := true})
-| "--old"     => modifyThe LakeOptions ({· with oldMode := true})
-| "--rehash"  => modifyThe LakeOptions ({· with trustHash := false})
-| "--dir"     => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
-| "--file"    => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
-| "--lean"    => do setLean <| ← takeOptArg "--lean" "path or command"
-| "--help"    => modifyThe LakeOptions ({· with wantsHelp := true})
-| "--"        => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
-| opt         => throw <| CliError.unknownLongOption opt
+| "--quiet"       => modifyThe LakeOptions ({· with verbosity := .quiet})
+| "--verbose"     => modifyThe LakeOptions ({· with verbosity := .verbose})
+| "--update"      => modifyThe LakeOptions ({· with updateDeps := true})
+| "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
+| "--old"         => modifyThe LakeOptions ({· with oldMode := true})
+| "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
+| "--dir"         => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
+| "--file"        => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
+| "--lean"        => do setLean <| ← takeOptArg "--lean" "path or command"
+| "--help"        => modifyThe LakeOptions ({· with wantsHelp := true})
+| "--"            => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
+| opt             =>  throw <| CliError.unknownLongOption opt
 
 def lakeOption :=
   option {
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 5e1a59d729..55c0fc53f1 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -248,19 +248,16 @@ namespace Package
 @[inline] def deps (self : Package) : Array Package  :=
   self.opaqueDeps.map (·.get)
 
-/--
-The path for storing the package's remote dependencies relative to `dir`.
-Either its `packagesDir` configuration or `defaultPackagesDir`.
--/
-def relPkgsDir (self : Package) : FilePath :=
-  self.config.packagesDir.getD defaultPackagesDir
+/-- The path for storing the package's remote dependencies relative to `dir` (i.e., `packagesDir`). -/
+@[inline] def relPkgsDir (self : Package) : FilePath :=
+  self.config.packagesDir
 
 /-- The package's `dir` joined with its `relPkgsDir` -/
-def pkgsDir (self : Package) : FilePath :=
+@[inline] def pkgsDir (self : Package) : FilePath :=
   self.dir / self.relPkgsDir
 
 /-- The package's JSON manifest of remote dependencies. -/
-def manifestFile (self : Package) : FilePath :=
+@[inline] def manifestFile (self : Package) : FilePath :=
   self.dir / self.config.manifestFile
 
 /-- The package's `dir` joined with its `buildDir` configuration. -/
diff --git a/src/lake/Lake/Config/WorkspaceConfig.lean b/src/lake/Lake/Config/WorkspaceConfig.lean
index 98e2f0ce18..fdd00a3b8b 100644
--- a/src/lake/Lake/Config/WorkspaceConfig.lean
+++ b/src/lake/Lake/Config/WorkspaceConfig.lean
@@ -16,5 +16,5 @@ structure WorkspaceConfig where
   The directory to which Lake should download remote dependencies.
   Defaults to `defaultPackagesDir` (i.e., `lake-packages`).
   -/
-  packagesDir : Option FilePath := none
+  packagesDir : FilePath := defaultPackagesDir
   deriving Inhabited, Repr
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index d3f5a2d61c..4c38f99507 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -26,3 +26,5 @@ structure LoadConfig where
   configOpts : NameMap String := {}
   /-- The Lean options with which to elaborate the configuration file. -/
   leanOpts : Options := {}
+  /-- If true, Lake will elaborate configuration files instead of using OLeans. -/
+  reconfigure : Bool := false
diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean
index 98ea541e36..0adffeda21 100644
--- a/src/lake/Lake/Load/Elab.lean
+++ b/src/lake/Lake/Load/Elab.lean
@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lean.Elab.Frontend
 import Lake.DSL.Extensions
 import Lake.Load.Config
+import Lake.Build.Trace
 import Lake.Util.Log
 
 namespace Lake
@@ -13,19 +14,29 @@ open Lean System
 
 deriving instance BEq, Hashable for Import
 
-/- Cache for the imported header environment of Lake configuration files. -/
-initialize importEnvCache : IO.Ref (HashMap (List Import) Environment) ← IO.mkRef {}
+/- Cache for the import state of Lake configuration files. -/
+initialize importStateCache : IO.Ref (HashMap (Array Import) ImportState) ← IO.mkRef {}
+
+/--
+Like `importModulesCore`, but fetch the
+resulting import state from the cache if possible. -/
+def importModulesUsingCache (imports : Array Import) : IO ImportState := do
+  match (← importStateCache.get).find? imports with
+  | none =>
+    let (_, s) ← importModulesCore imports |>.run
+    importStateCache.modify (·.insert imports s)
+    return s
+  | some s =>
+    return s
 
 /-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
-def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
+def processHeader (header : Syntax) (opts : Options)
 (inputCtx : Parser.InputContext) : StateT MessageLog IO Environment := do
   try
     let imports := Elab.headerToImports header
-    if let some env := (← importEnvCache.get).find? imports then
-      return env
-    let env ← importModules imports opts trustLevel
-    importEnvCache.modify (·.insert imports env)
-    return env
+    withImporting do
+      let s ← importModulesUsingCache imports
+      finalizeImport s imports opts 1024
   catch e =>
     let pos := inputCtx.fileMap.toPosition <| header.getPos?.getD 0
     modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
@@ -35,19 +46,19 @@ def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
 def configModuleName : Name := `lakefile
 
 /-- Elaborate `configFile` with the given package directory and options. -/
-def elabConfigFile (pkgDir : FilePath) (configOpts : NameMap String)
+def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
 (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) : LogIO Environment := do
 
   -- Read file and initialize environment
   let input ← IO.FS.readFile configFile
   let inputCtx := Parser.mkInputContext input configFile.toString
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages
+  let (env, messages) ← processHeader header leanOpts inputCtx messages
   let env := env.setMainModule configModuleName
 
   -- Configure extensions
   let env := dirExt.setState env pkgDir
-  let env := optsExt.setState env configOpts
+  let env := optsExt.setState env lakeOpts
 
   -- Elaborate File
   let commandState := Elab.Command.mkState env messages leanOpts
@@ -65,3 +76,30 @@ def elabConfigFile (pkgDir : FilePath) (configOpts : NameMap String)
     error s!"{configFile}: package configuration has errors"
   else
     return s.commandState.env
+
+/--
+If `reconfigure` is not set and up-to-date OLean for the configuration file exists,
+import it. Otherwise, elaborate the configuration and store save it to the OLean.
+-/
+def importConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
+(leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do
+  let olean := configFile.withExtension "olean"
+  let useOLean ← id do
+    if reconfigure then return false
+    unless (← olean.pathExists) do return false
+    unless (← getMTime olean) > (← getMTime configFile) do return false
+    return true
+  if useOLean then
+    withImporting do
+    let (mod, region) ← readModuleData olean
+    let s ← importModulesUsingCache mod.imports
+    let s := {s with
+      moduleData  := s.moduleData.push mod
+      regions     := s.regions.push region
+      moduleNames := s.moduleNames.push configModuleName
+    }
+    finalizeImport s #[configModuleName] leanOpts 1024
+  else
+    let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
+    Lean.writeModule env olean
+    return env
diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index 4b84884f58..d0cf836ca2 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -24,16 +24,16 @@ namespace Lake
 
 /-- Load the tagged `Dependency` definitions from a package configuration environment. -/
 def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array Dependency) := do
-  (packageDepAttr.ext.getState env).mapM (evalConstCheck env opts Dependency ``Dependency)
+  (packageDepAttr.getAllEntries env).mapM (evalConstCheck env opts Dependency ``Dependency)
 
 /--
 Elaborate a dependency's configuration file into a `Package`.
 The resulting package does not yet include any dependencies.
 -/
 def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
-(leanOpts : Options) (lakeOpts : NameMap String) : LogIO Package := do
+(leanOpts : Options) (lakeOpts : NameMap String) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
-  let configEnv ← elabConfigFile dir lakeOpts leanOpts (dir / defaultConfigFile)
+  let configEnv ← importConfigFile dir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
     dir, config, configEnv, leanOpts
@@ -48,8 +48,11 @@ Packages are updated to latest specific revision matching that in `require`
 (e.g., if the `require` is `@master`, update to latest commit on master) or
 removed if the `require` is removed. If `tuUpdate` is empty, update/remove all
 root dependencies. Otherwise, only update the root dependencies specified.
+
+If `reconfigure`, elaborate configuration files while updating, do not use OLeans.
 -/
-def buildUpdatedManifest (ws : Workspace) (toUpdate : NameSet := {}) : LogIO Manifest := do
+def buildUpdatedManifest (ws : Workspace)
+(toUpdate : NameSet := {}) (reconfigure := true) : LogIO (Workspace × Manifest) := do
   let res ← StateT.run (s := mkNameMap MaterializedDep) <| EStateT.run' (mkNameMap Package) do
     -- Use manifest versions of root packages that should not be updated
     unless toUpdate.isEmpty do
@@ -69,7 +72,7 @@ def buildUpdatedManifest (ws : Workspace) (toUpdate : NameSet := {}) : LogIO Man
           return (pkg, dep.relPkgDir)
         else
           -- Load the package
-          let depPkg ← loadDepPackage ws.dir dep pkg.leanOpts dep.opts
+          let depPkg ← loadDepPackage ws.dir dep pkg.leanOpts dep.opts reconfigure
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
@@ -83,9 +86,10 @@ def buildUpdatedManifest (ws : Workspace) (toUpdate : NameSet := {}) : LogIO Man
       -- Resolve dependencies's dependencies recursively
       return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
   match res with
-  | (.ok _, deps) =>
+  | (.ok root, deps) =>
     let manifest : Manifest := {packagesDir? := ws.relPkgsDir}
-    return deps.fold (fun m _ d => m.insert d.manifestEntry) manifest
+    let manifest := deps.fold (fun m _ d => m.insert d.manifestEntry) manifest
+    return ({ws with root}, manifest)
   | (.error cycle, _) =>
     let cycle := cycle.map (s!"  {·}")
     error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
@@ -96,7 +100,8 @@ Does not resolve dependencies.
 -/
 def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.env.leanSearchPath
-  let configEnv ← elabConfigFile config.rootDir config.configOpts config.leanOpts config.configFile
+  let configEnv ← importConfigFile config.rootDir
+    config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let repo := GitRepo.mk config.rootDir
   let root := {
@@ -140,7 +145,7 @@ def Workspace.finalize (ws : Workspace) : LogIO Workspace := do
 Resolving a workspace's dependencies using a manifest,
 downloading and/or updating them as necessary.
 -/
-def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) : LogIO Workspace := do
+def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigure := false) : LogIO Workspace := do
   if !manifest.isEmpty && manifest.packagesDir? != some ws.relPkgsDir then
     logWarning <|
       "manifest out of date: packages directory changed, " ++
@@ -168,7 +173,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) : LogIO Wor
           | error <| s!"dependency '{dep.name}' of '{pkg.name}' not in manifest, " ++
             "use `lake update` to update"
         let result ← entry.materialize ws.dir relPkgsDir
-        loadDepPackage ws.dir result pkg.leanOpts dep.opts
+        loadDepPackage ws.dir result pkg.leanOpts dep.opts reconfigure
       return { pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·) }
   match res with
   | Except.ok root =>
@@ -183,18 +188,18 @@ elaborating its configuration file and resolving its dependencies.
 If `updateDeps` is true, updates the manifest before resolving dependencies.
 -/
 def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
+  let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
-  let manifest ← do
-    if updateDeps then
-      let manifest ← buildUpdatedManifest ws
-      manifest.saveToFile ws.manifestFile
-      pure manifest
-    else
-      Manifest.loadOrEmpty ws.manifestFile
-  ws.materializeDeps manifest
+  if updateDeps then
+    let (ws, manifest) ← buildUpdatedManifest ws {} rc
+    manifest.saveToFile ws.manifestFile
+    ws.finalize
+  else
+    ws.materializeDeps (← Manifest.loadOrEmpty ws.manifestFile) rc
 
 /-- Updates the manifest for the loaded Lake workspace (see `buildUpdatedManifest`). -/
 def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
+  let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
-  let manifest ← buildUpdatedManifest ws toUpdate
+  let (ws, manifest) ← buildUpdatedManifest ws toUpdate rc
   manifest.saveToFile ws.manifestFile
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index a206c1011f..06a42e2721 100644
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -38,21 +38,21 @@ where
 def mkTagMap
 (env : Environment) (attr : OrderedTagAttribute)
 [Monad m]  (f : Name → m α) : m (NameMap α) :=
-  attr.ext.getState env |>.foldlM (init := {}) fun map declName =>
+  attr.getAllEntries env |>.foldlM (init := {}) fun map declName =>
     return map.insert declName <| ← f declName
 
 /-- Construct a `DNameMap` from the declarations tagged with `attr`. -/
 def mkDTagMap
 (env : Environment) (attr : OrderedTagAttribute)
 [Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) :=
-  attr.ext.getState env |>.foldlM (init := {}) fun map declName =>
+  attr.getAllEntries env |>.foldlM (init := {}) fun map declName =>
     return map.insert declName <| ← f declName
 
 /-- Load a `PackageConfig` from a configuration environment. -/
 def PackageConfig.loadFromEnv
 (env : Environment) (opts := Options.empty) : Except String PackageConfig := do
   let declName ←
-    match packageAttr.ext.getState env |>.toList with
+    match packageAttr.getAllEntries env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
     | [name] => pure name
     | _ => error s!"configuration file has multiple `package` declarations"
@@ -69,7 +69,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
   let scripts : NameMap Script ← mkTagMap env scriptAttr fun name => do
     let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn name
     return {fn, doc? := (← findDocString? env name)}
-  let defaultScripts ← defaultScriptAttr.ext.getState env |>.mapM fun name =>
+  let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name =>
     if let some script := scripts.find? name then pure script else
       error s!"package is missing script `{name}` marked as a default"
   let leanLibConfigs ← IO.ofExcept <| mkTagMap env leanLibAttr fun name =>
@@ -92,7 +92,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
       else
         error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`"
     | .error e => error e
-  let defaultTargets := defaultTargetAttr.ext.getState env
+  let defaultTargets := defaultTargetAttr.getAllEntries env
 
   -- Fill in the Package
   return {self with
@@ -107,15 +107,15 @@ Load module/package facets into a `Workspace` from a configuration environment.
 def Workspace.addFacetsFromEnv
 (env : Environment) (opts : Options) (self : Workspace) : Except String Workspace := do
   let mut ws := self
-  for name in moduleFacetAttr.ext.getState env do
+  for name in moduleFacetAttr.getAllEntries env do
     match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with
     | .ok decl => ws := ws.addModuleFacetConfig <| decl.config
     | .error e => error e
-  for name in packageFacetAttr.ext.getState env do
+  for name in packageFacetAttr.getAllEntries env do
     match evalConstCheck env opts PackageFacetDecl ``PackageFacetDecl name with
     | .ok decl => ws := ws.addPackageFacetConfig <| decl.config
     | .error e => error e
-  for name in libraryFacetAttr.ext.getState env do
+  for name in libraryFacetAttr.getAllEntries env do
     match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with
     | .ok decl => ws := ws.addLibraryFacetConfig <| decl.config
     | .error e => error e
diff --git a/src/lake/Lake/Util/OrderedTagAttribute.lean b/src/lake/Lake/Util/OrderedTagAttribute.lean
index 5c4ef60d30..0e22d5f60b 100644
--- a/src/lake/Lake/Util/OrderedTagAttribute.lean
+++ b/src/lake/Lake/Util/OrderedTagAttribute.lean
@@ -43,3 +43,8 @@ def OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (env : Environment)
   match env.getModuleIdxFor? decl with
   | some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
   | none        => (attr.ext.getState env).contains decl
+
+/-- Get all tagged declaration names, both those imported and those in the current module. -/
+def OrderedTagAttribute.getAllEntries (attr : OrderedTagAttribute) (env : Environment) : Array Name :=
+  let s := attr.ext.toEnvExtension.getState env
+  s.importedEntries.concatMap id ++ s.state