diff --git a/src/Lean.lean b/src/Lean.lean
index 83d95a42b814..ee1385321036 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -37,3 +37,4 @@ import Lean.SubExpr
 import Lean.LabelAttribute
 import Lean.AddDecl
 import Lean.Replay
+import Lean.PrivateName
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 6210a0ebacfb..664f7bf599fd 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.CoreM
+import Lean.Language.Basic
+import Lean.Elab.Exception
 
 namespace Lean
 
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 4a06fbc2c70f..03d2ad0d3d66 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -165,7 +165,7 @@ namespace TagAttribute
 def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
   match env.getModuleIdxFor? decl with
   | some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
-  | none        => (attr.ext.getState env).contains decl
+  | none        => (attr.ext.getState (asyncMode := .local) env).contains decl
 
 end TagAttribute
 
@@ -212,13 +212,14 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
 
 namespace ParametricAttribute
 
-def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
+def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name)
+    (asyncMode := attr.ext.toEnvExtension.asyncMode) : Option α :=
   match env.getModuleIdxFor? decl with
   | some modIdx =>
     match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, val) => some val
     | none          => none
-  | none        => (attr.ext.getState env).find? decl
+  | none        => (attr.ext.getState (asyncMode := asyncMode) env).find? decl
 
 def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
@@ -279,12 +280,12 @@ def getValue [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl
     match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, val) => some val
     | none          => none
-  | none        => (attr.ext.getState env).find? decl
+  | none        => (attr.ext.findStateAsync env decl).find? decl
 
 def setValue (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
     Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module")
-  else if ((attrs.ext.getState env).find? decl).isSome then
+  else if ((attrs.ext.findStateAsync env decl).find? decl).isSome then
     Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, attribute has already been set")
   else
     Except.ok (attrs.ext.addEntry env (decl, val))
@@ -353,6 +354,7 @@ private def AttributeExtension.addImported (es : Array (Array AttributeExtension
 private def addAttrEntry (s : AttributeExtensionState) (e : AttributeExtensionOLeanEntry × AttributeImpl) : AttributeExtensionState :=
   { s with map := s.map.insert e.2.name e.2, newEntries := e.1 :: s.newEntries }
 
+-- asynchrony: updated only during environment creation and commond-level `declare_syntax_cat`
 builtin_initialize attributeExtension : AttributeExtension ←
   registerPersistentEnvExtension {
     mkInitial       := AttributeExtension.mkInitial
@@ -383,14 +385,14 @@ def getBuiltinAttributeApplicationTime (n : Name) : IO AttributeApplicationTime
   pure attr.applicationTime
 
 def isAttribute (env : Environment) (attrName : Name) : Bool :=
-  (attributeExtension.getState env).map.contains attrName
+  (attributeExtension.getState (asyncMode := .local) env).map.contains attrName
 
 def getAttributeNames (env : Environment) : List Name :=
-  let m := (attributeExtension.getState env).map
+  let m := (attributeExtension.getState (asyncMode := .local) env).map
   m.fold (fun r n _ => n::r) []
 
 def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl :=
-  let m := (attributeExtension.getState env).map
+  let m := (attributeExtension.getState (asyncMode := .local) env).map
   match m[attrName]? with
   | some attr => pure attr
   | none      => throw ("unknown attribute '" ++ toString attrName ++ "'")
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index e591e7805d25..1f23aff1e178 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -53,6 +53,7 @@ end ClassState
 Type class environment extension
 -/
 -- TODO: add support for scoped instances
+-- asynchrony: set only by command-level `@[class]`
 builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ←
   registerSimplePersistentEnvExtension {
     addEntryFn    := ClassState.addEntry
@@ -62,11 +63,11 @@ builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry Clas
 /-- Return `true` if `n` is the name of type class in the given environment. -/
 @[export lean_is_class]
 def isClass (env : Environment) (n : Name) : Bool :=
-  (classExtension.getState env).outParamMap.contains n
+  (classExtension.getState (asyncMode := .local) env).outParamMap.contains n
 
 /-- If `declName` is a class, return the position of its `outParams`. -/
 def getOutParamPositions? (env : Environment) (declName : Name) : Option (Array Nat) :=
-  (classExtension.getState env).outParamMap.find? declName
+  (classExtension.getState (asyncMode := .local) env).outParamMap.find? declName
 
 /-- Return `true` if the given `declName` is a type class with output parameters. -/
 @[export lean_has_out_params]
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index e719dd4b69f8..9a0ab0c305e9 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -59,7 +59,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
   return { arity? := arity?, entries := entries.toList }
 
 @[extern "lean_add_extern"]
-opaque addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
+private opaque addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
 
 builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
   registerParametricAttribute {
diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index 9d2aae8115d0..4df8462f77bf 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -18,7 +18,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
     let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
-    let fnDecl ← getConstInfo fnName
+    let fnDecl ← getConstVal fnName
     unless decl.levelParams.length == fnDecl.levelParams.length do
       throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"
     let declType := decl.type
diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean
index 66f79ad1a2e3..e484404506a9 100644
--- a/src/Lean/Compiler/Old.lean
+++ b/src/Lean/Compiler/Old.lean
@@ -31,12 +31,11 @@ def getDeclNamesForCodeGen : Declaration → List Name
   | Declaration.axiomDecl { name := n, .. }  => [n] -- axiom may be tagged with `@[extern ...]`
   | _                                        => []
 
-def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=
-match env.find? n with
-  | (some (ConstantInfo.defnInfo _))   => Except.ok ()
-  | (some (ConstantInfo.opaqueInfo _)) => Except.ok ()
-  | none => Except.error s!"unknown declaration '{n}'"
-  | _    => Except.error s!"declaration is not a definition '{n}'"
+def checkIsDefinition (env : Environment) (n : Name) : Except String Unit := do
+  let some info := env.findAsync? n
+    | throw s!"declaration is not a definition '{n}'"
+  unless info.kind matches .defn | .opaque do
+    throw s!"unknown declaration '{n}'"
 
 /--
   We generate auxiliary unsafe definitions for regular recursive definitions.
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index cd4817682de9..706bb6dc53a3 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -193,7 +193,7 @@ protected def withFreshMacroScope (x : CoreM α) : CoreM α := do
 
 instance : MonadQuotation CoreM where
   getCurrMacroScope   := return (← read).currMacroScope
-  getMainModule       := return (← get).env.mainModule
+  getMainModule       := return (← getEnv).mainModule
   withFreshMacroScope := Core.withFreshMacroScope
 
 instance : Elab.MonadInfoTree CoreM where
@@ -210,7 +210,7 @@ instance : Elab.MonadInfoTree CoreM where
 @[inline] def modifyInstLevelValueCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit :=
   modifyCache fun ⟨c₁, c₂⟩ => ⟨c₁, f c₂⟩
 
-def instantiateTypeLevelParams (c : ConstantInfo) (us : List Level) : CoreM Expr := do
+def instantiateTypeLevelParams (c : ConstantVal) (us : List Level) : CoreM Expr := do
   if let some (us', r) := (← get).cache.instLevelType.find? c.name then
     if us == us' then
       return r
@@ -426,6 +426,11 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact d
         traceState := { tid }
         snapshotTasks := #[]
       }
+      modify fun st => { st with
+        messages := st.messages.markAllReported
+        traceState := { tid }
+        snapshotTasks := #[]
+      }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
index 76566d950bce..2bf54b277b8d 100644
--- a/src/Lean/DeclarationRange.lean
+++ b/src/Lean/DeclarationRange.lean
@@ -20,11 +20,10 @@ def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRange
   builtinDeclRanges.modify (·.insert declName declRanges)
 
 def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit := do
-  unless declRangeExt.contains (← getEnv) declName do
-    modifyEnv fun env => declRangeExt.insert env declName declRanges
+  modifyEnv fun env => declRangeExt.insert env declName declRanges
 
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
-  return declRangeExt.find? (← getEnv) declName
+  return declRangeExt.find? (asyncMode := .async) (← getEnv) declName
 
 def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 9c880cdfbbd4..f8ac16214f97 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -96,7 +96,8 @@ partial def quoteAutoTactic : Syntax → CoreM Expr
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
-    let name ← MonadQuotation.addMacroScope `_auto
+    let name := (← getDeclName?).getD .anonymous ++ `_auto
+    let name ← MonadQuotation.addMacroScope name
     let type := Lean.mkConst `Lean.Syntax
     let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index a31fdcffa024..5c3408fac455 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -135,12 +135,10 @@ private def cleanupOfNat (type : Expr) : MetaM Expr := do
 Elaborates only the declaration view headers. We have to elaborate the headers first because we
 support mutually recursive declarations in Lean 4.
 -/
-private def elabHeaders (views : Array DefView)
+private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandDeclIdResult)
     (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)))
     (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) :
     TermElabM (Array DefViewElabHeader) := do
-  let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
-    Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
   withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
     let mut headers := #[]
     -- Can we reuse the result for a body? For starters, all headers (even those below the body)
@@ -415,7 +413,9 @@ private def useProofAsSorry (k : DefKind) : CoreM Bool := do
         return true
   return false
 
-private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (sc : Command.Scope) : TermElabM (Array Expr) :=
+private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr)
+    (sc : Command.Scope) :
+    TermElabM (Array Expr) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
     if let some snap := header.bodySnap? then
@@ -1010,43 +1010,96 @@ where
   go := do
     let bodyPromises ← views.mapM fun _ => IO.Promise.new
     let tacPromises ← views.mapM fun _ => IO.Promise.new
+    let valPromise ← IO.Promise.new
     let scopeLevelNames ← getLevelNames
-    let headers ← elabHeaders views bodyPromises tacPromises
+    let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
+      Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
+    let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
     let allUserLevelNames := getAllUserLevelNames headers
     withFunLocalDecls headers fun funFVars => do
       for view in views, funFVar in funFVars do
         addLocalVarInfo view.declId funFVar
-      let values ←
+      let mut async? := none
+      if let (#[view], #[declId]) := (views, expandedDeclIds) then
+        if Elab.async.get (← getOptions) && view.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then
+          let env ← getEnv
+          let async ← env.addConstAsync declId.declName .thm
+          modifyEnv fun _=> async.mainEnv
+          async? := some async
+
+          -- TODO: parallelize? must refactor auto implicits catch, makes `@[simp]` etc harder?
+          let header := headers[0]!
+          let type ← withHeaderSecVars vars sc #[header] fun vars => do
+            mkForallFVars vars header.type >>= instantiateMVars
+          let type ← withLevelNames allUserLevelNames <| levelMVarToParam type
+          let mut s : CollectLevelParams.State := {}
+          s := collectLevelParams s type
+          let levelParams ← IO.ofExcept <| sortDeclLevelParams scopeLevelNames allUserLevelNames s.params
+          async.commitSignature { name := header.declName, levelParams, type }
+
+      let finishElab headers :=
         try
-          let values ← elabFunValues headers vars sc
-          Term.synthesizeSyntheticMVarsNoPostponing
-          values.mapM (instantiateMVarsProfiling ·)
-        catch ex =>
-          logException ex
-          headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
-      let headers ← headers.mapM instantiateMVarsAtHeader
-      let letRecsToLift ← getLetRecsToLift
-      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-      checkLetRecsToLiftTypes funFVars letRecsToLift
-      (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
-        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-        checkAllDeclNamesDistinct preDefs
-        for preDef in preDefs do
-          trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
-        let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
-        let preDefs ← instantiateMVarsAtPreDecls preDefs
-        let preDefs ← shareCommonPreDefs preDefs
-        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-        for preDef in preDefs do
-          trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
-        addPreDefinitions preDefs
+          let values ← try
+            let values ← elabFunValues headers vars sc
+            Term.synthesizeSyntheticMVarsNoPostponing
+            values.mapM (instantiateMVarsProfiling ·)
+          catch ex =>
+            logException ex
+            headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
+          if let #[value] := values then
+            valPromise.resolve value
+          let headers ← headers.mapM instantiateMVarsAtHeader
+          let letRecsToLift ← getLetRecsToLift
+          let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+          checkLetRecsToLiftTypes funFVars letRecsToLift
+          (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
+            let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+            checkAllDeclNamesDistinct preDefs
+            for preDef in preDefs do
+              trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+            let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs
+            let preDefs ← instantiateMVarsAtPreDecls preDefs
+            let preDefs ← shareCommonPreDefs preDefs
+            let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+            for preDef in preDefs do
+              trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
+            addPreDefinitions preDefs
+            if let some async := async? then
+              async.commitConst (← getEnv)
+        finally
+          valPromise.resolve (Expr.const `failedAsyncElab [])
+      let checkAndCompile :=
         processDeriving headers
-    for view in views, header in headers do
+        if let some async := async? then
+          async.commitCheckEnv (← getEnv)
+      if let some async := async? then
+        let headers := headers.map fun header => { header with modifiers.attrs := #[] }
+        let act ← wrapAsyncAsSnapshot (desc := s!"elaborating proof of {expandedDeclIds[0]?.map (·.declName) |>.get!}") fun _ => do
+          modifyEnv fun _ => async.asyncEnv
+          finishElab headers
+          let checkAct ← wrapAsyncAsSnapshot (desc := s!"finishing proof of {expandedDeclIds[0]?.map (·.declName) |>.get!}") fun _ => do
+            checkAndCompile
+          let checkTask ← BaseIO.mapTask (t := (← getEnv).checked) fun _ => checkAct
+          Core.logSnapshotTask { range? := none, task := checkTask }
+        Core.logSnapshotTask { range? := none, task := (← BaseIO.asTask act) }
+        for view in views, declId in expandedDeclIds do
+          applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
+          applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
+      else
+        let env ← getEnv
+        let headers := headers.map fun header => { header with
+          modifiers.attrs := header.modifiers.attrs.filter fun attr =>
+            getAttributeImpl env attr.name |>.map (·.applicationTime != .afterCompilation) |>.toOption |>.getD false
+        }
+        finishElab headers
+        checkAndCompile
+        for view in views, declId in expandedDeclIds do
+          applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
+    for view in views, declId in expandedDeclIds do
       -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
       -- that depends only on a part of the ref
-      addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref
-
+      addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
@@ -1097,14 +1150,19 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
       }
       reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
     views := views.push view
-  if let some snap := snap? then
-    -- no non-fatal diagnostics at this point
-    snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
-  let sc ← getScope
-  runTermElabM fun vars => Term.elabMutualDef vars sc views
+    let sc ← getScope
+    runTermElabM fun vars => do
+      if let some snap := snap? then
+        -- no non-fatal diagnostics at this point
+        snap.new.resolve <| .ofTyped {
+            desc := s!"{decl_name%}: {views.map (·.declId)}"
+            defs
+            diagnostics := .empty : DefsParsedSnapshot }
+      Term.elabMutualDef vars sc views
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure
+  registerTraceClass `Elab.async
 
 end Command
 end Lean.Elab
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 2948a36f6117..4ad93ad47822 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -79,8 +79,7 @@ where
   -- makes infoview hovers and the like work. This technique only works because the names are known
   -- to be global constants, so we don't need the local context.
   showName (env : Environment) (n : Name) : MessageData :=
-      let params :=
-        env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+      let params := env.find? n |>.map (·.levelParams.map Level.param) |>.getD []
       .ofFormatWithInfos {
         fmt := "'" ++ .tag 0 (format n) ++ "'",
         infos :=
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 2bd384167e2d..e6c0887f1828 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -416,12 +416,13 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (
     trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
     let name := (Name.str declName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
-    let value ← mkEqnProof declName type tryRefl
-    let (type, value) ← removeUnusedEqnHypotheses type value
-    addDecl <| Declaration.thmDecl {
-      name, type, value
-      levelParams := info.levelParams
-    }
+    realizeConst declName name .thm do
+      let value ← mkEqnProof declName type tryRefl
+      let (type, value) ← removeUnusedEqnHypotheses type value
+      return .thmInfo {
+        name, type, value
+        levelParams := info.levelParams
+      }
   return thmNames
 
 /--
@@ -466,20 +467,22 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
+  let baseName := declName
+  let name := Name.str baseName unfoldThmSuffix
   withOptions (tactic.hygienic.set · false) do
-    let baseName := declName
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
       let goal ← mkFreshExprSyntheticOpaqueMVar type
+      -- TODO: calls getEqnsFor!!!
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := Name.str baseName unfoldThmSuffix
-      addDecl <| Declaration.thmDecl {
-        name, type, value
-        levelParams := info.levelParams
-      }
+      realizeConst declName name .thm do
+        return .thmInfo {
+          name, type, value
+          levelParams := info.levelParams
+        }
       return name
 
 def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 94c6ee45ce58..d33d2137edfd 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -139,13 +139,13 @@ private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array
     else
       return preDef
 
-private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
+private def addSorried (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
-    let decl := Declaration.axiomDecl {
+    let decl := Declaration.thmDecl {
       name        := preDef.declName,
       levelParams := preDef.levelParams,
       type        := preDef.type,
-      isUnsafe    := preDef.modifiers.isUnsafe
+      value       := (← mkSorry (synthetic := true) preDef.type)
     }
     addDecl decl
     withSaveInfoContext do  -- save new env
@@ -260,10 +260,10 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
           -/
           let preDef ← eraseRecAppSyntax preDefs[0]!
           ensureEqnReservedNamesAvailable preDef.declName
-          if preDef.modifiers.isNoncomputable then
-            addNonRec preDef
-          else
-            addAndCompileNonRec preDef
+            if preDef.modifiers.isNoncomputable then
+              addNonRec preDef
+            else
+              addAndCompileNonRec preDef
           preDef.termination.ensureNone "not recursive"
         else if preDefs.any (·.modifiers.isUnsafe) then
           addAndCompileUnsafe preDefs
@@ -306,9 +306,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
                   catch _ =>
                     -- Compilation failed try again just as axiom
                     s.restore
-                    addAsAxioms preDefs
+                    addSorried preDefs
               else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
-                addAsAxioms preDefs
+                addSorried preDefs
             catch _ => s.restore
 
 builtin_initialize
diff --git a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
index 1f650a707f7f..0f8503773912 100644
--- a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
@@ -25,10 +25,11 @@ private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSu
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)
       let name := declName ++ suffix
-      addDecl <| Declaration.thmDecl {
-        name, type, value
-        levelParams := info.levelParams
-      }
+      realizeConst declName name .thm do
+        return .thmInfo {
+          name, type, value
+          levelParams := info.levelParams
+        }
       return some name
   else
     return none
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index b3e039ae9fd6..d2d74c1d7018 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -74,12 +74,14 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
     thmNames := thmNames.push name
+    -- may need to realize e.g. equations of a contained matcher so can't be inside `realizeConst`
     let value ← mkProof info.declName type
-    let (type, value) ← removeUnusedEqnHypotheses type value
-    addDecl <| Declaration.thmDecl {
-      name, type, value
-      levelParams := info.levelParams
-    }
+    realizeConst baseName name .thm do
+      let (type, value) ← removeUnusedEqnHypotheses type value
+      return .thmInfo {
+        name, type, value
+        levelParams := info.levelParams
+      }
   return thmNames
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index e638e737fa12..0a936dc48ffa 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -776,7 +776,7 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
   let us ← mkFreshLevelMVars ctorVal.levelParams.length
   let val  := Lean.mkConst ctorVal.name us
-  let type ← instantiateTypeLevelParams (ConstantInfo.ctorInfo ctorVal) us
+  let type ← instantiateTypeLevelParams ctorVal.toConstantVal us
   let r ← mkCtorHeaderAux ctorVal.numParams type val #[] #[]
   propagateExpectedType r.ctorFnType ctorVal.numFields expectedType?
   synthesizeAppInstMVars r.instMVars r.ctorFn
diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean
index 011fabf5126d..7444d5abcde9 100644
--- a/src/Lean/Elab/Tactic/Doc.lean
+++ b/src/Lean/Elab/Tactic/Doc.lean
@@ -71,8 +71,7 @@ only works for global constants, as the local context is not included.
 -/
 private def showParserName (n : Name) : MetaM MessageData := do
   let env ← getEnv
-  let params :=
-    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+  let params := env.find? n |>.map (·.levelParams.map Level.param) |>.getD []
   let tok ←
     if let some descr := env.find? n |>.bind (·.value?) then
       if let some tk ← getFirstTk descr then
diff --git a/src/Lean/Elab/Tactic/RCases.lean b/src/Lean/Elab/Tactic/RCases.lean
index 31d3ecac7164..738e1fd0d8dc 100644
--- a/src/Lean/Elab/Tactic/RCases.lean
+++ b/src/Lean/Elab/Tactic/RCases.lean
@@ -27,6 +27,8 @@ instance : Coe (TSyntax ``rcasesPatMed) (TSyntax ``rcasesPatLo) where
 instance : Coe (TSyntax `rcasesPat) (TSyntax `rintroPat) where
   coe stx := Unhygienic.run `(rintroPat| $stx:rcasesPat)
 
+set_option interpreter.prefer_native false
+
 /-- A list, with a disjunctive meaning (like a list of inductive constructors, or subgoals) -/
 local notation "ListΣ" => List
 
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 1616aa69e1c0..6a0cfb51845a 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -94,7 +94,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Co
 private def addDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
-    let info ← getConstInfo declName
+    let info ← getConstVal declName
     if (← isProp info.type) then
       thms.addConst declName (post := post) (inv := inv)
     else
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 4636a9dc9b04..4f94ac9ad9aa 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -943,6 +943,7 @@ private def applyAttributesCore
     return
   withDeclName declName do
     for attr in attrs do
+      withTraceNode `Elab.attribute (fun _ => pure m!"applying [{attr.stx}]") do
       withRef attr.stx do withLogging do
       let env ← getEnv
       match getAttributeImpl env attr.name with
@@ -1661,7 +1662,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     let givenNameView := { view with name := n }
     let mut globalDeclFoundNext := globalDeclFound
     unless globalDeclFound do
-      let r ← resolveGlobalName givenNameView.review
+      let r ← withTraceNode `Elab.resolveGlobalName (fun _ => pure givenNameView.review) do resolveGlobalName givenNameView.review
       let r := r.filter fun (_, fieldList) => fieldList.isEmpty
       unless r.isEmpty do
         globalDeclFoundNext := true
@@ -2109,7 +2110,7 @@ private def checkDeprecatedCore (constName : Name) : TermElabM Unit := do
 -/
 def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
   checkDeprecatedCore constName
-  let cinfo ← getConstInfo constName
+  let cinfo ← getConstVal constName
   if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels for '{constName}'"
   else
@@ -2280,5 +2281,6 @@ export Term (TermElabM)
 
 builtin_initialize
   registerTraceClass `Elab.implicitForall
+  registerTraceClass `Elab.attribute
 
 end Lean.Elab
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index bbe640f45f15..ccd3b272a612 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -161,18 +161,17 @@ structure Diagnostics where
   deriving Inhabited
 
 /--
-An environment stores declarations provided by the user. The kernel
-currently supports different kinds of declarations such as definitions, theorems,
-and inductive families. Each has a unique identifier (i.e., `Name`), and can be
-parameterized by a sequence of universe parameters.
-A constant in Lean is just a reference to a `ConstantInfo` object. The main task of
-the kernel is to type check these declarations and refuse type incorrect ones. The
-kernel does not allow declarations containing metavariables and/or free variables
-to be added to an environment. Environments are never destructively updated.
-
-The environment also contains a collection of extensions. For example, the `simp` theorems
-declared by users are stored in an environment extension. Users can declare new extensions
-using meta-programming.
+An environment stores declarations provided by the user. The kernel currently supports different
+kinds of declarations such as definitions, theorems, and inductive families. Each has a unique
+identifier (i.e., `Name`), and can be parameterized by a sequence of universe parameters. A constant
+in Lean is just a reference to a `ConstantInfo` object. The main task of the kernel is to type check
+these declarations and refuse type incorrect ones. The kernel does not allow declarations containing
+metavariables and/or free variables to be added to an environment. Environments are never
+destructively updated.
+
+This type contains only the minimal data necessary for basic type checking. Other data used only by
+and for elaboration, as well data for the TCB extension of native reduction, is stored in
+`Lean.Environment`.
 -/
 structure Environment where
   /--
@@ -248,6 +247,65 @@ inductive Exception where
 
 namespace Environment
 
+--
+--private def modifyCheckedAsync (env : Environment) (f : EnvironmentBase → EnvironmentBase) : Environment :=
+--  { env with checked := env.checked.map (sync := true) f, checkedNoAsync := f env.checkedNoAsync }
+--
+--private def setCheckedSync (env : Environment) (newChecked : EnvironmentBase) : Environment :=
+--  { env with checked := .pure newChecked, checkedNoAsync := newChecked }
+
+--/-- Type check given declaration and add it to the environment. -/
+--@[extern "lean_elab_add_decl"]
+--opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration)
+--  (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment
+--
+--@[inherit_doc Kernel.Environment.addDeclWithoutChecking, extern "lean_elab_add_decl_without_checking"]
+--opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except Kernel.Exception Environment
+--
+--def EIO.ofExcept : Except e α → EIO e α
+--  | .ok a    => pure a
+--  | .error e => throw e
+--
+--private def addDeclNoDelay (env : Environment) (opts : Options) (decl : Declaration)
+--    (cancelTk? : Option IO.CancelToken := none) (skipExisting := false) :
+--    Except Kernel.Exception Environment := do
+--  if skipExisting then
+--    if let [name] := decl.getNames then
+--      if env.checked.get.kernel.find? name |>.isSome then
+--        return env.synchronize
+--  if debug.skipKernelTC.get opts then
+--    addDeclWithoutChecking env decl
+--  else
+--    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
+--
+--def addDecl (env : Environment) (opts : Options) (decl : Declaration)
+--    (cancelTk? : Option IO.CancelToken := none) (checkAsyncPrefix := true) (skipExisting := false) :
+--    Except Kernel.Exception Environment := do
+--  if let some n := env.realizingConst? then
+--    panic! s!"cannot add declaration {decl.getNames} while realizing constant {n}"
+--  doAdd
+--where doAdd := addDeclNoDelay env opts decl cancelTk? skipExisting
+--
+--@[export lean_elab_environment_to_kernel_env_unchecked]
+--def toKernelEnvUnchecked (env : Environment) : Kernel.Environment := Id.run do
+--  let mut kenv := env.checkedNoAsync.kernel
+--  for asyncConst in env.asyncConsts.toArray do
+--    kenv := kenv.add asyncConst.info.info.get
+--  kenv
+--
+--@[export lean_elab_environment_to_kernel_env_no_async]
+--def toKernelEnv (env : Environment) : Kernel.Environment :=
+--  env.checked.get.kernel
+--
+--def constants (env : Environment) : ConstMap :=
+--  env.checked.get.kernel.constants
+--
+--def getImportedConstants (env : Environment) : Std.HashMap Name ConstantInfo :=
+--  env.checkedNoAsync.kernel.constants.map₁
+--
+--def getLocalConstantsUnchecked (env : Environment) : NameMap AsyncConstantInfo := Id.run do
+--  let map := env.checkedNoAsync.kernel.constants.map₂.foldl (fun m n c => m.insert n (.ofConstantInfo c)) .empty
+--  env.asyncConsts.toArray.foldl (fun m c => m.insert c.info.name c.info) map
 @[export lean_environment_find]
 def find? (env : Environment) (n : Name) : Option ConstantInfo :=
   /- It is safe to use `find'` because we never overwrite imported declarations. -/
@@ -354,6 +412,11 @@ def ofConstantInfo (c : ConstantInfo) : AsyncConstantInfo where
   sig := .pure c.toConstantVal
   constInfo := .pure c
 
+def isUnsafe (c : AsyncConstantInfo) : Bool :=
+  match c.kind with
+  | .thm => false
+  | _ => c.toConstantInfo.isUnsafe
+
 end AsyncConstantInfo
 
 /--
@@ -442,18 +505,25 @@ structure Environment where
   private asyncConsts : AsyncConsts := {}
   /-- Information about this asynchronous branch of the environment, if any. -/
   private asyncCtx?   : Option AsyncContext := none
+  private realizedExternConsts? : Option (IO.Ref (NameMap AsyncConst))
+  private realizedLocalConsts  : NameMap (IO.Ref (NameMap AsyncConst)) := {}
+  realizingConst? : Option Name := none
 deriving Nonempty
 
 namespace Environment
 
+-- used only when the kernel calls into the interpreter, and in `Lean.Kernel.Exception.mkCtx`
 @[export lean_elab_environment_of_kernel_env]
 def ofKernelEnv (env : Kernel.Environment) : Environment :=
-  { checkedWithoutAsync := env }
+  { checkedWithoutAsync := env, realizedExternConsts? := none }
 
 @[export lean_elab_environment_to_kernel_env]
 def toKernelEnv (env : Environment) : Kernel.Environment :=
   env.checked.get
 
+def synchronize (env : Environment) : Environment :=
+  { env with checkedWithoutAsync := env.checked.get }
+
 /-- Consistently updates synchronous and asynchronous parts of the environment without blocking. -/
 private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
   { env with checked := env.checked.map (sync := true) f, checkedWithoutAsync := f env.checkedWithoutAsync }
@@ -571,6 +641,17 @@ def findConstVal? (env : Environment) (n : Name) : Option ConstantVal := do
     return asyncConst.constInfo.toConstantVal
   else env.findNoAsync n |>.map (·.toConstantVal)
 
+def enableRealizationsForConst (env : Environment) (c : Name) : BaseIO Environment := do
+  if env.realizedLocalConsts.contains c then
+    return env
+  return { env with realizedLocalConsts := env.realizedLocalConsts.insert c (← IO.mkRef {}) }
+
+def isAsync (env : Environment) : Bool :=
+  env.asyncCtx?.isSome
+
+def unlockAsync (env : Environment) : Environment :=
+  env  --{ env with asyncCtx? := env.asyncCtx?.map ({ · with declPrefix := .anonymous }) }
+
 /--
 Looks up the given declaration name in the environment, blocking on the corresponding elaboration
 task if not yet complete.
@@ -588,8 +669,12 @@ def dbgFormatAsyncState (env : Environment) : BaseIO String :=
   return s!"\
     asyncCtx.declPrefix: {repr <| env.asyncCtx?.map (·.declPrefix)}\
   \nasyncConsts: {repr <| env.asyncConsts.toArray.map (·.constInfo.name)}\
-  \ncheckedWithoutAsync.constants.map₂: {repr <|
-      env.checkedWithoutAsync.constants.map₂.toList.map (·.1)}"
+  \nrealizedLocalConsts: {repr (← env.realizedLocalConsts.toList.filterMapM fun (n, m) => do
+    let consts := (← m.get).toList
+    return guard (!consts.isEmpty) *> some (n, consts.map (·.1)))}
+  \nrealizedExternConsts?: {repr <| (← env.realizedExternConsts?.mapM fun consts => do
+    return (← consts.get).toList.map fun (n, m) => (n, m.constInfo.name))}
+  \ncheckedWithoutAsync.constants.map₂: {repr <| env.checkedWithoutAsync.constants.map₂.toList.map (·.1)}"
 
 /-- Returns debug output about the synchronous state of the environment. -/
 def dbgFormatCheckedSyncState (env : Environment) : BaseIO String :=
@@ -630,6 +715,7 @@ information.
 def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts := true) :
     IO AddConstAsyncResult := do
   assert! env.asyncMayContain constName
+  let env ← enableRealizationsForConst env constName
   let sigPromise ← IO.Promise.new
   let infoPromise ← IO.Promise.new
   let extensionsPromise ← IO.Promise.new
@@ -762,12 +848,93 @@ def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
 def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
   env.header.moduleNames.findIdx? (· == moduleName)
 
+def EIO.ofExcept (e : Except ε α) : EIO ε α :=
+  match e with
+  | Except.ok a    => pure a
+  | Except.error e => throw e
+
+def realizeConst (env : Environment) (forConst : Name) (constName : Name) (kind : ConstantKind)
+    (sig? : Option (Task ConstantVal) := none) :
+    IO (Environment × Option (Option ConstantInfo → EIO Kernel.Exception Environment)) := do
+  let mut env := env
+  if (env.checkedWithoutAsync.find? constName |>.isSome) || (env.asyncConsts.find? constName |>.isSome) then
+    return (env, none)
+  if let some n := env.realizingConst? then
+    panic! s!"cannot realize {constName} while already realizing {n}"
+  let prom ← IO.Promise.new
+  let asyncConst := Thunk.mk fun _ => {
+    constInfo := {
+      name := constName
+      kind
+      sig := sig?.getD (prom.result!.map (sync := true) (·.toConstantVal))
+      constInfo := prom.result!
+    }
+    exts? := none  -- will be reported by the caller eventually
+  }
+  let ref ← if env.checkedWithoutAsync.const2ModIdx.contains forConst then
+    env.realizedExternConsts?.getDM <|
+      throw <| .userError s!"Environment.realizeConst: `realizedExternConsts` is empty"
+  else
+    match env.realizedLocalConsts.find? forConst with
+    | some ref => pure ref
+    | none     =>
+      if env.asyncCtx?.any (·.mayContain forConst) then
+        let ref ← IO.mkRef {}
+        env := { env with realizedLocalConsts := env.realizedLocalConsts.insert forConst ref }
+        pure ref
+      else
+        throw <| .userError s!"trying to realize {constName} but `enableRealizationsForConst` must be called for '{forConst}' first"
+      throw <| .userError s!"trying to realize {constName} but `enableRealizationsForConst` must be called for '{forConst}' first"
+  let existingConst? ← ref.modifyGet fun m => match m.find? constName with
+    | some prom' => (some prom', m)
+    | none       => (none, m.insert constName asyncConst.get)
+  if let some existingConst := existingConst? then
+    env := { env with
+      asyncConsts := env.asyncConsts.add existingConst
+      checked := env.checked.map fun env =>
+        if env.find? constName |>.isSome then
+          env
+        else
+          env.add existingConst.constInfo.toConstantInfo
+    }
+    return (env, none)
+  else
+    env := { env with realizingConst? := some constName }
+    return (env, some fun
+      | none => do
+        prom.resolve /- TODO -/ default
+        return { env with realizingConst? := none }
+      | some const => do
+        let env := { env with realizingConst? := none }
+        let decl ← match const with
+          | .thmInfo thm   => pure <| .thmDecl thm
+          | .defnInfo defn => pure <| .defnDecl defn
+          | _              => throw <| .other s!"Environment.realizeConst: {constName} must be definition/theorem"
+        -- must happen before `addDeclCore` because on the main thread that can block on a use of `constName`
+        prom.resolve const
+        let async ← env.addConstAsync (reportExts := false) constName kind |>.adaptExcept (·.toString |> .other)
+        async.commitConst async.asyncEnv (some const) |>.adaptExcept (·.toString |> .other)
+        let _checkTask ← BaseIO.mapTask (t := env.checked) fun _ => EIO.catchExceptions (h := fun _e =>
+          panic! s!"realizeConst {constName} failed"
+        ) do
+          let env ← EIO.ofExcept <| addDeclCore async.asyncEnv 0 decl none
+          async.commitCheckEnv env |>.adaptExcept (·.toString |> .other)
+        if const.name != constName then
+          throw <| .other s!"Environment.realizeConst: realized constant has name {const.name} but expected {constName}"
+        let kind' := .ofConstantInfo const
+        if kind != kind' then
+          throw <| .other s!"Environment.realizeConst: realized constant has kind {repr kind} but expected {repr kind'}"
+        return async.mainEnv)
+
 end Environment
 
+def ConstantVal.instantiateTypeLevelParams (c : ConstantVal) (ls : List Level) : Expr :=
+  c.type.instantiateLevelParams c.levelParams ls
+
 namespace ConstantInfo
 
 def instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr :=
-  c.type.instantiateLevelParams c.levelParams ls
+  c.toConstantVal.instantiateTypeLevelParams ls
 
 def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) : Expr :=
   c.value!.instantiateLevelParams c.levelParams ls
@@ -975,7 +1142,7 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
   let initializing ← IO.initializing
   if initializing then throw (IO.userError "environment objects cannot be created during initialization")
   let exts ← mkInitialExtensionStates
-  pure {
+  return {
     checkedWithoutAsync := {
       const2ModIdx    := {}
       constants       := {}
@@ -983,11 +1150,14 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
       extraConstNames := {}
       extensions      := exts
     }
+    realizedExternConsts? := some (← IO.mkRef {})
   }
 
 structure PersistentEnvExtensionState (α : Type) (σ : Type) where
   importedEntries : Array (Array α)  -- entries per imported module
   state : σ
+  async : Bool := false
+deriving Inhabited
 
 structure ImportM.Context where
   env  : Environment
@@ -1048,9 +1218,6 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
   exportEntriesFn : σ → Array α
   statsFn         : σ → Format
 
-instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
-  ⟨{importedEntries := #[], state := default }⟩
-
 instance {α β σ} [Inhabited σ] : Inhabited (PersistentEnvExtension α β σ) where
   default := {
      toEnvExtension := default,
@@ -1073,8 +1240,9 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
     { s with state := state }
 
 /-- Get the current state of the given extension in the given environment. -/
-def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : σ :=
-  (ext.toEnvExtension.getState env).state
+def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment)
+    (asyncMode := ext.toEnvExtension.asyncMode) : σ :=
+  (ext.toEnvExtension.getState (asyncMode := asyncMode) env).state
 
 /-- Set the current state of the given extension in the given environment. -/
 def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=
@@ -1175,8 +1343,9 @@ def getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension
   (PersistentEnvExtension.getState ext env).1
 
 /-- Get the current state of the given `SimplePersistentEnvExtension`. -/
-def getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) : σ :=
-  (PersistentEnvExtension.getState ext env).2
+def getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment)
+    (asyncMode := ext.toEnvExtension.asyncMode) : σ :=
+  (PersistentEnvExtension.getState (asyncMode := asyncMode) ext env).2
 
 /-- Set the current state of the given `SimplePersistentEnvExtension`. This change is *not* persisted across files. -/
 def setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) : Environment :=
@@ -1186,6 +1355,10 @@ def setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : En
 def modifyState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) : Environment :=
   PersistentEnvExtension.modifyState ext env (fun ⟨entries, s⟩ => (entries, f s))
 
+def findStateAsync {α σ : Type} [Inhabited σ]
+    (ext : SimplePersistentEnvExtension α σ) (env : Environment) (declName : Name) : σ :=
+  PersistentEnvExtension.findStateAsync ext env declName |>.2
+
 end SimplePersistentEnvExtension
 
 /-- Environment extension for tagging declarations.
@@ -1213,7 +1386,7 @@ def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) :
 def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : Bool :=
   match env.getModuleIdxFor? declName with
   | some modIdx => (ext.getModuleEntries env modIdx).binSearchContains declName Name.quickLt
-  | none        => (ext.getState env).contains declName
+  | none        => (ext.getState (asyncMode := .local) env).contains declName
 
 end TagDeclarationExtension
 
@@ -1241,13 +1414,14 @@ def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Na
   assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`
   ext.addEntry env (declName, val)
 
-def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Option α :=
+def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name)
+    (asyncMode := ext.toEnvExtension.asyncMode) : Option α :=
   match env.getModuleIdxFor? declName with
   | some modIdx =>
     match (ext.getModuleEntries env modIdx).binSearch (declName, default) (fun a b => Name.quickLt a.1 b.1) with
     | some e => some e.2
     | none   => none
-  | none => (ext.getState env).find? declName
+  | none => (ext.getState (asyncMode := asyncMode) env).find? declName
 
 def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Bool :=
   match env.getModuleIdxFor? declName with
@@ -1478,6 +1652,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
         moduleData   := s.moduleData
       }
     }
+    realizedExternConsts? := some (← IO.mkRef {})
   }
   env ← setImportedEntries env s.moduleData
   if leakEnv then
@@ -1561,7 +1736,10 @@ namespace Environment
 
 /-- Register a new namespace in the environment. -/
 def registerNamespace (env : Environment) (n : Name) : Environment :=
-  if (namespacesExt.getState env).contains n then env else namespacesExt.addEntry env n
+  namespacesExt.toEnvExtension.modifyState env fun s =>
+    if s.state.1.contains n then s else
+      let state   := namespacesExt.addEntryFn s.state n;
+      { s with state := state }
 
 /-- Return `true` if `n` is the name of a namespace in `env`. -/
 def isNamespace (env : Environment) (n : Name) : Bool :=
@@ -1616,7 +1794,7 @@ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName :
 def hasUnsafe (env : Environment) (e : Expr) : Bool :=
   let c? := e.find? fun e => match e with
     | Expr.const c _ =>
-      match env.find? c with
+      match env.findAsync? c with
       | some cinfo => cinfo.isUnsafe
       | none       => false
     | _ => false;
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 07f24d82fb97..435beb6daf7a 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -184,4 +184,33 @@ macro_rules
   | `(throwErrorAt $ref $msg:interpolatedStr) => `(Lean.throwErrorAt $ref (m! $msg))
   | `(throwErrorAt $ref $msg:term)            => `(Lean.throwErrorAt $ref $msg)
 
+/--
+`MonadExcept` variant that is expected to catch all exceptions of the given type in case the
+standard instance doesn't.
+
+In most circumstances, we want to let runtime exceptions during term elaboration bubble up to the
+command elaborator (see `Core.tryCatch`). However, in a few cases like building the trace tree, we
+really need to handle (and then re-throw) every exception lest we end up with a broken tree.
+-/
+class MonadAlwaysExcept (ε : outParam (Type u)) (m : Type u → Type v) where
+  except : MonadExceptOf ε m
+
+-- instances sufficient for inferring `MonadAlwaysExcept` for the elaboration monads
+
+instance : MonadAlwaysExcept ε (EIO ε) where
+  except := inferInstance
+
+instance [always : MonadAlwaysExcept ε m] [Monad m] : MonadAlwaysExcept ε (StateT σ m) where
+  except := let _ := always.except; inferInstance
+
+instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where
+  except := let _ := always.except; inferInstance
+
+instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where
+  except := let _ := always.except; inferInstance
+
+instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] :
+    MonadAlwaysExcept ε (MonadCacheT α β m) where
+  except := let _ := always.except; inferInstance
+
 end Lean
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 20ae50e90035..4b9834529b61 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -509,7 +509,10 @@ with
         (t.data.hasLevelMVar || v.data.hasLevelMVar || b.data.hasLevelMVar)
         (t.data.hasLevelParam || v.data.hasLevelParam || b.data.hasLevelParam)
     | .lit l => mkData (mixHash 3 (hash l))
-deriving Inhabited, Repr
+deriving Repr
+
+instance : Inhabited Expr where
+  default := .const `_inhabitedExprDummy []
 
 namespace Expr
 
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index bcc608cd311a..576b1d5d6200 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -161,7 +161,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact de
 
 /-- Retrieve entries tagged with `[attr key]` or `[builtinAttr key]`. -/
 def getEntries {γ} (attr : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List (AttributeEntry γ) :=
-  let s := attr.ext.getState env
+  let s := attr.ext.getState (asyncMode := .local) env
   let attrs := s.table.findD key []
   if s.erased.isEmpty then
     attrs
diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
index 660c1d615d40..d45d96e3582f 100644
--- a/src/Lean/Language/Basic.lean
+++ b/src/Lean/Language/Basic.lean
@@ -138,6 +138,10 @@ structure SyntaxGuarded (α : Type) where
   /-- Potentially reusable value. -/
   val : α
 
+/-- Applies `f` to `s.val`. -/
+def SyntaxGuarded.mapVal (s : SyntaxGuarded α) (f : α → β) : SyntaxGuarded β :=
+  { s with val := f s.val }
+
 /--
 Pair of (optional) old snapshot task usable for incremental reuse and new snapshot promise for
 incremental reporting. Inside the elaborator, we build snapshots by carrying such bundles and then
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 94807f0c2bf4..6033b74dfe72 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -539,7 +539,7 @@ where
       -- is not `Inhabited`
       prom.resolve <| {
         diagnostics := .empty, stx := .missing, parserState
-        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        elabSnap := default
         finishedSnap := .pure { diagnostics := .empty, cmdState }
         reportSnap := default
         tacticCache := (← IO.mkRef {})
diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean
index e9ac7a1ee2ba..4d5b73c370ee 100644
--- a/src/Lean/Linter/Deprecated.lean
+++ b/src/Lean/Linter/Deprecated.lean
@@ -49,7 +49,7 @@ def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
   if getLinterValue linter.deprecated (← getOptions) then
-    let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
+    let some attr := deprecatedAttr.getParam? (asyncMode := .async) (← getEnv) declName | pure ()
     logWarning <| .tagged ``deprecatedAttr <|
       m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with
       | some text => s!": {text}"
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 742ad05f8b96..150bcef40d5d 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -48,6 +48,7 @@ opaque mkHandler (constName : Name) : ImportM Handler
 
 builtin_initialize builtinHandlersRef : IO.Ref (NameMap Handler) ← IO.mkRef {}
 
+-- asynchrony: only set by the command-level `@[missing_docs_handler]`
 builtin_initialize missingDocsExt :
   PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler) ←
   registerPersistentEnvExtension {
@@ -63,7 +64,7 @@ builtin_initialize missingDocsExt :
 def addHandler (env : Environment) (declName key : Name) (h : Handler) : Environment :=
   missingDocsExt.addEntry env (declName, key, h)
 
-def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getState env).2
+def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getState (asyncMode := .local) env).2
 
 partial def missingDocs : Linter where
   run stx := do
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 7d7abe40bbe9..ad1c066ac56b 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -78,7 +78,7 @@ open Lean.Elab.Command Lean.Server Std
 
 /-- Enables or disables all unused variable linter warnings -/
 register_builtin_option linter.unusedVariables : Bool := {
-  defValue := true,
+  defValue := false,  -- TODO
   descr := "enable the 'unused variables' linter"
 }
 /-- Enables or disables unused variable linter warnings in function arguments -/
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 26d333ee796d..8a8d46fe3685 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -317,7 +317,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
   loop fType 0 0 #[] #[]
 
 private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
-  let cinfo ← getConstInfo constName
+  let cinfo ← getConstVal constName
   let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
   let f := mkConst constName us
   let fType ← instantiateTypeLevelParams cinfo us
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index d18ab6d9ca6e..d03fa3b6beb7 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -18,7 +18,7 @@ private def ensureType (e : Expr) : MetaM Unit := do
   discard <| getLevel e
 
 private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do
-  let cinfo ← getConstInfo constName
+  let cinfo ← getConstVal constName
   unless us.length == cinfo.levelParams.length do
     throwIncorrectNumberOfLevels constName us
 
diff --git a/src/Lean/Meta/Constructions/CasesOn.lean b/src/Lean/Meta/Constructions/CasesOn.lean
index e4ab37384d95..5b83c2f5a3fd 100644
--- a/src/Lean/Meta/Constructions/CasesOn.lean
+++ b/src/Lean/Meta/Constructions/CasesOn.lean
@@ -15,6 +15,7 @@ open Meta
 
 def mkCasesOn (declName : Name) : MetaM Unit := do
   let name := mkCasesOnName declName
+  -- can use unchecked as `addDecl` will check the result
   let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv).toKernelEnv declName)
   addDecl decl
   setReducibleAttribute name
diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean
index 52cf24dbcfe3..66703a960039 100644
--- a/src/Lean/Meta/Constructions/NoConfusion.lean
+++ b/src/Lean/Meta/Constructions/NoConfusion.lean
@@ -10,8 +10,8 @@ import Lean.Meta.CompletionName
 
 namespace Lean
 
-@[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
-@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
+@[extern "lean_mk_no_confusion_type"] private opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
+@[extern "lean_mk_no_confusion"] private opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except Kernel.Exception Declaration
 
 open Meta
 
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index e350d2fca13c..d2a2c77f540e 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -128,9 +128,8 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
 
 /-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
-  if let some (.defnInfo info) := (← getEnv).find? declName then
-    if (← isProp info.type) then return false
-    return true
+  if let some { kind := .defn, sig, .. } := (← getEnv).findAsync? declName then
+    return !(← isProp sig.get.type)
   else
     return false
 
@@ -153,10 +152,11 @@ private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSu
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)
       let name := declName ++ suffix
-      addDecl <| Declaration.thmDecl {
-        name, type, value
-        levelParams := info.levelParams
-      }
+      realizeConst declName name .thm do
+        return .thmInfo {
+          name, type, value
+          levelParams := info.levelParams
+        }
       return some name
   else
     return none
@@ -165,7 +165,7 @@ private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSu
 Returns `some declName` if `thmName` is an equational theorem for `declName`.
 -/
 def isEqnThm? (thmName : Name) : CoreM (Option Name) := do
-  return eqnsExt.getState (← getEnv) |>.mapInv.find? thmName
+  return eqnsExt.getState (asyncMode := .local) (← getEnv) |>.mapInv.find? thmName
 
 /--
 Returns `true` if `thmName` is an equational theorem.
@@ -202,11 +202,17 @@ private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array N
     return none
 
 private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
+  -- Test this first as it blocks on the least data
+  if !(← shouldGenerateEqnThms declName) then
+    return none
+  -- must use `NoAsync` as otherwise we may be able to see the extension state
+  -- from a different thread without the constant being realized on this thread
+  -- yet, and also it would be a hard block
+  else if let some eqs := eqnsExt.getState (asyncMode := .local) (← getEnv) |>.map.find? declName then
     return some eqs
   else if let some eqs ← alreadyGenerated? declName then
     return some eqs
-  else if (← shouldGenerateEqnThms declName) then
+  else
     for f in (← getEqnsFnsRef.get) do
       if let some r ← f declName then
         registerEqnThms declName r
diff --git a/src/Lean/Meta/Eval.lean b/src/Lean/Meta/Eval.lean
index c96e032630a2..e35a1beaf79c 100644
--- a/src/Lean/Meta/Eval.lean
+++ b/src/Lean/Meta/Eval.lean
@@ -10,7 +10,7 @@ import Lean.Util.CollectLevelParams
 
 namespace Lean.Meta
 
-unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (safety := DefinitionSafety.safe) : MetaM α :=
+unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (safety := DefinitionSafety.safe) : MetaM α := do
   withoutModifyingEnv do
     let name ← mkFreshUserName `_tmp
     let value ← instantiateMVars value
diff --git a/src/Lean/Meta/GetUnfoldableConst.lean b/src/Lean/Meta/GetUnfoldableConst.lean
index 1a5fdde385e5..bb66ad860ac7 100644
--- a/src/Lean/Meta/GetUnfoldableConst.lean
+++ b/src/Lean/Meta/GetUnfoldableConst.lean
@@ -37,11 +37,19 @@ This is part of the implementation of `whnf`.
 External users wanting to look up names should be using `Lean.getConstInfo`.
 -/
 def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
-  match (← getEnv).find? constName with
-  | some (info@(.thmInfo _))  => getTheoremInfo info
-  | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | some _                    => return none
-  | none                      => throwUnknownConstant constName
+  let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstant constName
+  match ainfo.kind with
+  | .thm =>
+    if (← shouldReduceAll) then
+      return some ainfo.constInfo.get
+    else
+      return none
+  | _ => match ainfo.toConstantInfo with
+    | info@(.defnInfo _) => if (← canUnfold info) then return info else return none
+    | info@(.recInfo _)  => return some info
+    -- `.lift` and `.ind` are reducible; no point in finer-grained filtering at this point
+    | info@(.quotInfo _) => return some info
+    | _                  => return none
 
 /--
 As with `getUnfoldableConst?` but return `none` instead of failing if the constant is not found.
@@ -50,6 +58,9 @@ def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) :=
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
+  | some (info@(.recInfo _))  => return some info
+  -- `.lift` and `.ind` are reducible; no point in finer-grained filtering at this point
+  | some (info@(.quotInfo _)) => return some info
   | _                         => return none
 
 end Meta
diff --git a/src/Lean/Meta/GlobalInstances.lean b/src/Lean/Meta/GlobalInstances.lean
index 1cb5401f00ef..9b6081bb5beb 100644
--- a/src/Lean/Meta/GlobalInstances.lean
+++ b/src/Lean/Meta/GlobalInstances.lean
@@ -20,6 +20,6 @@ def addGlobalInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit
 
 @[export lean_is_instance]
 def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
-  globalInstanceExtension.getState env |>.contains declName
+  globalInstanceExtension.getState (asyncMode := .local) env |>.contains declName
 
 end Lean.Meta
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index c99fe03df2fb..cc2682ef970c 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -88,7 +88,7 @@ def throwIncorrectNumberOfLevels {α} (constName : Name) (us : List Level) : Met
   throwError "incorrect number of universe levels {mkConst constName us}"
 
 private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
-  let cinfo ← getConstInfo c
+  let cinfo ← getConstVal c
   if cinfo.levelParams.length == us.length then
     instantiateTypeLevelParams cinfo us
   else
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index d7802c3d4c1a..f6fea5ef0b06 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -246,23 +246,23 @@ builtin_initialize
   }
 
 def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
-  return Meta.instanceExtension.getState (← getEnv) |>.discrTree
+  return Meta.instanceExtension.getState (asyncMode := .local) (← getEnv) |>.discrTree
 
 def getErasedInstances : CoreM (PHashSet Name) :=
-  return Meta.instanceExtension.getState (← getEnv) |>.erased
+  return Meta.instanceExtension.getState (asyncMode := .local) (← getEnv) |>.erased
 
 def isInstanceCore (env : Environment) (declName : Name) : Bool :=
-  Meta.instanceExtension.getState env |>.instanceNames.contains declName
+  Meta.instanceExtension.getState (asyncMode := .local) env |>.instanceNames.contains declName
 
 def isInstance (declName : Name) : CoreM Bool :=
   return isInstanceCore (← getEnv) declName
 
 def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
-  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none
+  let some entry := Meta.instanceExtension.getState (asyncMode := .local) (← getEnv) |>.instanceNames.find? declName | return none
   return entry.priority
 
 def getInstanceAttrKind? (declName : Name) : CoreM (Option AttributeKind) := do
-  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none
+  let some entry := Meta.instanceExtension.getState (asyncMode := .local) (← getEnv) |>.instanceNames.find? declName | return none
   return entry.attrKind
 
 /-! # Default instance support -/
@@ -315,9 +315,9 @@ builtin_initialize
   registerTraceClass `Meta.synthOrder
 
 def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
-  return defaultInstanceExtension.getState (← getEnv) |>.priorities
+  return defaultInstanceExtension.getState (asyncMode := .local) (← getEnv) |>.priorities
 
 def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
-  return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
+  return defaultInstanceExtension.getState (asyncMode := .local) (← getEnv) |>.defaultInstances.find? className |>.getD []
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index d8909221a485..953c93647eab 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -773,7 +773,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   let env ← getEnv
   let mkMatcherConst name :=
     mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
-  match (matcherExt.getState env).find? (result.value, compile) with
+  match (matcherExt.getState (asyncMode := .local) env).find? (result.value, compile) with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
     let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 9c08c3f01ba1..b69d2a2be393 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -714,59 +714,69 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
         for discr in discrs.toArray.reverse, pattern in patterns.reverse do
           notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt
         notAlt ← mkForallFVars (discrs ++ ys) notAlt
-        /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
-           Thus, we need to create new `alts`. -/
-        withNewAlts numDiscrEqs discrs patterns alts fun alts => do
-          let alt := alts[i]!
-          let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
-          let rhs := mkAppN alt rhsArgs
-          let thmType ← mkEq lhs rhs
-          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
-          let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
-          let thmType ← unfoldNamedPattern thmType
-          let thmVal ← proveCondEqThm matchDeclName thmType
-          addDecl <| Declaration.thmDecl {
-            name        := thmName
-            levelParams := constInfo.levelParams
-            type        := thmType
-            value       := thmVal
-          }
-          return (notAlt, splitterAltType, splitterAltNumParam, argMask)
+        realizeConst matchDeclName thmName .thm do
+          /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant.
+            Thus, we need to create new `alts`. -/
+          withNewAlts numDiscrEqs discrs patterns alts fun alts => do
+            let alt := alts[i]!
+            let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
+            let rhs := mkAppN alt rhsArgs
+            let thmType ← mkEq lhs rhs
+            let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+            let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
+            let thmType ← unfoldNamedPattern thmType
+            let thmVal ← proveCondEqThm matchDeclName thmType
+            return .thmInfo {
+              name        := thmName
+              levelParams := constInfo.levelParams
+              type        := thmType
+              value       := thmVal
+            }
+        return (notAlt, splitterAltType, splitterAltNumParam, argMask)
       notAlts := notAlts.push notAlt
       splitterAltTypes := splitterAltTypes.push splitterAltType
       splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam
       altArgMasks := altArgMasks.push argMask
       trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}"
       idx := idx + 1
-    -- Define splitter with conditional/refined alternatives
-    withSplitterAlts splitterAltTypes fun altsNew => do
-      let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
-      let splitterType ← mkForallFVars splitterParams matchResultType
-      trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
-      let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
-      let template ← deltaExpand template (· == constInfo.name)
-      let template := template.headBeta
-      let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
-      addAndCompile <| Declaration.defnDecl {
-        name        := splitterName
-        levelParams := constInfo.levelParams
-        type        := splitterType
-        value       := splitterVal
-        hints       := .abbrev
-        safety      := .safe
-      }
-      setInlineAttribute splitterName
-      let result := { eqnNames, splitterName, splitterAltNumParams }
-      registerMatchEqns matchDeclName result
-      return result
+    realizeConst matchDeclName splitterName .defn do
+      -- Define splitter with conditional/refined alternatives
+      withSplitterAlts splitterAltTypes fun altsNew => do
+        let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
+        let splitterType ← mkForallFVars splitterParams matchResultType
+        trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
+        let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
+        let template ← deltaExpand template (· == constInfo.name)
+        let template := template.headBeta
+        let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
+        setInlineAttribute splitterName  -- TODO
+        -- TODO compilation?
+        return .defnInfo {
+          name        := splitterName
+          levelParams := constInfo.levelParams
+          type        := splitterType
+          value       := splitterVal
+          hints       := .abbrev
+          safety      := .safe
+        }
+    let result := { eqnNames, splitterName, splitterAltNumParams }
+    registerMatchEqns matchDeclName result
+    return result
 
 /- See header at `MatchEqsExt.lean` -/
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
-  match matchEqnsExt.getState (← getEnv) |>.map.find? matchDeclName with
+  match matchEqnsExt.getState (asyncMode := .local) (← getEnv) |>.map.find? matchDeclName with
   | some matchEqns => return matchEqns
   | none => mkEquationsFor matchDeclName
 
-builtin_initialize registerTraceClass `Meta.Match.matchEqs
+builtin_initialize
+  registerTraceClass `Meta.Match.matchEqs
+  registerReservedNamePredicate fun _ name =>
+    name matches .str _ "splitter"
+  registerReservedNameAction fun name => do
+    let .str p "splitter" := name | return false
+    MetaM.run' <| discard <| getEquationsFor <| privateToUserName p
+    return true
 
 end Lean.Meta.Match
diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean
index 45ce62ee1d4a..fce18fd38b15 100644
--- a/src/Lean/Meta/Match/MatcherInfo.lean
+++ b/src/Lean/Meta/Match/MatcherInfo.lean
@@ -88,7 +88,7 @@ def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo)
   extension.addEntry env { name := matcherName, info := info }
 
 def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo :=
-  (extension.getState env).map.find? declName
+  (extension.findStateAsync env declName).map.find? declName
 
 end Extension
 
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 00e2ce222a22..a9397dd064f3 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -205,6 +205,6 @@ def getCustomEliminator? (targets : Array Expr) (induction : Bool) : MetaM (Opti
     let targetType := (← instantiateMVars (← inferType target)).headBeta
     let .const declName .. := targetType.getAppFn | return none
     key := key.push declName
-  return customEliminatorExt.getState (← getEnv) |>.map.find? (induction, key)
+  return customEliminatorExt.getState (asyncMode := .local) (← getEnv) |>.map.find? (induction, key)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index ace83b9e8902..ead99949c434 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -661,85 +661,81 @@ Given a unary definition `foo` defined via `WellFounded.fixF`, derive a suitable
 def deriveUnaryInduction (name : Name) : MetaM Name := do
   let inductName := .append name `induct
   if ← hasConst inductName then return inductName
-
-  let info ← getConstInfoDefn name
-
-  let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
-
-  -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
-  -- to make sure that `target` indeed the last parameter
-  let e := info.value
-  let e ← lambdaTelescope e fun params body => do
-    if body.isAppOfArity ``WellFounded.fix 5 then
-      forallBoundedTelescope (← inferType body) (some 1) fun xs _ => do
-        unless xs.size = 1 do
-          throwError "functional induction: Failed to eta-expand{indentExpr e}"
-        mkLambdaFVars (params ++ xs) (mkAppN body xs)
-    else
-      pure e
-  let e' ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
-    match_expr funBody with
-    | fix@WellFounded.fix α _motive rel wf body target =>
-      unless params.back! == target do
-        throwError "functional induction: expected the target as last parameter{indentExpr e}"
-      let fixedParams := params.pop
-      let motiveType ← mkForallFVars #[target] (.sort levelZero)
-      withLocalDeclD `motive motiveType fun motive => do
-        let fn := mkAppN (← mkConstWithLevelParams name) fixedParams
-        let isRecCall : Expr → Option Expr := fun e =>
-          if e.isApp && e.appFn!.isFVarOf motive.fvarId! then
-            mkApp fn e.appArg!
-          else
-            none
-
-        let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
-        let e' := mkApp4 e' α motive rel wf
-        check e'
-        let (body', mvars) ← M2.run do
-          forallTelescope (← inferType e').bindingDomain! fun xs goal => do
-            if xs.size ≠ 2 then
-              throwError "expected recursor argument to take 2 parameters, got {xs}" else
-            let targets : Array Expr := xs[:1]
-            let genIH := xs[1]!
-            let extraParams := xs[2:]
-            -- open body with the same arg
-            let body ← instantiateLambda body targets
-            lambdaTelescope1 body fun oldIH body => do
-              let body ← instantiateLambda body extraParams
-              let body' ← buildInductionBody #[oldIH, genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
-              if body'.containsFVar oldIH then
-                throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
-              mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
-        let e' := mkApp2 e' body' target
-        let e' ← mkLambdaFVars #[target] e'
-        let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
-        let e' ← mkLambdaFVars #[motive] e'
-
-        -- We used to pass (usedOnly := false) below in the hope that the types of the
-        -- induction principle match the type of the function better.
-        -- But this leads to avoidable parameters that make functional induction strictly less
-        -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal)
-        let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) fixedParams e'
-        instantiateMVars e'
-    | _ =>
-      if funBody.isAppOf ``WellFounded.fix then
-        throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+  realizeConst name inductName .thm do
+    let info ← getConstInfoDefn name
+
+    let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
+
+    -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
+    -- to make sure that `target` indeed the last parameter
+    let e := info.value
+    let e ← lambdaTelescope e fun params body => do
+      if body.isAppOfArity ``WellFounded.fix 5 then
+        forallBoundedTelescope (← inferType body) (some 1) fun xs _ => do
+          unless xs.size = 1 do
+            throwError "functional induction: Failed to eta-expand{indentExpr e}"
+          mkLambdaFVars (params ++ xs) (mkAppN body xs)
       else
-        throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
+        pure e
+    let e' ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
+      match_expr funBody with
+      | fix@WellFounded.fix α _motive rel wf body target =>
+        unless params.back! == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let fixedParams := params.pop
+        let motiveType ← mkForallFVars #[target] (.sort levelZero)
+        withLocalDeclD `motive motiveType fun motive => do
+          let fn := mkAppN (← mkConstWithLevelParams name) fixedParams
+          let isRecCall : Expr → Option Expr := fun e =>
+            if e.isApp && e.appFn!.isFVarOf motive.fvarId! then
+              mkApp fn e.appArg!
+            else
+              none
+
+          let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
+          let e' := mkApp4 e' α motive rel wf
+          check e'
+          let (body', mvars) ← M2.run do
+            forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+              if xs.size ≠ 2 then
+                throwError "expected recursor argument to take 2 parameters, got {xs}" else
+              let targets : Array Expr := xs[:1]
+              let genIH := xs[1]!
+              let extraParams := xs[2:]
+              -- open body with the same arg
+              let body ← instantiateLambda body targets
+              lambdaTelescope1 body fun oldIH body => do
+                let body ← instantiateLambda body extraParams
+                let body' ← buildInductionBody #[oldIH, genIH.fvarId!] goal oldIH genIH.fvarId! isRecCall body
+                if body'.containsFVar oldIH then
+                  throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
+                mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+          let e' := mkApp2 e' body' target
+          let e' ← mkLambdaFVars #[target] e'
+          let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
+          let e' ← mkLambdaFVars #[motive] e'
 
-  unless (← isTypeCorrect e') do
-    logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"
-    check e'
+          -- We used to pass (usedOnly := false) below in the hope that the types of the
+          -- induction principle match the type of the function better.
+          -- But this leads to avoidable parameters that make functional induction strictly less
+          -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal)
+          let e' ← mkLambdaFVars (binderInfoForMVars := .default) (usedOnly := true) fixedParams e'
+          instantiateMVars e'
+      | _ =>
+        if funBody.isAppOf ``WellFounded.fix then
+          throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+        else
+          throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
 
-  let eTyp ← inferType e'
-  let eTyp ← elimOptParam eTyp
-  -- logInfo m!"eTyp: {eTyp}"
-  let params := (collectLevelParams {} eTyp).params
-  -- Prune unused level parameters, preserving the original order
-  let us := info.levelParams.filter (params.contains ·)
+    let eTyp ← inferType e'
+    let eTyp ← elimOptParam eTyp
+    -- logInfo m!"eTyp: {eTyp}"
+    let params := (collectLevelParams {} eTyp).params
+    -- Prune unused level parameters, preserving the original order
+    let us := info.levelParams.filter (params.contains ·)
 
-  addDecl <| Declaration.thmDecl
-    { name := inductName, levelParams := us, type := eTyp, value := e' }
+    return .thmInfo
+      { name := inductName, levelParams := us, type := eTyp, value := e' }
   return inductName
 
 /--
@@ -752,14 +748,14 @@ def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit
 
   for name in names, idx in [:names.size] do
     let inductName := .append name `induct
-    unless ← hasConst inductName do
+    realizeConst name inductName .thm do
       let value ← forallTelescope ci.type fun xs _body => do
         let value := .const ci.name (levelParams.map mkLevelParam)
         let value := mkAppN value xs
         let value ← PProdN.projM names.size idx value
         mkLambdaFVars xs value
       let type ← inferType value
-      addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
+      return .thmInfo { name := inductName, levelParams, type, value }
 
 /--
 In the type of `value`, reduces
@@ -822,48 +818,47 @@ Takes `foo._unary.induct`, where the motive is a `PSigma`/`PSum` type and
 unpacks it into a n-ary and (possibly) joint induction principle.
 -/
 def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : MetaM Name := do
+  let baseName := eqnInfo.declNames[0]!
   let inductName := if eqnInfo.declNames.size > 1 then
-    .append eqnInfo.declNames[0]! `mutual_induct
+    .append baseName `mutual_induct
   else
     -- If there is no mutual recursion, we generate the `foo.induct` directly.
-    .append eqnInfo.declNames[0]! `induct
-  if ← hasConst inductName then return inductName
-
-  let ci ← getConstInfo unaryInductName
-  let us := ci.levelParams
-  let value := .const ci.name (us.map mkLevelParam)
-  let motivePos ← forallTelescope ci.type fun xs concl => concl.withApp fun motive targets => do
-    unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do
-      throwError "conclusion {concl} does not look like a packed motive application"
-    let packedTarget := targets[0]!
-    unless xs.back! == packedTarget do
-      throwError "packed target not last argument to {unaryInductName}"
-    let some motivePos := xs.findIdx? (· == motive)
-      | throwError "could not find motive {motive} in {xs}"
-    pure motivePos
-  let value ← forallBoundedTelescope ci.type motivePos fun params type => do
-    let value := mkAppN value params
-    eqnInfo.argsPacker.curryParam value type fun motives value type =>
-      -- Bring the rest into scope
-      forallTelescope type fun xs _concl => do
-        let alts := xs.pop
-        let value := mkAppN value alts
-        let value ← eqnInfo.argsPacker.curry value
-        let value ← mkLambdaFVars alts value
-        let value ← mkLambdaFVars motives value
-        let value ← mkLambdaFVars params value
-        check value
-        let value ← cleanPackedArgs eqnInfo value
-        return value
-
-  unless ← isTypeCorrect value do
-    logError m!"failed to unpack induction principle:{indentExpr value}"
-    check value
-  let type ← inferType value
-  let type ← elimOptParam type
-
-  addDecl <| Declaration.thmDecl
-    { name := inductName, levelParams := ci.levelParams, type, value }
+    .append baseName `induct
+  realizeConst baseName inductName .thm do
+    let ci ← getConstInfo unaryInductName
+    let us := ci.levelParams
+    let value := .const ci.name (us.map mkLevelParam)
+    let motivePos ← forallTelescope ci.type fun xs concl => concl.withApp fun motive targets => do
+      unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do
+        throwError "conclusion {concl} does not look like a packed motive application"
+      let packedTarget := targets[0]!
+      unless xs.back! == packedTarget do
+        throwError "packed target not last argument to {unaryInductName}"
+      let some motivePos := xs.findIdx? (· == motive)
+        | throwError "could not find motive {motive} in {xs}"
+      pure motivePos
+    let value ← forallBoundedTelescope ci.type motivePos fun params type => do
+      let value := mkAppN value params
+      eqnInfo.argsPacker.curryParam value type fun motives value type =>
+        -- Bring the rest into scope
+        forallTelescope type fun xs _concl => do
+          let alts := xs.pop
+          let value := mkAppN value alts
+          let value ← eqnInfo.argsPacker.curry value
+          let value ← mkLambdaFVars alts value
+          let value ← mkLambdaFVars motives value
+          let value ← mkLambdaFVars params value
+          check value
+          let value ← cleanPackedArgs eqnInfo value
+          return value
+
+    unless ← isTypeCorrect value do
+      logError m!"failed to unpack induction priciple:{indentExpr value}"
+      check value
+    let type ← inferType value
+    let type ← elimOptParam type
+
+    return .thmInfo { name := inductName, levelParams := ci.levelParams, type, value }
   return inductName
 
 
diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
index f03bd6625e37..6df5b9568019 100644
--- a/src/Lean/Meta/Tactic/Simp/Attr.lean
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -24,13 +24,13 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
         Attribute.add declName simprocAttrName stx attrKind
       else
         let go : MetaM Unit := do
-          let info ← getConstInfo declName
+          let info ← getAsyncConstInfo declName
           let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
           let inv := !stx[2].isNone
           let prio ← getAttrParamOptPrio stx[3]
-          if (← isProp info.type) then
+          if (← isProp info.sig.get.type) then
             addSimpTheorem ext declName post (inv := inv) attrKind prio
-          else if info.hasValue then
+          else if info.kind matches .defn then
             if inv then
               throwError "invalid '←' modifier, '{declName}' is a declaration name to be unfolded"
             if (← SimpTheorems.ignoreEquations declName) then
diff --git a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
index 8a22d23437ba..b1c41b5ed6dd 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
@@ -119,6 +119,6 @@ builtin_initialize
   }
 
 def getSimpCongrTheorems : CoreM SimpCongrTheorems :=
-  return congrExtension.getState (← getEnv)
+  return congrExtension.getState (asyncMode := .local) (← getEnv)
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 9d5e9fb39cfa..369c33ad29e3 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -151,6 +151,8 @@ mutual
         return false
 
   partial def isRflTheorem (declName : Name) : CoreM Bool := do
+    if !(← getEnv).contains declName && isReservedName (← getEnv) declName then
+      executeReservedNameAction declName
     let .thmInfo info ← getConstInfo declName | return false
     isRflProofCore info.type info.value
 end
@@ -399,8 +401,27 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
     return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
+private def realizePreprocessedSimpTheorems (declName : Name) (inv : Bool) : MetaM (Array Name) := withReducible do
+  let cinfo ← getConstVal declName
+  let us := cinfo.levelParams.map mkLevelParam
+  let val := mkConst declName us
+  let mut r := #[]
+  let type ← inferType val
+  for (val, type) in (← preprocess val type inv (isGlobal := true)) do
+    let mut name := declName ++ `_simp
+    if inv then
+      name := name ++ `inv
+    name := name.mkNum r.size
+    realizeConst declName name .thm do
+      return .thmInfo {
+        name,
+        levelParams := cinfo.levelParams, type, value := val
+      }
+    r := r.push name
+  return r
+
 private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) : MetaM (Array SimpTheorem) := do
-  let cinfo ← getConstInfo declName
+  let cinfo ← getConstVal declName
   let us := cinfo.levelParams.map mkLevelParam
   let origin := .decl declName post inv
   let val := mkConst declName us
@@ -408,14 +429,21 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
     let type ← inferType val
     checkTypeIsProp type
     if inv || (← shouldPreprocess type) then
-      let mut r := #[]
-      for (val, type) in (← preprocess val type inv (isGlobal := true)) do
-        let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false))
-      return r
+      (← realizePreprocessedSimpTheorems declName inv).mapM fun name =>
+        mkSimpTheoremCore origin (mkConst name us) #[] (mkConst name) post prio (noIndexAtArgs := false)
     else
       return #[← mkSimpTheoremCore origin (mkConst declName us) #[] (mkConst declName) post prio (noIndexAtArgs := false)]
 
+builtin_initialize
+  registerReservedNameAction fun name => do
+    let .num name _ := name | return false
+    let (name, inv) :=
+      if let .str name' "inv" := name then (name', true)
+      else (name, false)
+    let .str declName "_simp" := name | return false
+    let _ ← realizePreprocessedSimpTheorems declName inv |>.run
+    return true
+
 inductive SimpEntry where
   | thm      : SimpTheorem → SimpEntry
   | toUnfold : Name → SimpEntry
@@ -425,7 +453,7 @@ inductive SimpEntry where
 abbrev SimpExtension := SimpleScopedEnvExtension SimpEntry SimpTheorems
 
 def SimpExtension.getTheorems (ext : SimpExtension) : CoreM SimpTheorems :=
-  return ext.getState (← getEnv)
+  return ext.getState (asyncMode := .local) (← getEnv)
 
 def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv : Bool) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let simpThms ← mkSimpTheoremsFromConst declName post inv prio
@@ -458,7 +486,7 @@ def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (i
 
 def SimpTheorem.getValue (simpThm : SimpTheorem) : MetaM Expr := do
   if simpThm.proof.isConst && simpThm.levelParams.isEmpty then
-    let info ← getConstInfo simpThm.proof.constName!
+    let info ← getConstVal simpThm.proof.constName!
     if info.levelParams.isEmpty then
       return simpThm.proof
     else
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 204ad1907a4d..03719a0cd985 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -44,6 +44,7 @@ structure SimprocDeclExtState where
 def SimprocDecl.lt (decl₁ decl₂ : SimprocDecl) : Bool :=
   Name.quickLt decl₁.declName decl₂.declName
 
+-- asynchrony: only set by command-level `simproc_pattern%`
 builtin_initialize simprocDeclExt : PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState ←
   registerPersistentEnvExtension {
     mkInitial       := return { builtin := (← builtinSimprocDeclsRef.get).keys }
@@ -61,14 +62,14 @@ def getSimprocDeclKeys? (declName : Name) : CoreM (Option (Array SimpTheoremKey)
       let some decl := (simprocDeclExt.getModuleEntries env modIdx).binSearch { declName, keys := #[] } SimprocDecl.lt
         | pure none
       pure (some decl.keys)
-    | none        => pure ((simprocDeclExt.getState env).newEntries.find? declName)
+    | none        => pure ((simprocDeclExt.getState (asyncMode := .local) env).newEntries.find? declName)
   if let some keys := keys? then
     return some keys
   else
-    return (simprocDeclExt.getState env).builtin[declName]?
+    return (simprocDeclExt.getState (asyncMode := .local) env).builtin[declName]?
 
 def isBuiltinSimproc (declName : Name) : CoreM Bool := do
-  let s := simprocDeclExt.getState (← getEnv)
+  let s := simprocDeclExt.getState (asyncMode := .local) (← getEnv)
   return s.builtin.contains declName
 
 def isSimproc (declName : Name) : CoreM Bool :=
@@ -432,10 +433,10 @@ builtin_initialize
   }
 
 def getSimprocs : CoreM Simprocs :=
-  return simprocExtension.getState (← getEnv)
+  return simprocExtension.getState (asyncMode := .local) (← getEnv)
 
 def getSEvalSimprocs : CoreM Simprocs :=
-  return simprocSEvalExtension.getState (← getEnv)
+  return simprocSEvalExtension.getState (asyncMode := .local) (← getEnv)
 
 def getSimprocExtensionCore? (attrName : Name) : IO (Option SimprocExtension) :=
   return (← simprocExtensionMapRef.get)[attrName]?
diff --git a/src/Lean/Meta/Tactic/Symm.lean b/src/Lean/Meta/Tactic/Symm.lean
index 31b61ab08a18..32b2b38d1d20 100644
--- a/src/Lean/Meta/Tactic/Symm.lean
+++ b/src/Lean/Meta/Tactic/Symm.lean
@@ -51,7 +51,7 @@ namespace Lean.Expr
 def getSymmLems (tgt : Expr) : MetaM (Array Name) := do
   let .app (.app rel _) _ := tgt
     | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
-  (symmExt.getState (← getEnv)).getMatch rel
+  (symmExt.getState (asyncMode := .local) (← getEnv)).getMatch rel
 
 /-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
 def applySymm (e : Expr) : MetaM Expr := do
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 6b499228a3ed..bfb6d5bcaae2 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -102,7 +102,7 @@ def tryUnificationHints (t s : Expr) : MetaM Bool := do
     return false
   if t.isMVar then
     return false
-  let hints := unificationHintExtension.getState (← getEnv)
+  let hints := unificationHintExtension.getState (asyncMode := .local) (← getEnv)
   let candidates ← withConfigWithKey config <| hints.discrTree.getMatch t
   for candidate in candidates do
     if (← tryCandidate candidate) then
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index e52aaeef4db6..48fe69b78b61 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -25,21 +25,17 @@ def withEnv [Monad m] [MonadFinally m] [MonadEnv m] (env : Environment) (x : m 
     setEnv saved
 
 def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match (← getEnv).find? declName with
-  | some (ConstantInfo.inductInfo ..) => return true
-  | _ => return false
+  return (← getEnv).findAsync? declName matches some { kind := .induct, .. }
 
 def isRecCore (env : Environment) (declName : Name) : Bool :=
-  match env.find? declName with
-  | some (ConstantInfo.recInfo ..) => true
-  | _ => false
+  env.findAsync? declName matches some { kind := .recursor, .. }
 
 def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
   return isRecCore (← getEnv) declName
 
 @[inline] def withoutModifyingEnv [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α := do
   let env ← getEnv
-  try x finally setEnv env
+  try withEnv env.unlockAsync x finally setEnv env
 
 /-- Similar to `withoutModifyingEnv`, but also returns the updated environment -/
 @[inline] def withoutModifyingEnv' [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m (α × Environment) := do
@@ -94,8 +90,18 @@ def getConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Co
   | some info => pure info
   | none      => throwError "unknown constant '{.ofConstName constName}'"
 
+def getConstVal [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantVal := do
+  match (← getEnv).findConstVal? constName with
+  | some val => pure val
+  | none     => throwError "unknown constant '{mkConst constName}'"
+
+def getAsyncConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m AsyncConstantInfo := do
+  match (← getEnv).findAsync? constName with
+  | some val => pure val
+  | none     => throwError "unknown constant '{mkConst constName}'"
+
 def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do
-  let info ← getConstInfo constName
+  let info ← getConstVal constName
   return mkConst constName (info.levelParams.map mkLevelParam)
 
 def getConstInfoDefn [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m DefinitionVal := do
@@ -171,4 +177,18 @@ def isEnumType  [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Bool
   else
     return false
 
+def realizeConst [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] [MonadLiftT IO m] [MonadAlwaysExcept ε m]
+    (forConst : Name) (constName : Name) (kind : ConstantKind)
+    (doRealize : m ConstantInfo) (sig? : Option (Task ConstantVal) := none) : m Unit := do
+  let env ← getEnv
+  let (env, resolve?) ← env.realizeConst forConst constName kind sig?
+  setEnv env
+  if let some resolve := resolve? then
+    let _ := MonadAlwaysExcept.except (m := m)
+    try
+      let x ← doRealize
+      setEnv <| (← ofExceptKernelException (← resolve x |>.toBaseIO |> liftM (m := IO)))
+    catch _ =>
+      setEnv <| (← ofExceptKernelException (← resolve none |>.toBaseIO |> liftM (m := IO)))
+
 end Lean
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 2b7f0984c39e..f14cd4fc0f30 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1705,7 +1705,7 @@ builtin_initialize categoryParserFnRef : IO.Ref CategoryParserFn ← IO.mkRef fu
 builtin_initialize categoryParserFnExtension : EnvExtension CategoryParserFn ← registerEnvExtension $ categoryParserFnRef.get
 
 def categoryParserFn (catName : Name) : ParserFn := fun ctx s =>
-  let fn := categoryParserFnExtension.getState ctx.env
+  let fn := categoryParserFnExtension.getState (asyncMode := .local) ctx.env
   fn catName ctx s
 
 def categoryParser (catName : Name) (prec : Nat) : Parser where
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 87acbcfe343c..a91183ff88d0 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -346,7 +346,7 @@ builtin_initialize parserExtension : ParserExtension ←
   }
 
 def isParserCategory (env : Environment) (catName : Name) : Bool :=
-  (parserExtension.getState env).categories.contains catName
+  (parserExtension.getState (asyncMode := .local) env).categories.contains catName
 
 def addParserCategory (env : Environment) (catName declName : Name) (behavior : LeadingIdentBehavior) : Except String Environment := do
   if isParserCategory env catName then
@@ -355,12 +355,12 @@ def addParserCategory (env : Environment) (catName declName : Name) (behavior :
     return parserExtension.addEntry env <| ParserExtension.Entry.category catName declName behavior
 
 def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBehavior :=
-  match getCategory (parserExtension.getState env).categories catName with
+  match getCategory (parserExtension.getState (asyncMode := .local) env).categories catName with
   | none     => LeadingIdentBehavior.default
   | some cat => cat.behavior
 
 unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
-  let categories := (parserExtension.getState ctx.env).categories
+  let categories := (parserExtension.getState (asyncMode := .local) ctx.env).categories
   match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
   | .ok (_, p) =>
     -- We should manually register `p`'s tokens before invoking it as it might not be part of any syntax category (yet)
@@ -406,7 +406,7 @@ def mkCategoryAntiquotParser (kind : Name) : Parser :=
 
 def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s =>
   let catName := if catName == `syntax then `stx else catName -- temporary Hack
-  let categories := (parserExtension.getState ctx.env).categories
+  let categories := (parserExtension.getState (asyncMode := .local) ctx.env).categories
   match getCategory categories catName with
   | some cat =>
     prattParser catName cat.tables cat.behavior (mkCategoryAntiquotParserFn catName) ctx s
@@ -418,24 +418,24 @@ builtin_initialize
 def addToken (tk : Token) (kind : AttributeKind) : AttrM Unit := do
   -- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
   -- So, we must run it here to handle exception.
-  discard <| ofExcept <| addTokenConfig (parserExtension.getState (← getEnv)).tokens tk
+  discard <| ofExcept <| addTokenConfig (parserExtension.getState (asyncMode := .local) (← getEnv)).tokens tk
   parserExtension.add (ParserExtension.Entry.token tk) kind
 
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
   parserExtension.addEntry env <| ParserExtension.Entry.kind k
 
 def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
-  let kinds := (parserExtension.getState env).kinds
+  let kinds := (parserExtension.getState (asyncMode := .local) env).kinds
   -- accept any constant in stage 1 (i.e. when compiled by stage 0) so that
   -- we can add a built-in parser and its elaborator in the same stage
   kinds.contains k || (Internal.isStage0 () && env.contains k)
 
 def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind :=
-  let kinds := (parserExtension.getState env).kinds
+  let kinds := (parserExtension.getState (asyncMode := .local) env).kinds
   kinds.foldl (fun ks k _ => k::ks) []
 
 def getTokenTable (env : Environment) : TokenTable :=
-  (parserExtension.getState env).tokens
+  (parserExtension.getState (asyncMode := .local) env).tokens
 
 -- Note: `crlfToLf` preserves logical line and column numbers for each character.
 def mkInputContext (input : String) (fileName : String) (normalizeLineEndings := true) : InputContext :=
@@ -511,7 +511,7 @@ def registerBuiltinParserAttribute (attrName declName : Name)
 private def ParserAttribute.add (_attrName : Name) (catName : Name) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
   let prio ← Attribute.Builtin.getPrio stx
   let env ← getEnv
-  let categories := (parserExtension.getState env).categories
+  let categories := (parserExtension.getState (asyncMode := .local) env).categories
   let p ← mkParserOfConstant categories declName
   let leading    := p.1
   let parser     := p.2
@@ -574,7 +574,7 @@ private def withNamespaces (ids : Array Name) (addOpenSimple : Bool) : ParserFn
       let env := parserExtension.activateScoped env ns
       (env, openDecls)
     { c with env, openDecls }
-  let tokens := parserExtension.getState c.env |>.tokens
+  let tokens := parserExtension.getState (asyncMode := .local) c.env |>.tokens
   { c with tokens }
 
 def withOpenDeclFnCore (openDeclStx : Syntax) (p : ParserFn) : ParserFn := fun c s =>
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 44a435655a32..e18090392566 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -692,7 +692,7 @@ partial def delabAppMatch : Delab := whenNotPPOption getPPExplicit <| whenPPOpti
       (do
         let params := (← getExpr).getAppArgs
         let matcherTy : SubExpr :=
-          { expr := ← instantiateForall (← instantiateTypeLevelParams (← getConstInfo c) us) params
+          { expr := ← instantiateForall (← instantiateTypeLevelParams (← getConstVal c) us) params
             pos := (← getPos).pushType }
         guard <| ← isDefEq matcherTy.expr (← inferType (← getExpr))
         return { info, matcherTy })
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index 9873c4f4a4ba..657a6fa00c36 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -40,7 +40,7 @@ namespace Environment
 
 @[export lean_get_projection_info]
 def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
-  projectionFnInfoExt.find? env projName
+  projectionFnInfoExt.find? (asyncMode := .async) env projName
 
 def isProjectionFn (env : Environment) (declName : Name) : Bool :=
   projectionFnInfoExt.contains env declName
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index ab6bf712c3ac..ee7688e893ea 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -21,18 +21,15 @@ def ReducibilityStatus.toAttrString : ReducibilityStatus → String
   | .irreducible => "[irreducible]"
   | .semireducible => "[semireducible]"
 
-builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
-  registerPersistentEnvExtension {
+builtin_initialize reducibilityCoreExt : SimplePersistentEnvExtension (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
+  registerSimplePersistentEnvExtension {
     name            := `reducibilityCore
-    mkInitial       := pure {}
-    addImportedFn   := fun _ _ => pure {}
+    addImportedFn   := fun _ => {}
     addEntryFn      := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
-    exportEntriesFn := fun m =>
-      let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[]
-      r.qsort (fun a b => Name.quickLt a.1 b.1)
-    statsFn         := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
+    toArrayFn := fun a => a.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
   }
 
+-- asynchrony: only set immediately after declaration is added to environment
 builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←
   registerSimpleScopedEnvExtension {
     name := `reducibilityExtra
@@ -43,7 +40,7 @@ builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × Redu
 
 @[export lean_get_reducibility_status]
 def getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus :=
-  let m := reducibilityExtraExt.getState env
+  let m := reducibilityExtraExt.getState (asyncMode := .local) env
   if let some status := m.find? declName then
     status
   else match env.getModuleIdxFor? declName with
@@ -51,7 +48,7 @@ def getReducibilityStatusCore (env : Environment) (declName : Name) : Reducibili
     match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, status) => status
     | none => .semireducible
-  | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
+  | none => reducibilityCoreExt.findStateAsync env declName |>.find? declName |>.getD .semireducible
 
 private def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
   if attrKind matches .global then
diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean
index 930ae4f0be9c..1bdd26868f1a 100644
--- a/src/Lean/Replay.lean
+++ b/src/Lean/Replay.lean
@@ -127,7 +127,7 @@ when we replayed the inductives.
 -/
 def checkPostponedConstructors : M Unit := do
   for ctor in (← get).postponedConstructors do
-    match (← get).env.constants.find? ctor, (← read).newConstants[ctor]? with
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
     | some (.ctorInfo info), some (.ctorInfo info') =>
       if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}"
     | _, _ => throw <| IO.userError s!"No such constructor {ctor}"
@@ -138,7 +138,7 @@ when we replayed the inductives.
 -/
 def checkPostponedRecursors : M Unit := do
   for ctor in (← get).postponedRecursors do
-    match (← get).env.constants.find? ctor, (← read).newConstants[ctor]? with
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
     | some (.recInfo info), some (.recInfo info') =>
       if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}"
     | _, _ => throw <| IO.userError s!"No such recursor {ctor}"
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index a5167193d9fa..19dc481f0522 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -45,7 +45,7 @@ builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment
 Returns `true` if `name` is a reserved name.
 -/
 def isReservedName (env : Environment) (name : Name) : Bool :=
-  reservedNamePredicatesExt.getState env |>.any (· env name)
+  reservedNamePredicatesExt.getState (asyncMode := .local) env |>.any (· env name)
 
 /-!
   We use aliases to implement the `export <id> (<id>+)` command.
@@ -78,7 +78,7 @@ def getAliasState (env : Environment) : AliasState :=
   declarations that are not marked as `protected`.
 -/
 def getAliases (env : Environment) (a : Name) (skipProtected : Bool) : List Name :=
-  match aliasExtension.getState env |>.find? a with
+  match aliasExtension.getState (asyncMode := .local) env |>.find? a with
   | none    => []
   | some es =>
     if skipProtected then
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index 68e2e7ec3d44..fdda4f00ee5d 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -121,16 +121,16 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope
 opaque registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ)
 
 def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
-  let s := ext.ext.getState env
-  match s.stateStack with
-  | [] => env
-  | state :: stack => ext.ext.setState env { s with stateStack := state :: state :: stack }
+  ext.ext.modifyState env fun s =>
+    match s.stateStack with
+    | [] => s
+    | state :: stack => { s with stateStack := state :: state :: stack }
 
 def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
-  let s := ext.ext.getState env
-  match s.stateStack with
-  | _      :: state₂ :: stack => ext.ext.setState env { s with stateStack := state₂ :: stack }
-  | _ => env
+  ext.ext.modifyState env fun s =>
+    match s.stateStack with
+    | _      :: state₂ :: stack => { s with stateStack := state₂ :: stack }
+    | _ => s
 
 def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
   ext.ext.addEntry env (Entry.global b)
@@ -156,36 +156,37 @@ def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : Sc
   let ns ← getCurrNamespace
   modifyEnv (ext.addCore · b kind ns)
 
-def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
-  match ext.ext.getState env |>.stateStack with
+def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ)
+    (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode) : σ :=
+  match ext.ext.getState (asyncMode := asyncMode) env |>.stateStack with
   | top :: _ => top.state
   | _        => unreachable!
 
 def ScopedEnvExtension.activateScoped (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) : Environment :=
-  let s := ext.ext.getState env
-  match s.stateStack with
-  | top :: stack =>
-    if top.activeScopes.contains namespaceName then
-      env
-    else
-      let activeScopes := top.activeScopes.insert namespaceName
-      let top :=
-        match s.scopedEntries.map.find? namespaceName with
-        | none =>
-          { top with activeScopes := activeScopes }
-        | some bs => Id.run do
-          let mut state := top.state
-          for b in bs do
-            state := ext.descr.addEntry state b
-          { state := state, activeScopes := activeScopes }
-      ext.ext.setState env { s with stateStack := top :: stack }
-  | _ => env
+  ext.ext.modifyState env fun s =>
+    match s.stateStack with
+    | top :: stack =>
+      if top.activeScopes.contains namespaceName then
+        s
+      else
+        let activeScopes := top.activeScopes.insert namespaceName
+        let top :=
+          match s.scopedEntries.map.find? namespaceName with
+          | none =>
+            { top with activeScopes := activeScopes }
+          | some bs => Id.run do
+            let mut state := top.state
+            for b in bs do
+              state := ext.descr.addEntry state b
+            { state := state, activeScopes := activeScopes }
+        { s with stateStack := top :: stack }
+    | _ => s
 
 def ScopedEnvExtension.modifyState (ext : ScopedEnvExtension α β σ) (env : Environment) (f : σ → σ) : Environment :=
-  let s := ext.ext.getState env
-  match s.stateStack with
-  | top :: stack => ext.ext.setState env { s with stateStack := { top with state := f top.state } :: stack }
-  | _ => env
+  ext.ext.modifyState env fun s =>
+    match s.stateStack with
+    | top :: stack => { s with stateStack := { top with state := f top.state } :: stack }
+    | _ => s
 
 def pushScope [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 2fa0e7936b48..de445375d2a5 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -206,9 +206,8 @@ end Ilean
 
 /-- Gets the name of the module that contains `declName`. -/
 def getModuleContainingDecl? (env : Environment) (declName : Name) : Option Name := do
-  if env.constants.map₂.contains declName then
-    return env.header.mainModule
-  let modIdx ← env.getModuleIdxFor? declName
+  let some modIdx := env.getModuleIdxFor? declName
+    | env.header.mainModule
   env.allImportedModuleNames.get? modIdx
 
 /--
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 00fe3b994caa..654350be0e2f 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -122,7 +122,7 @@ def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name
 def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo :=
   match env.getModuleIdxFor? structName with
   | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt
-  | none        => structureExt.getState env |>.snd.map.find? structName
+  | none        => structureExt.getState (asyncMode := .async) env |>.snd.map.find? structName
 
 /--
 Gets the `StructureInfo` for `structName`, which is assumed to have been declared as a structure to the elaborator.
diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean
index cd1608bf652e..a25f65c7a0c1 100644
--- a/src/Lean/Util/FoldConsts.lean
+++ b/src/Lean/Util/FoldConsts.lean
@@ -72,12 +72,12 @@ def getUsedConstantsAsSet (c : ConstantInfo) : NameSet :=
 end ConstantInfo
 
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
-  e.foldConsts 0 fun constName max =>
-    match env.find? constName with
-    | ConstantInfo.defnInfo val =>
-      match val.hints with
-      | ReducibilityHints.regular h => if h > max then h else max
-      | _                           => max
-    | _ => max
+  e.foldConsts 0 fun constName max => Id.run do
+    if let some c := env.findAsync? constName then
+      if c.kind matches .defn then
+        if let .defnInfo { hints := .regular h, .. } := c.toConstantInfo then
+          if h > max then
+            return h
+    return max
 
 end Lean
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 22db50dd6a99..099aa729e1fe 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -214,35 +214,6 @@ invocations, which is the common case."
     -- milliseconds to seconds
     (trace.profiler.threshold.get o).toFloat / 1000
 
-/--
-`MonadExcept` variant that is expected to catch all exceptions of the given type in case the
-standard instance doesn't.
-
-In most circumstances, we want to let runtime exceptions during term elaboration bubble up to the
-command elaborator (see `Core.tryCatch`). However, in a few cases like building the trace tree, we
-really need to handle (and then re-throw) every exception lest we end up with a broken tree.
--/
-class MonadAlwaysExcept (ε : outParam (Type u)) (m : Type u → Type v) where
-  except : MonadExceptOf ε m
-
--- instances sufficient for inferring `MonadAlwaysExcept` for the elaboration monads
-
-instance : MonadAlwaysExcept ε (EIO ε) where
-  except := inferInstance
-
-instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateT σ m) where
-  except := let _ := always.except; inferInstance
-
-instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where
-  except := let _ := always.except; inferInstance
-
-instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where
-  except := let _ := always.except; inferInstance
-
-instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] :
-    MonadAlwaysExcept ε (MonadCacheT α β m) where
-  except := let _ := always.except; inferInstance
-
 def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)
     (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
   let _ := always.except
diff --git a/src/lean.mk.in b/src/lean.mk.in
index 1a37a59cf9e6..802049583d7a 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -22,7 +22,7 @@ BIN_OUT = $(OUT)/bin
 LIB_OUT = $(OUT)/lib
 BIN_NAME = $(PKG)
 STATIC_LIB_NAME = lib$(PKG).a
-LEAN_OPTS = @LEAN_EXTRA_MAKE_OPTS@
+LEAN_OPTS += @LEAN_EXTRA_MAKE_OPTS@
 LEANC_OPTS = -O3 -DNDEBUG
 LINK_OPTS =
 
@@ -163,5 +163,7 @@ clean:
 .PRECIOUS: $(BC_OUT)/%.bc $(C_OUT)/%.c $(TEMP_OUT)/%.o $(TEMP_OUT)/%.o.export
 
 ifndef C_ONLY
+ifndef UNSAFE_INCREMENTAL
 include $(DEPS)
 endif
+endif
diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp
index 6340fabf7b2d..e1c5767de043 100644
--- a/src/library/compiler/specialize.cpp
+++ b/src/library/compiler/specialize.cpp
@@ -954,13 +954,13 @@ class specialize_fn {
             return optional<comp_decl>();
         }
         lean_assert(!has_fvar(code));
-        /* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
+        /* We add the auxiliary declaration `n` as a "meta" axiom to the elab_environment.
            This is a hack to make sure we can use `csimp` to simplify `code` and
            other definitions that use `n`. `csimp` uses the kernel type checker to infer
            types, and it will fail to infer the type of `n`-applications if we do not have
-           an entry in the environment.
+           an entry in the elab_environment.
 
-           Remark: we mark the axiom as `meta` to make sure it does not pollute the environment
+           Remark: we mark the axiom as `meta` to make sure it does not pollute the elab_environment
            regular definitions.
 
            We also considered the following cleaner solution: modify `csimp` to use a custom
diff --git a/src/library/constructions/no_confusion.h b/src/library/constructions/no_confusion.h
index 951959c7fb02..6931ce498660 100644
--- a/src/library/constructions/no_confusion.h
+++ b/src/library/constructions/no_confusion.h
@@ -11,18 +11,18 @@ namespace lean {
 /** \brief Given an inductive datatype \c n (which is not a proposition) in \c env,
     returns the declaration for <tt>n.no_confusion_type</tt>.
 
-    \remark This procedure assumes the environment contains <tt>eq, n.cases_on</tt>.
-    If the environment has an impredicative Prop, it also assumes heq is defined.
-    If the environment does not have an impredicative Prop, then it also assumes lift is defined.
+    \remark This procedure assumes the elab_environment contains <tt>eq, n.cases_on</tt>.
+    If the elab_environment has an impredicative Prop, it also assumes heq is defined.
+    If the elab_environment does not have an impredicative Prop, then it also assumes lift is defined.
 */
 declaration mk_no_confusion_type(elab_environment const & env, name const & n);
 
 /** \brief Given an inductive datatype \c n (which is not a proposition) in \c env,
     returns the declaration for <tt>n.no_confusion</tt>.
 
-    \remark This procedure assumes the environment contains <tt>eq, n.cases_on, n.no_confusion_type</tt>.
-    If the environment has an impredicative Prop, it also assumes heq is defined.
-    If the environment does not have an impredicative Prop, then it also assumes lift is defined.
+    \remark This procedure assumes the elab_environment contains <tt>eq, n.cases_on, n.no_confusion_type</tt>.
+    If the elab_environment has an impredicative Prop, it also assumes heq is defined.
+    If the elab_environment does not have an impredicative Prop, then it also assumes lift is defined.
 */
 declaration mk_no_confusion(elab_environment const & env, name const & n);
 }
diff --git a/src/library/elab_environment.h b/src/library/elab_environment.h
index db21ccf13b49..c837592ed97c 100644
--- a/src/library/elab_environment.h
+++ b/src/library/elab_environment.h
@@ -38,6 +38,7 @@ class LEAN_EXPORT elab_environment : public object_ref {
 
     environment to_kernel_env() const;
 
+    // TODO: delete together with old compiler
     operator environment() const { return to_kernel_env(); }
 };
 }
diff --git a/src/runtime/interrupt.cpp b/src/runtime/interrupt.cpp
index 903f665a11df..76859465faed 100644
--- a/src/runtime/interrupt.cpp
+++ b/src/runtime/interrupt.cpp
@@ -65,18 +65,4 @@ void check_system(char const * component_name, bool do_check_interrupted) {
         check_heartbeat();
     }
 }
-
-void sleep_for(unsigned ms, unsigned step_ms) {
-    if (step_ms == 0)
-        step_ms = 1;
-    unsigned rounds = ms / step_ms;
-    chrono::milliseconds c(step_ms);
-    chrono::milliseconds r(ms % step_ms);
-    for (unsigned i = 0; i < rounds; i++) {
-        this_thread::sleep_for(c);
-        check_interrupted();
-    }
-    this_thread::sleep_for(r);
-    check_interrupted();
-}
 }
diff --git a/src/runtime/interrupt.h b/src/runtime/interrupt.h
index 14cf99385beb..9dd766bd5fd1 100644
--- a/src/runtime/interrupt.h
+++ b/src/runtime/interrupt.h
@@ -62,14 +62,4 @@ LEAN_EXPORT void check_interrupted();
    be a fatal error.
 */
 LEAN_EXPORT void check_system(char const * component_name, bool do_check_interrupted = false);
-
-constexpr unsigned g_small_sleep = 10;
-
-/**
-   \brief Put the current thread to sleep for \c ms milliseconds.
-
-   \remark check_interrupted is invoked every \c step_ms milliseconds;
-*/
-LEAN_EXPORT void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep);
-LEAN_EXPORT inline void sleep_for(chrono::milliseconds const & ms) { sleep_for(ms.count(), 10); }
 }
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index 13c3c30d40f8..1c66fbff5b26 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -31,6 +31,10 @@ Author: Jared Roesch
 #include <sys/syscall.h>
 #endif
 
+#ifdef __linux
+#include <sys/syscall.h>
+#endif
+
 #include "runtime/object.h"
 #include "runtime/io.h"
 #include "runtime/array_ref.h"
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index e678ff8b068e..28564b72c8dc 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "library/print.h"
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"
+#include "library/elab_environment.h"
 #include "util/path.h"
 #include "stdlib_flags.h"
 #ifdef _MSC_VER
@@ -229,7 +230,7 @@ static void display_help(std::ostream & out) {
     std::cout << "      --print-prefix     print the installation prefix for Lean and exit\n";
     std::cout << "      --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
     std::cout << "      --profile          display elaboration/type checking time for each definition/theorem\n";
-    std::cout << "      --stats            display environment statistics\n";
+    std::cout << "      --stats            display elab_environment statistics\n";
     DEBUG_CODE(
     std::cout << "      --debug=tag        enable assertions with the given tag\n";
         )
diff --git a/tests/Sublist.lean b/tests/Sublist.lean
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/tests/lean/kernelCheck.lean b/tests/lean/kernelCheck.lean
new file mode 100644
index 000000000000..7eb2552b9444
--- /dev/null
+++ b/tests/lean/kernelCheck.lean
@@ -0,0 +1,15 @@
+import Lean
+
+/-!
+The kernel should catch misbehaving tactics.
+NOTE that this test should **NOT** use `#guard_msgs` as it disables parallelism, which is the main
+thing we want to test here.
+-/
+
+open Lean Elab Tactic
+
+elab "wrong" : tactic => do
+  let mvar ← getMainGoal
+  mvar.assign <| .const ``True []
+
+theorem no : False := by wrong
diff --git a/tests/lean/kernelCheck.lean.expected.out b/tests/lean/kernelCheck.lean.expected.out
new file mode 100644
index 000000000000..47580695c0fc
--- /dev/null
+++ b/tests/lean/kernelCheck.lean.expected.out
@@ -0,0 +1,4 @@
+kernelCheck.lean:15:8-15:10: error: (kernel) declaration type mismatch, 'no' has type
+  Prop
+but it is expected to have type
+  False
diff --git a/tests/lean/run/4306.lean b/tests/lean/run/4306.lean
index 9a4d2017035b..3f574e966876 100644
--- a/tests/lean/run/4306.lean
+++ b/tests/lean/run/4306.lean
@@ -10,6 +10,7 @@ info: 12776324570088369205
 #guard_msgs in
 #eval (123456789012345678901).toUInt64.toNat
 
+set_option trace.Elab.snapshotTree true
 /--
 error: tactic 'native_decide' evaluated that the proposition
   (Nat.toUInt64 123456789012345678901).toNat = 123456789012345678901
diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean
index b6c4d3d0c4bf..531eef1d5d69 100644
--- a/tests/lean/run/grind_pattern2.lean
+++ b/tests/lean/run/grind_pattern2.lean
@@ -54,6 +54,8 @@ info: [grind.internalize] foo x y
 [grind.internalize] x
 [grind.internalize] y
 [grind.internalize] z
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs (info) in
 set_option trace.grind.internalize true in
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 0f91fc58530d..30a4873500b9 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -194,6 +194,8 @@ info: [grind.issues] found congruence between
     and
       f a
     but functions have different types
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs (info) in
 set_option trace.grind.issues true in
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index db3cdf24fcf0..8d1685226a75 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -19,7 +19,7 @@ inst✝ inst : α
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.78 : Inhabited α
+inst.75 : Inhabited α
 inst inst : α
 ⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder