diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 4a06fbc2c70f..2c15998566c1 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -51,6 +51,9 @@ structure AttributeImpl extends AttributeImplCore where
   /-- This is run when the attribute is applied to a declaration `decl`. `stx` is the syntax of the attribute including arguments. -/
   add (decl : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit
   erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
+  /-- Implementations should push an `attr` syntax corresponding to (a best approximation of)
+  the attribute state for the given definition. -/
+  delab (decl : Name) : StateT (Array (TSyntax `attr)) AttrM Unit
   deriving Inhabited
 
 builtin_initialize attributeMapRef : IO.Ref (Std.HashMap Name AttributeImpl) ← IO.mkRef {}
@@ -134,6 +137,15 @@ structure TagAttribute where
   ext  : PersistentEnvExtension Name Name NameSet
   deriving Inhabited
 
+namespace TagAttribute
+
+private def hasTagCore (ext : PersistentEnvExtension Name Name NameSet) (env : Environment) (decl : Name) : Bool :=
+  match env.getModuleIdxFor? decl with
+  | some modIdx => (ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
+  | none        => (ext.getState env).contains decl
+
+end TagAttribute
+
 def registerTagAttribute (name : Name) (descr : String)
     (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO TagAttribute := do
   let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
@@ -156,6 +168,9 @@ def registerTagAttribute (name : Name) (descr : String)
         throwError "invalid attribute '{name}', declaration is in an imported module"
       validate decl
       modifyEnv fun env => ext.addEntry env decl
+    delab := fun decl => do
+      if TagAttribute.hasTagCore ext (← getEnv) decl then
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident))
   }
   registerBuiltinAttribute attrImpl
   return { attr := attrImpl, ext := ext }
@@ -163,9 +178,7 @@ def registerTagAttribute (name : Name) (descr : String)
 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
+  hasTagCore attr.ext env decl
 
 end TagAttribute
 
@@ -182,10 +195,21 @@ structure ParametricAttribute (α : Type) where
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   getParam : Name → Syntax → AttrM α
+  delabParam : Name → α → StateT (Array (TSyntax `attr)) AttrM Unit
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
 
-def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
+def ParametricAttribute.getParam?Core [Inhabited α]
+    (ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
+    (env : Environment) (decl : Name) : Option α :=
+  match env.getModuleIdxFor? decl with
+  | some modIdx =>
+    match (ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
+    | some (_, val) => some val
+    | none          => none
+  | none        => (ext.getState env).find? decl
+
+def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
     name            := impl.ref
     mkInitial       := pure {}
@@ -198,7 +222,7 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
   }
   let attrImpl : AttributeImpl := {
     impl.toAttributeImplCore with
-    add   := fun decl stx kind => do
+    add := fun decl stx kind => do
       unless kind == AttributeKind.global do throwError "invalid attribute '{impl.name}', must be global"
       let env ← getEnv
       unless (env.getModuleIdxFor? decl).isNone do
@@ -206,6 +230,9 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
       let val ← impl.getParam decl stx
       modifyEnv fun env => ext.addEntry env (decl, val)
       try impl.afterSet decl val catch _ => setEnv env
+    delab := fun decl => do
+      if let some val := ParametricAttribute.getParam?Core ext (← getEnv) decl then
+        impl.delabParam decl val
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl, ext := ext }
@@ -213,12 +240,7 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
 namespace ParametricAttribute
 
 def getParam? [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : 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
+  getParam?Core attr.ext env decl
 
 def setParam (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
@@ -239,7 +261,17 @@ structure EnumAttributes (α : Type) where
   ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
   deriving Inhabited
 
-def registerEnumAttributes (attrDescrs : List (Name × String × α))
+private def EnumAttributes.getValueCore [Inhabited α]
+    (ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
+    (env : Environment) (decl : Name) : Option α :=
+  match env.getModuleIdxFor? decl with
+  | some modIdx =>
+    match (ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
+    | some (_, val) => some val
+    | none          => none
+  | none        => (ext.getState env).find? decl
+
+def registerEnumAttributes [Inhabited α] [BEq α] (attrDescrs : List (Name × String × α))
     (validate : Name → α → AttrM Unit := fun _ _ => pure ())
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
     (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
@@ -265,6 +297,10 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
         throwError "invalid attribute '{name}', declaration is in an imported module"
       validate decl val
       modifyEnv fun env => ext.addEntry env (decl, val)
+    delab           := fun decl => do
+      if let some v := EnumAttributes.getValueCore ext (← getEnv) decl then
+        if v == val then
+          modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident))
     applicationTime := applicationTime
     : AttributeImpl
   }
@@ -274,12 +310,7 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
 namespace EnumAttributes
 
 def getValue [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : 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
+  getValueCore attr.ext env decl
 
 def setValue (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
@@ -377,6 +408,11 @@ def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do
   | some attr => pure attr
   | none      => throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'"))
 
+def delabAttributesOfDecl (declName : Name) : AttrM (Array (TSyntax `attr)) := do
+  let m ← attributeMapRef.get
+  let act := m.forM fun _ attr => attr.delab declName
+  (·.2) <$> act.run #[]
+
 @[export lean_attribute_application_time]
 def getBuiltinAttributeApplicationTime (n : Name) : IO AttributeApplicationTime := do
   let attr ← getBuiltinAttributeImpl n
diff --git a/src/Lean/BuiltinDocAttr.lean b/src/Lean/BuiltinDocAttr.lean
index ab12c9cfed87..49316b8a1ecb 100644
--- a/src/Lean/BuiltinDocAttr.lean
+++ b/src/Lean/BuiltinDocAttr.lean
@@ -22,6 +22,7 @@ builtin_initialize
     add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       declareBuiltinDocStringAndRanges decl
+    delab := fun _ => pure ()
   }
 
 end Lean
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index e591e7805d25..5ba0e7be0509 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -169,6 +169,9 @@ builtin_initialize
       unless kind == AttributeKind.global do throwError "invalid attribute 'class', must be global"
       let env ← ofExcept (addClass env decl)
       setEnv env
+    delab := fun decl => do
+      if isClass (← getEnv) decl then
+        modify (·.push <| Unhygienic.run `(attr| class))
   }
 
 end Lean
diff --git a/src/Lean/Compiler/CSimpAttr.lean b/src/Lean/Compiler/CSimpAttr.lean
index 1fad0e367b4d..6550f1e6c866 100644
--- a/src/Lean/Compiler/CSimpAttr.lean
+++ b/src/Lean/Compiler/CSimpAttr.lean
@@ -48,15 +48,6 @@ def add (declName : Name) (kind : AttributeKind) : CoreM Unit := do
   else
     throwError "invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
 
-builtin_initialize
-  registerBuiltinAttribute {
-    name  := `csimp
-    descr := "simplification theorem for the compiler"
-    add   := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      discard <| add declName attrKind
-  }
-
 @[export lean_csimp_replace_constants]
 def replaceConstants (env : Environment) (e : Expr) : Expr :=
   let s := ext.getState env
@@ -73,4 +64,16 @@ end CSimp
 def hasCSimpAttribute (env : Environment) (declName : Name) : Bool :=
   CSimp.ext.getState env |>.thmNames.contains declName
 
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `csimp
+    descr := "simplification theorem for the compiler"
+    add   := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      discard <| CSimp.add declName attrKind
+    delab := fun declName => do
+      if hasCSimpAttribute (← getEnv) declName then
+        modify (·.push <| Unhygienic.run `(attr| csimp))
+  }
+
 end Lean.Compiler
diff --git a/src/Lean/Compiler/ExportAttr.lean b/src/Lean/Compiler/ExportAttr.lean
index 2fafe73c2e8d..f360c5870d0a 100644
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@@ -26,6 +26,8 @@ builtin_initialize exportAttr : ParametricAttribute Name ←
       unless isValidCppName exportName do
         throwError "invalid 'export' function name, is not a valid C++ identifier"
       return exportName
+    delabParam := fun _ exportName => do
+      modify (·.push <| Unhygienic.run `(attr| export $(mkIdent exportName)))
   }
 
 @[export lean_get_export_name_for]
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index b7eb708e3566..f626eddc1d44 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -57,6 +57,20 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
       entries := entries.push <| ExternEntry.inline backend str
   return { arity? := arity?, entries := entries.toList }
 
+private def externAttrDataToSyntax (data : ExternAttrData) : AttrM (TSyntax `attr) := do
+  let arity? := data.arity?.map Syntax.mkNatLit
+  let mut entries := #[]
+  unless data matches {arity? := none, entries := [.adhoc `all]} do
+    for entry in data.entries do
+      let (inline, backend, str) ←  match entry with
+        | .standard backend str => pure (none, backend, str)
+        | .inline backend str => pure (some (mkAtom "inline"), backend, str)
+        | _ => continue
+      let backend := if backend == `all then none else some (mkIdent backend)
+      entries := entries.push <| mkNode `Lean.Parser.Attr.externEntry #[
+        mkOptionalNode backend, mkOptionalNode inline, Syntax.mkStrLit str]
+  `(attr| extern $(arity?)? $entries*)
+
 @[extern "lean_add_extern"]
 opaque addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
 
@@ -73,6 +87,9 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
           return ()
         let env ← ofExcept <| addExtern env declName
         setEnv env
+    delabParam := fun decl val => do
+      let stx ← externAttrDataToSyntax val
+      modify (·.push stx)
   }
 
 @[export lean_get_extern_attr_data]
diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index 9d2aae8115d0..6e6f0896ea79 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -28,6 +28,9 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
     if decl.name == fnDecl.name then
       throwError "invalid 'implemented_by' argument '{fnName}', function cannot be implemented by itself"
     return fnName
+  delabParam := fun _ val => do
+    let val ← unresolveNameGlobal val
+    modify (·.push <| Unhygienic.run `(attr| implemented_by $(mkIdent val):ident))
 }
 
 @[export lean_get_implemented_by]
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index 212e3c6de316..eddab0374c23 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -56,6 +56,12 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       | none =>
         if isIOUnit decl.type then pure Name.anonymous
         else throwError "initialization function must have type `IO Unit`"
+    delabParam := fun _ val => do
+      if val.isAnonymous then
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent attrName):ident))
+      else
+        let val ← unresolveNameGlobal val
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent attrName):ident $(mkIdent val)))
     afterImport := fun entries => do
       let ctx ← read
       if runAfterImport && (← isInitializerExecutionEnabled) then
diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index 1356a0a4b4a1..9012fc0d5394 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -116,6 +116,7 @@ builtin_initialize
       Attribute.Builtin.ensureNoArgs stx
       unless kind == AttributeKind.global do throwError "invalid attribute 'cpass', must be global"
       discard <| addPass declName
+    delab := fun _ => pure ()
     applicationTime := .afterCompilation
   }
 
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
index dc17f83b19b2..01a116ff4539 100644
--- a/src/Lean/Compiler/Specialize.lean
+++ b/src/Lean/Compiler/Specialize.lean
@@ -46,6 +46,9 @@ builtin_initialize specializeAttr : ParametricAttribute (Array Nat) ←
     getParam := fun declName stx => do
       let args := stx[1].getArgs
       elabSpecArgs declName args |>.run'
+    delabParam := fun declName val => do
+      let val := val.map fun n => Syntax.mkNatLit (n + 1)
+      modify (·.push <| Unhygienic.run `(attr| specialize $val*))
   }
 
 def getSpecializationArgs? (env : Environment) (declName : Name) : Option (Array Nat) :=
diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
index ecc5f316517e..a458a3b4c7b5 100644
--- a/src/Lean/Elab/InheritDoc.lean
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -27,4 +27,5 @@ builtin_initialize
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"
+    delab := fun _ => pure ()
   }
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index a895c7dc04db..778c97fbcc60 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -23,12 +23,18 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
     return m ++ "}"
 
 private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
+  let attrs ← liftCoreM <| delabAttributesOfDecl id
   let m : MessageData :=
-    match (← getReducibilityStatus id) with
-    | ReducibilityStatus.irreducible => "@[irreducible] "
-    | ReducibilityStatus.reducible => "@[reducible] "
-    | ReducibilityStatus.semireducible => ""
-  let m :=
+    if attrs.isEmpty then
+      ""
+    else
+      -- This sorting is not perfect, but we need to do some sorting here because
+      -- otherwise the attributes come out in random order which causes problems for reproducibility
+      let key {k} (stx : TSyntax k) := (stx.raw.getKind, stx.raw[0].getKind)
+      have : Ord (Name × Name) := Ord.lex ⟨Name.cmp⟩ ⟨Name.cmp⟩
+      let attrs := attrs.qsort (fun a b => compare (key a) (key b) = .lt)
+      "@[" ++ MessageData.joinSep (attrs.toList.map fun s => .ofSyntax s.raw) ", " ++ "] "
+    let m :=
     m ++
     match safety with
     | DefinitionSafety.unsafe  => "unsafe "
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
index bfca67675de2..a5e14380e54a 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
@@ -58,12 +58,12 @@ def addBVNormalizeProcBuiltinAttr (declName : Name) (post : Bool) (proc : Sum Si
 
 builtin_initialize
   registerBuiltinAttribute {
-    ref             := by exact decl_name%
     name            := `bvNormalizeProcBuiltinAttr
     descr           := "Builtin bv_normalize simproc"
     applicationTime := AttributeApplicationTime.afterCompilation
     erase           := fun _ => throwError "Not implemented yet, [-builtin_bv_normalize_proc]"
     add             := fun declName stx _ => addBuiltin declName stx ``addBVNormalizeProcBuiltinAttr
+    delab           := fun _ => pure ()
   }
 
 end Frontend
diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean
index 837c8d61dc4f..4f8004694fe7 100644
--- a/src/Lean/Elab/Tactic/Ext.lean
+++ b/src/Lean/Elab/Tactic/Ext.lean
@@ -261,6 +261,12 @@ builtin_initialize registerBuiltinAttribute {
     -- Realize iff theorem
     if iff then
       discard <| liftCommandElabM <| withRef stx <| realizeExtIffTheorem declName
+  delab := fun decl => do
+    if let some {priority, .. : ExtTheorem} := (extExtension.getState (← getEnv)).tree.fold
+      (fun o _ v => o <|> guard (v.declName == decl) *> pure v) none
+    then
+      let prio := if priority = eval_prio default then none else some (Syntax.mkNatLit priority)
+      modify (·.push <| Unhygienic.run `(attr| ext $[$prio:num]?))
   erase := fun declName => do
     let s := extExtension.getState (← getEnv)
     let s ← s.erase declName
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 62e688d21515..debd85d98828 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -2158,6 +2158,9 @@ builtin_initialize
       unless kind == AttributeKind.global do
         throwError "invalid attribute 'builtin_incremental', must be global"
       declareBuiltin decl <| mkApp (mkConst ``addBuiltinIncrementalElab) (toExpr decl)
+    delab           := fun decl => do
+      if (← builtinIncrementalElabs.get).contains decl then
+        modify (·.push <| Unhygienic.run `(attr| builtin_incremental))
   }
 
 /-- Checks whether a declaration is annotated with `[builtin_incremental]` or `[incremental]`. -/
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index bcc608cd311a..b4f2db117991 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -122,6 +122,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact de
       ref   := attrDeclName
       name  := df.builtinName
       descr := "(builtin) " ++ df.descr
+      delab := fun _ => pure ()
       add   := fun declName stx kind => do
         unless kind == AttributeKind.global do throwError "invalid attribute '{df.builtinName}', must be global"
         let key ← df.evalKey true stx
@@ -145,6 +146,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact de
       let s := ext.getState (← getEnv)
       let s ← s.erase df.name declName
       modifyEnv fun env => ext.modifyState env fun _ => s
+    delab           := fun _ => pure ()
     add             := fun declName stx attrKind => do
       let key ← df.evalKey false stx
       match IR.getSorryDep (← getEnv) declName with
diff --git a/src/Lean/LabelAttribute.lean b/src/Lean/LabelAttribute.lean
index 43d79e31b80d..b5d4a2d44731 100644
--- a/src/Lean/LabelAttribute.lean
+++ b/src/Lean/LabelAttribute.lean
@@ -54,6 +54,9 @@ registerBuiltinAttribute {
   applicationTime := AttributeApplicationTime.afterCompilation
   add   := fun declName _ kind =>
     ext.add declName kind
+  delab := fun declName => do
+    if (ext.getState (← getEnv)).contains declName then
+      modify (·.push <| Unhygienic.run `(attr| $(mkIdent attrName):ident))
   erase := fun declName => do
     let s := ext.getState (← getEnv)
     modifyEnv fun env => ext.modifyState env fun _ => s.erase declName
diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean
index 0e6428888586..d161177a24ef 100644
--- a/src/Lean/Linter/Deprecated.lean
+++ b/src/Lean/Linter/Deprecated.lean
@@ -32,6 +32,11 @@ builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
       let text? := text?.map TSyntax.getString
       let since? := since?.map TSyntax.getString
       return { newName?, text?, since? }
+    delabParam := fun _ { newName?, text?, since? } => do
+      let id? ← newName?.mapM (mkIdent <$> unresolveNameGlobal ·)
+      let text? := text?.map Syntax.mkStrLit
+      let since? := since?.map Syntax.mkStrLit
+      modify (·.push <| Unhygienic.run `(attr| deprecated $(id?)? $(text?)? $[(since := $since?)]?))
   }
 
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 6df6d7473f90..edade2457abc 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -97,6 +97,7 @@ builtin_initialize
         declareBuiltin declName <| mkApp2 (mkConst ``addBuiltinHandler) (toExpr key) h
       else
         setEnv <| missingDocsExt.addEntry env (declName, key, ← mkHandler declName)
+    delab           := fun _ => pure ()
   }
   mkAttr true `builtin_missing_docs_handler
   mkAttr false `missing_docs_handler
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 5cefd948e5c7..f2e8a85b296c 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -181,6 +181,7 @@ builtin_initialize
         declareBuiltin decl <| mkApp (mkConst ``addBuiltinUnusedVariablesIgnoreFn) h
       else
         setEnv <| unusedVariablesIgnoreFnsExt.addEntry env (decl, ← mkIgnoreFn decl)
+    delab           := fun _ => pure ()
   }
   mkAttr true `builtin_unused_variables_ignore_fn
   mkAttr false `unused_variables_ignore_fn
diff --git a/src/Lean/Meta/CoeAttr.lean b/src/Lean/Meta/CoeAttr.lean
index 0509cd2b2217..4fa27c3a3b0d 100644
--- a/src/Lean/Meta/CoeAttr.lean
+++ b/src/Lean/Meta/CoeAttr.lean
@@ -82,6 +82,9 @@ builtin_initialize registerBuiltinAttribute {
     unless kind == .global do
       throwError "cannot add local or scoped coe attribute"
     registerCoercion decl
+  delab := fun decl => do
+    if let some _ ← getCoeFnInfo? decl then
+      modify (·.push <| Unhygienic.run `(attr| coe))
 }
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index d7802c3d4c1a..bb77bc5e9a1b 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -232,19 +232,6 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
-builtin_initialize
-  registerBuiltinAttribute {
-    name  := `instance
-    descr := "type class instance"
-    add   := fun declName stx attrKind => do
-      let prio ← getAttrParamOptPrio stx[1]
-      discard <| addInstance declName attrKind prio |>.run {} {}
-    erase := fun declName => do
-      let s := instanceExtension.getState (← getEnv)
-      let s ← s.erase declName
-      modifyEnv fun env => instanceExtension.modifyState env fun _ => s
-  }
-
 def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
   return Meta.instanceExtension.getState (← getEnv) |>.discrTree
 
@@ -265,6 +252,22 @@ def getInstanceAttrKind? (declName : Name) : CoreM (Option AttributeKind) := do
   let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none
   return entry.attrKind
 
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `instance
+    descr := "type class instance"
+    add   := fun declName stx attrKind => do
+      let prio ← getAttrParamOptPrio stx[1]
+      discard <| addInstance declName attrKind prio |>.run {} {}
+    delab := fun declName => do
+      if ← isInstance declName then
+        modify (·.push <| Unhygienic.run `(attr| instance))
+    erase := fun declName => do
+      let s := instanceExtension.getState (← getEnv)
+      let s ← s.erase declName
+      modifyEnv fun env => instanceExtension.modifyState env fun _ => s
+  }
+
 /-! # Default instance support -/
 
 structure DefaultInstanceEntry where
@@ -311,6 +314,16 @@ builtin_initialize
       let prio ← getAttrParamOptPrio stx[1]
       unless kind == AttributeKind.global do throwError "invalid attribute 'default_instance', must be global"
       discard <| addDefaultInstance declName prio |>.run {} {}
+    delab := fun declName => do
+      -- TODO: this is a global search, which could be slow. Maybe add a reverse lookup?
+      for (_, ls) in defaultInstanceExtension.getState (← getEnv) |>.defaultInstances do
+        for (inst, prio) in ls do
+          if inst == declName then
+            let prio :=
+              if prio = eval_prio default then none
+              else some (Syntax.mkNumLit (toString prio))
+            modify (·.push <| Unhygienic.run `(attr| default_instance $(prio)?))
+            return
   }
   registerTraceClass `Meta.synthOrder
 
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index f2693bf6d6c8..1c1a297559d6 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -231,6 +231,8 @@ builtin_initialize recursorAttribute : ParametricAttribute Nat ←
     name := `recursor,
     descr := "user defined recursor, numerical parameter specifies position of the major premise",
     getParam := fun _ stx => Attribute.Recursor.getMajorPos stx
+    delabParam := fun _ val =>
+      modify (·.push <| Unhygienic.run `(attr| recursor $(Syntax.mkNatLit (val+1))))
     afterSet := fun declName majorPos => do
       discard <| mkRecursorInfoCore declName (some majorPos) |>.run'
   }
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 0ada47e2eedf..d2454ed530bd 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -177,6 +177,7 @@ builtin_initialize
     descr := "custom `rec`-like eliminator for the `induction` tactic"
     add   := fun declName _ attrKind => do
       discard <| addCustomEliminator declName attrKind (induction := true) |>.run {} {}
+    delab := fun _ => pure ()
   }
 
 builtin_initialize
@@ -185,6 +186,7 @@ builtin_initialize
     descr := "custom `casesOn`-like eliminator for the `cases` tactic"
     add   := fun declName _ attrKind => do
       discard <| addCustomEliminator declName attrKind (induction := false) |>.run {} {}
+    delab := fun _ => pure ()
   }
 
 /-- Gets all the eliminators defined using the `@[induction_eliminator]` and `@[cases_eliminator]` attributes. -/
diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean
index 0fb78c9186db..892b9fe651ea 100644
--- a/src/Lean/Meta/Tactic/Grind/Attr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Attr.lean
@@ -64,6 +64,9 @@ builtin_initialize
     add   := fun declName _ attrKind => do
       validateGrindCasesAttr declName
       grindCasesExt.add declName attrKind
+    delab := fun decl => do
+      if ← isGrindCasesTarget decl then
+        modify (·.push <| Unhygienic.run `(attr| grind_cases))
   }
 
 end Lean.Meta.Grind
diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean
index d727d309c841..ef7f4d6e9c5c 100644
--- a/src/Lean/Meta/Tactic/NormCast.lean
+++ b/src/Lean/Meta/Tactic/NormCast.lean
@@ -159,6 +159,7 @@ builtin_initialize registerBuiltinAttribute {
     | "squash" => addSquash decl kind prio
     | none => addInfer decl kind prio
     | _ => unreachable!
+  delab := fun _ => pure ()
 }
 
 end Lean.Meta.NormCast
diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index bb55f734c86a..8a1ea6613e17 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -41,6 +41,9 @@ initialize registerBuiltinAttribute {
     unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
     let key ← DiscrTree.mkPath rel
     reflExt.add (decl, key) kind
+  delab := fun decl => do
+    if (reflExt.getState (← getEnv)).foldValues (· || decl == ·) false then
+      modify (·.push <| Unhygienic.run `(attr| refl))
 }
 
 open Elab Tactic
diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
index f03bd6625e37..88cbe6bfdcc7 100644
--- a/src/Lean/Meta/Tactic/Simp/Attr.lean
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -46,6 +46,15 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
           else
             throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
         discard <| go.run {} {}
+    delab := fun declName => do
+      if attrName == `simp then -- TODO: other simp-like attrs
+        let s := ext.getState (← getEnv)
+        if s.isLemma (.decl declName) ||
+          s.isDeclToUnfold declName || s.toUnfoldThms.contains declName
+        then
+          modify (·.push <| Unhygienic.run `(attr| simp))
+        else if s.isLemma (.decl declName (inv := true)) then
+          modify (·.push <| Unhygienic.run `(attr| simp ←))
     erase := fun declName => do
       if (← isSimproc declName <||> isBuiltinSimproc declName) then
         let simprocAttrName := simpAttrNameToSimprocAttrName attrName
diff --git a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
index 8a22d23437ba..16737b967f52 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
@@ -116,6 +116,7 @@ builtin_initialize
     add   := fun declName stx attrKind => do
       let prio ← getAttrParamOptPrio stx[1]
       discard <| addSimpCongrTheorem declName attrKind prio |>.run {} {}
+    delab := fun _ => pure ()
   }
 
 def getSimpCongrTheorems : CoreM SimpCongrTheorems :=
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 204ad1907a4d..f7ab3ce3984b 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -374,6 +374,10 @@ def addSimprocAttr (ext : SimprocExtension) (declName : Name) (stx : Syntax) (at
     addSimprocAttrCore ext declName attrKind post
   discard <| go.run {} {}
 
+def printSimprocAttr (ext : SimprocExtension) (declName : Name) : StateT (Array (TSyntax `attr)) AttrM Unit := do
+  if (ext.getState (← getEnv)).simprocNames.contains declName then
+    modify (·.push <| Unhygienic.run `(attr| simproc)) -- FIXME: pre/post
+
 def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do
   registerBuiltinAttribute {
     ref   := name
@@ -381,6 +385,7 @@ def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension
     descr := attrDescr
     applicationTime := AttributeApplicationTime.afterCompilation
     add   := addSimprocAttr ext
+    delab := printSimprocAttr ext
     erase := eraseSimprocAttr ext
   }
 
@@ -413,22 +418,22 @@ private def addBuiltin (declName : Name) (stx : Syntax) (addDeclName : Name) : A
 
 builtin_initialize
   registerBuiltinAttribute {
-    ref             := by exact decl_name%
     name            := `simprocBuiltinAttr
     descr           := "Builtin simplification procedure"
     applicationTime := AttributeApplicationTime.afterCompilation
     erase           := fun _ => throwError "Not implemented yet, [-builtin_simproc]"
     add             := fun declName stx _ => addBuiltin declName stx ``addSimprocBuiltinAttr
+    delab           := fun _ => pure ()
   }
 
 builtin_initialize
   registerBuiltinAttribute {
-    ref             := by exact decl_name%
     name            := `sevalprocBuiltinAttr
     descr           := "Builtin symbolic evaluation procedure"
     applicationTime := AttributeApplicationTime.afterCompilation
     erase           := fun _ => throwError "Not implemented yet, [-builtin_sevalproc]"
     add             := fun declName stx _ => addBuiltin declName stx ``addSEvalprocBuiltinAttr
+    delab           := fun _ => pure ()
   }
 
 def getSimprocs : CoreM Simprocs :=
diff --git a/src/Lean/Meta/Tactic/Symm.lean b/src/Lean/Meta/Tactic/Symm.lean
index 31b61ab08a18..aae91f54386e 100644
--- a/src/Lean/Meta/Tactic/Symm.lean
+++ b/src/Lean/Meta/Tactic/Symm.lean
@@ -39,6 +39,9 @@ builtin_initialize registerBuiltinAttribute {
     let .app (.app rel _) _ := targetTy | fail
     let key ← withReducible <| DiscrTree.mkPath rel
     symmExt.add (decl, key) kind
+  delab := fun decl => do
+    if (symmExt.getState (← getEnv)).foldValues (· || decl == ·) false then
+      modify (·.push <| Unhygienic.run `(attr| symm))
 }
 
 end Lean.Meta.Symm
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 6b499228a3ed..8ad25164a583 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -94,6 +94,9 @@ builtin_initialize
     add   := fun declName stx kind => do
       Attribute.Builtin.ensureNoArgs stx
       discard <| addUnificationHint declName kind |>.run
+    delab := fun decl => do
+      if (unificationHintExtension.getState (← getEnv)).discrTree.foldValues (· || decl == ·) false then
+        modify (·.push <| Unhygienic.run `(attr| unification_hint))
   }
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 87acbcfe343c..b7f9173bfb18 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -318,6 +318,7 @@ builtin_initialize
     add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       runParserAttributeHooks Name.anonymous decl (builtin := true)
+    delab := fun _ => pure ()
   }
 
 builtin_initialize
@@ -327,6 +328,7 @@ builtin_initialize
     add   := fun decl stx _ => do
       Attribute.Builtin.ensureNoArgs stx
       runParserAttributeHooks Name.anonymous decl (builtin := false)
+    delab := fun _ => pure ()
   }
 
 private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → ImportM Entry
@@ -491,6 +493,20 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   declareBuiltinDocStringAndRanges declName
   runParserAttributeHooks catName declName (builtin := true)
 
+private def BuiltinParserAttribute.print (attrName : Name) (catName : Name)
+    (declName : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit := do
+  let prio ← Attribute.Builtin.getPrio stx
+  unless kind == AttributeKind.global do throwError "invalid attribute '{attrName}', must be global"
+  let decl ← getConstInfo declName
+  match decl.type with
+  | Expr.const `Lean.Parser.TrailingParser _ =>
+    declareTrailingBuiltinParser catName declName prio
+  | Expr.const `Lean.Parser.Parser _ =>
+    declareLeadingBuiltinParser catName declName prio
+  | _ => throwError "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)"
+  declareBuiltinDocStringAndRanges declName
+  runParserAttributeHooks catName declName (builtin := true)
+
 /--
 The parsing tables for builtin parsers are "stored" in the extracted source code.
 -/
@@ -505,6 +521,7 @@ def registerBuiltinParserAttribute (attrName declName : Name)
     name            := attrName
     descr           := "Builtin parser"
     add             := fun declName stx kind => liftM $ BuiltinParserAttribute.add attrName catName declName stx kind
+    delab           := fun _ => pure ()
     applicationTime := AttributeApplicationTime.afterCompilation
   }
 
@@ -535,6 +552,7 @@ def mkParserAttributeImpl (attrName catName : Name) (ref : Name := by exact decl
   name                      := attrName
   descr                     := "parser"
   add declName stx attrKind := ParserAttribute.add attrName catName declName stx attrKind
+  delab                     := fun _ => pure ()
   applicationTime           := AttributeApplicationTime.afterCompilation
 
 /-- A builtin parser attribute that can be extended by users. -/
diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean
index 8b4d25cd073a..bbf1926e6ea8 100644
--- a/src/Lean/Parser/Tactic/Doc.lean
+++ b/src/Lean/Parser/Tactic/Doc.lean
@@ -89,6 +89,11 @@ builtin_initialize
       if (← findSimpleDocString? (← getEnv) decl).isSome then
         logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
 
+    delab := fun decl => do
+      if let some tgt := alternativeOfTactic (← getEnv) decl then
+        let tgt ← unresolveNameGlobal tgt
+        modify (·.push <| Unhygienic.run `(attr| tactic_alt $(Lean.mkIdent tgt)))
+
     descr :=
       "Register a tactic parser as an alternative form of an existing tactic, so they " ++
       "can be grouped together in documentation.",
@@ -213,6 +218,12 @@ builtin_initialize
               m!"(expected {suggestions})"
 
           throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
+
+    delab := fun decl => do
+      if let some tags := (tacticTagExt.getState (← getEnv)).find? decl then
+        let tags := tags.fold (·.push <| Lean.mkIdent ·) #[]
+        modify (·.push <| Unhygienic.run `(attr| tactic_tag $tags*))
+
     descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
       "grouped together in documentation.",
     -- This runs prior to elaboration because it allows a check for whether the decl is present
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index a8bc59e06081..59544a0f7493 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -32,6 +32,10 @@ def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by
       let env ← getEnv
       let parserDeclName ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
       setEnv <| ext.addEntry env (parserDeclName, decl)
+    delab := fun decl => do
+      if let some val := (ext.getState (← getEnv)).find? decl then
+        let val ← unresolveNameGlobal val
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident $(mkIdent val)))
   }
   registerBuiltinAttribute attrImpl
   pure { impl := attrImpl, ext := ext }
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index ab6bf712c3ac..3aa9938fa9ae 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -133,6 +133,10 @@ private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Synta
   let ns ← getCurrNamespace
   modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns
 
+private def printAttr (status : ReducibilityStatus) (attrName : Name) (declName : Name) : StateT (Array (TSyntax `attr)) AttrM Unit := do
+  if getReducibilityStatusCore (← getEnv) declName == status then
+    modify (·.push <| Unhygienic.run `(attr| $(mkIdent attrName):ident))
+
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
@@ -140,6 +144,7 @@ builtin_initialize
     descr           := "irreducible declaration"
     add             := addAttr .irreducible
     applicationTime := .afterTypeChecking
+    delab           := printAttr .irreducible `irreducible
  }
 
 builtin_initialize
@@ -149,6 +154,7 @@ builtin_initialize
     descr           := "reducible declaration"
     add             := addAttr .reducible
     applicationTime := .afterTypeChecking
+    delab           := printAttr .reducible `reducible
  }
 
 builtin_initialize
@@ -158,6 +164,7 @@ builtin_initialize
     descr           := "semireducible declaration"
     add             := addAttr .semireducible
     applicationTime := .afterTypeChecking
+    delab           := fun _ => pure ()
  }
 
 /-- Return the reducibility attribute for the given declaration. -/
diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean
index 231751893d62..2386298cbad8 100644
--- a/src/Lean/Server/CodeActions/Attr.lean
+++ b/src/Lean/Server/CodeActions/Attr.lean
@@ -54,6 +54,7 @@ builtin_initialize
         throwError "invalid attribute 'hole_code_action', must be global"
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       modifyEnv (holeCodeActionExt.addEntry · (decl, ← mkHoleCodeAction decl))
+    delab := fun _ => pure ()
   }
 
 /-- A command code action extension. -/
@@ -124,6 +125,7 @@ builtin_initialize
       let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
+    delab := fun _ => pure ()
   }
 
 private def addBuiltin (declName : Name) (args : Array Name) : AttrM Unit := do
@@ -135,7 +137,6 @@ private def addBuiltin (declName : Name) (args : Array Name) : AttrM Unit := do
 
 builtin_initialize
   registerBuiltinAttribute {
-    ref             := by exact decl_name%
     name            := `builtin_command_code_action
     descr           := "Declare a new builtin command code action, to appear in the code actions on commands"
     applicationTime := .afterCompilation
@@ -147,4 +148,5 @@ builtin_initialize
       let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       addBuiltin decl args
+    delab := fun _ => pure ()
   }
diff --git a/src/Lean/Server/CodeActions/Basic.lean b/src/Lean/Server/CodeActions/Basic.lean
index 43963cac6dc3..b5036e546a2e 100644
--- a/src/Lean/Server/CodeActions/Basic.lean
+++ b/src/Lean/Server/CodeActions/Basic.lean
@@ -97,6 +97,9 @@ builtin_initialize
         declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
       else
         setEnv <| codeActionProviderExt.addEntry env decl
+    delab           := fun decl => do
+      if (codeActionProviderExt.getState (← getEnv)).contains decl then
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident))
   }
   mkAttr true `builtin_code_action_provider
   mkAttr false `code_action_provider
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index b4905d359e42..f8842ccc62a8 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -135,6 +135,9 @@ builtin_initialize registerBuiltinAttribute {
   applicationTime := AttributeApplicationTime.afterCompilation
   add := fun decl _ _ =>
     registerRpcProcedure decl
+  delab := fun decl => do
+    if userRpcProcedures.contains (← getEnv) decl then
+      modify (·.push <| Unhygienic.run `(attr| server_rpc_method))
 }
 
 end Lean.Server
diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index f4debf21abd1..dcdba304313b 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -103,6 +103,9 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ←
           declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinModule) (toExpr decl) h
         else
           setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
+      delab           := fun decl => do
+        if (moduleRegistry.getState (← getEnv)).fold (fun b _ x => b || decl == x.1) false then
+          modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident))
     }
     registerBuiltinAttribute impl
     return impl
diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean
index 7c89acd56cb8..38f19c2005d3 100644
--- a/src/lake/Lake/DSL/Attributes.lean
+++ b/src/lake/Lake/DSL/Attributes.lean
@@ -18,5 +18,6 @@ initialize
       logWarningAt stx "@[test_runner] has been deprecated, use @[test_driver] instead"
       testDriverAttr.attr.add decl stx attrKind
     applicationTime := testDriverAttr.attr.applicationTime
+    delab           := fun decl => testDriverAttr.attr.delab decl
     erase           := fun decl => testDriverAttr.attr.erase decl
  }
diff --git a/src/lake/Lake/Util/OrderedTagAttribute.lean b/src/lake/Lake/Util/OrderedTagAttribute.lean
index a486a380a28f..1c78eebd1035 100644
--- a/src/lake/Lake/Util/OrderedTagAttribute.lean
+++ b/src/lake/Lake/Util/OrderedTagAttribute.lean
@@ -13,6 +13,11 @@ structure OrderedTagAttribute where
   ext  : PersistentEnvExtension Name Name (Array Name)
   deriving Inhabited
 
+private def OrderedTagAttribute.hasTagCore (ext : PersistentEnvExtension Name Name (Array Name)) (env : Environment) (decl : Name) : Bool :=
+  match env.getModuleIdxFor? decl with
+  | some modIdx => (ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
+  | none        => (ext.getState env).contains decl
+
 def registerOrderedTagAttribute (name : Name) (descr : String)
     (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) : IO OrderedTagAttribute := do
   let ext ← registerPersistentEnvExtension {
@@ -35,14 +40,15 @@ def registerOrderedTagAttribute (name : Name) (descr : String)
         throwError "invalid attribute '{name}', declaration is in an imported module"
       validate decl
       modifyEnv fun env => ext.addEntry env decl
+    delab := fun decl => do
+      if OrderedTagAttribute.hasTagCore ext (← getEnv) decl then
+        modify (·.push <| Unhygienic.run `(attr| $(mkIdent name):ident))
   }
   registerBuiltinAttribute attrImpl
   return { attr := attrImpl, ext }
 
 def OrderedTagAttribute.hasTag (attr : OrderedTagAttribute) (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
+  hasTagCore attr.ext env decl
 
 /-- Get all tagged declaration names, both those imported and those in the current module. -/
 def OrderedTagAttribute.getAllEntries (attr : OrderedTagAttribute) (env : Environment) : Array Name :=