perf: avoid re-exporting imported doc expanders

src/tests/Tests.lean

@@ -8,6 +8,7 @@ import Tests.Elab
 import Tests.GenericCode
 import Tests.Golden
 import Tests.CommentSkipping
+import Tests.DocElabExtensions.Use
 import Tests.HighlightedToTeX
 import Tests.Html
 import Tests.HtmlEntities

src/tests/Tests/DocElabExtensions/Define.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import VersoManual
+
+namespace Verso.Tests.DocElabExtensions
+
+open Verso Genre Manual
+open Verso.Doc.Elab
+open Lean
+
+@[role]
+def inheritedRole : RoleExpanderOf Unit
+  | (), _contents => ``(Doc.Inline.text "inherited role")
+
+@[code_block]
+def inheritedCode : CodeBlockExpanderOf Unit
+  | (), str => ``(Doc.Block.code $(quote str.getString))
+
+@[directive]
+def inheritedDirective : DirectiveExpanderOf Unit
+  | (), blocks => do
+    let blocks ← blocks.mapM elabBlock
+    ``(Doc.Block.concat #[$blocks,*])
+
+@[block_command]
+def inheritedCommand : BlockCommandOf Unit
+  | () => ``(Doc.Block.para #[Doc.Inline.text "inherited command"])
+
+end Verso.Tests.DocElabExtensions

src/tests/Tests/DocElabExtensions/Middle.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Tests.DocElabExtensions.Define
+
+namespace Verso.Tests.DocElabExtensions
+
+def importedThroughMiddle : Bool := true
+
+end Verso.Tests.DocElabExtensions

src/tests/Tests/DocElabExtensions/Use.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import Tests.DocElabExtensions.Middle
+
+namespace Verso.Tests.DocElabExtensions
+
+open Verso Genre Manual
+
+#docs (Manual) inheritedDocElabExtensions "Inherited Doc Elab Extensions" :=
+:::::::
+This custom {inheritedRole}[] is provided through a transitive import.
+
+```inheritedCode
+code block body
+```
+
+:::inheritedDirective
+Directive body
+:::
+
+{inheritedCommand}
+:::::::
+
+#guard importedThroughMiddle
+#guard inheritedDocElabExtensions.toPart.content.size == 4
+
+end Verso.Tests.DocElabExtensions

src/verso/Verso/Doc/Elab/Monad.lean

@@ -549,18 +549,36 @@ unsafe def blockExpandersForUnsafe (x : Name) : DocElabM (Array BlockExpander) :
 @[implemented_by blockExpandersForUnsafe]
 public opaque blockExpandersFor (x : Name) : DocElabM (Array BlockExpander)
 
-initialize expanderSignatureExt : PersistentEnvExtension (Name × SigDoc) (Name × SigDoc) (NameMap SigDoc) ←
+private def addSignatureEntry (entries : NameMap SigDoc) (key : Name) (value : SigDoc) :
+    NameMap SigDoc :=
+  entries.insert key value
+
+private def importSignatureEntries (entrySets : Array (Array (Name × SigDoc))) :
+    NameMap SigDoc :=
+  entrySets.foldl (init := {}) fun entries entrySet =>
+    entrySet.foldl (init := entries) fun entries (key, value) =>
+      addSignatureEntry entries key value
+
+public structure SignatureExtensionState where
+  allEntries : NameMap SigDoc := {}
+  localEntries : NameMap SigDoc := {}
+  deriving Inhabited
+
+private def SignatureExtensionState.addEntry (state : SignatureExtensionState) (key : Name)
+    (value : SigDoc) : SignatureExtensionState :=
+  { allEntries := addSignatureEntry state.allEntries key value
+    localEntries := addSignatureEntry state.localEntries key value }
+
+initialize expanderSignatureExt : PersistentEnvExtension (Name × SigDoc) (Name × SigDoc) SignatureExtensionState ←
   registerPersistentEnvExtension {
-    mkInitial := pure {},
+    mkInitial := pure {}
     addImportedFn xss :=
-      pure <| xss.foldl (init := {}) fun ns xs =>
-        xs.foldl (init := ns) fun ns (x, s) =>
-          ns.insert x s
+      pure { allEntries := importSignatureEntries xss, localEntries := {} }
     addEntryFn
       | xs, (x, y) =>
-        xs.insert x y
+        xs.addEntry x y
     exportEntriesFn xs :=
-      xs.toArray
+      xs.localEntries.toArray
   }
 
 public def sig (α) [inst : FromArgs α DocElabM] : Option ArgParse.SigDoc :=
@@ -579,6 +597,31 @@ unsafe def partCommandsForUnsafe (x : Name) : PartElabM (Array PartCommand) := d
 public opaque partCommandsFor (x : Name) : PartElabM (Array PartCommand)
 
 
+private def addExpanderEntry (entries : NameMap (Array Name)) (key value : Name) :
+    NameMap (Array Name) :=
+  entries.insert key <| (entries.find? key |>.getD #[]).push value
+
+private def addExpanderEntries (entries : NameMap (Array Name)) (key : Name) (values : Array Name) :
+    NameMap (Array Name) :=
+  values.foldl (init := entries) fun entries value =>
+    addExpanderEntry entries key value
+
+private def importExpanderEntries (entrySets : Array (Array (Name × Array Name))) :
+    NameMap (Array Name) :=
+  entrySets.foldl (init := {}) fun entries entrySet =>
+    entrySet.foldl (init := entries) fun entries (key, values) =>
+      addExpanderEntries entries key values
+
+public structure ExpanderExtensionState where
+  allEntries : NameMap (Array Name) := {}
+  localEntries : NameMap (Array Name) := {}
+  deriving Inhabited
+
+private def ExpanderExtensionState.addEntry (state : ExpanderExtensionState) (key value : Name) :
+    ExpanderExtensionState :=
+  { allEntries := addExpanderEntry state.allEntries key value
+    localEntries := addExpanderEntry state.localEntries key value }
+
 public abbrev RoleExpander := Array Arg → TSyntaxArray `inline → DocElabM (Array (TSyntax `term))
 
 public abbrev RoleExpanderOf α := α → TSyntaxArray `inline → DocElabM Term
@@ -595,26 +638,24 @@ public section
 syntax (name := role) "role " (ident)? : attr
 end
 
-initialize roleExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+initialize roleExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) ExpanderExtensionState ←
   registerPersistentEnvExtension {
-    mkInitial := pure {},
+    mkInitial := pure {}
     addImportedFn xss :=
-      pure <| xss.foldl (init := {}) fun ns xs =>
-        xs.foldl (init := ns) fun ns (x, ys) =>
-          ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+      pure { allEntries := importExpanderEntries xss, localEntries := {} }
     addEntryFn
       | xs, (x, y) =>
-        xs.insert x (xs.find? x |>.getD #[] |>.push y)
+        xs.addEntry x y
     exportEntriesFn xs :=
-      xs.toArray
+      xs.localEntries.toArray
   }
 
 private unsafe def roleExpandersForUnsafe' (x : Name) : DocElabM (Array (RoleExpander × Option String × Option SigDoc)) := do
-  let expanders := roleExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+  let expanders := roleExpanderExt.getState (← getEnv) |>.allEntries.find? x |>.getD #[]
   expanders.mapM fun n => do
     let e ← evalConst RoleExpander n
     let doc? ← findDocString? (← getEnv) n
-    let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+    let sig := expanderSignatureExt.getState (← getEnv) |>.allEntries.find? n
     return (e, doc?, sig)
 
 private unsafe def roleExpandersForUnsafe'' (x : Name) : DocElabM (Array RoleExpander) := do
@@ -723,18 +764,16 @@ public def toCodeBlock {α : Type} [FromArgs α DocElabM] (expander : α → Str
 
 syntax (name := code_block) "code_block " (ident)? : attr
 
-initialize codeBlockExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+initialize codeBlockExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) ExpanderExtensionState ←
   registerPersistentEnvExtension {
-    mkInitial := pure {},
+    mkInitial := pure {}
     addImportedFn xss :=
-      pure <| xss.foldl (init := {}) fun ns xs =>
-        xs.foldl (init := ns) fun ns (x, ys) =>
-          ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+      pure { allEntries := importExpanderEntries xss, localEntries := {} }
     addEntryFn
       | xs, (x, y) =>
-        xs.insert x (xs.find? x |>.getD #[] |>.push y)
+        xs.addEntry x y
     exportEntriesFn xs :=
-      xs.toArray
+      xs.localEntries.toArray
   }
 
 unsafe initialize registerBuiltinAttribute {
@@ -787,11 +826,11 @@ unsafe initialize registerBuiltinAttribute {
 }
 
 private unsafe def codeBlockExpandersForUnsafe' (x : Name) : DocElabM (Array (CodeBlockExpander × Option String × Option SigDoc)) := do
-  let expanders := codeBlockExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+  let expanders := codeBlockExpanderExt.getState (← getEnv) |>.allEntries.find? x |>.getD #[]
   expanders.mapM fun n => do
     let e ← evalConst CodeBlockExpander n
     let doc? ← findDocString? (← getEnv) n
-    let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+    let sig := expanderSignatureExt.getState (← getEnv) |>.allEntries.find? n
     return (e, doc?, sig)
 
 private unsafe def codeBlockExpandersForUnsafe'' (x : Name) : DocElabM (Array CodeBlockExpander) := do
@@ -819,18 +858,16 @@ public def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSy
 
 syntax (name := directive) "directive " (ident)? : attr
 
-initialize directiveExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+initialize directiveExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) ExpanderExtensionState ←
   registerPersistentEnvExtension {
-    mkInitial := pure {},
+    mkInitial := pure {}
     addImportedFn xss :=
-      pure <| xss.foldl (init := {}) fun ns xs =>
-        xs.foldl (init := ns) fun ns (x, ys) =>
-          ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+      pure { allEntries := importExpanderEntries xss, localEntries := {} }
     addEntryFn
       | xs, (x, y) =>
-        xs.insert x (xs.find? x |>.getD #[] |>.push y)
+        xs.addEntry x y
     exportEntriesFn xs :=
-      xs.toArray
+      xs.localEntries.toArray
   }
 
 unsafe initialize registerBuiltinAttribute {
@@ -883,11 +920,11 @@ unsafe initialize registerBuiltinAttribute {
 }
 
 private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do
-  let expanders := directiveExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+  let expanders := directiveExpanderExt.getState (← getEnv) |>.allEntries.find? x |>.getD #[]
   expanders.mapM fun n => do
     let e ← evalConst DirectiveExpander n
     let doc? ← findDocString? (← getEnv) n
-    let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+    let sig := expanderSignatureExt.getState (← getEnv) |>.allEntries.find? n
     return (e, doc?, sig)
 
 private unsafe def directiveExpandersForUnsafe'' (x : Name) : DocElabM (Array DirectiveExpander) := do
@@ -915,18 +952,16 @@ public def toBlockCommand {α : Type} [FromArgs α DocElabM] (expander : α →
 
 syntax (name := block_command) "block_command " (ident)? : attr
 
-initialize blockCommandExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) (NameMap (Array Name)) ←
+initialize blockCommandExpanderExt : PersistentEnvExtension (Name × Array Name) (Name × Name) ExpanderExtensionState ←
   registerPersistentEnvExtension {
-    mkInitial := pure {},
+    mkInitial := pure {}
     addImportedFn xss :=
-      pure <| xss.foldl (init := {}) fun ns xs =>
-        xs.foldl (init := ns) fun ns (x, ys) =>
-          ns.insert x <| (ns.find? x |>.getD #[]) ++ ys
+      pure { allEntries := importExpanderEntries xss, localEntries := {} }
     addEntryFn
       | xs, (x, y) =>
-        xs.insert x (xs.find? x |>.getD #[] |>.push y)
+        xs.addEntry x y
     exportEntriesFn xs :=
-      xs.toArray
+      xs.localEntries.toArray
   }
 
 unsafe initialize registerBuiltinAttribute {
@@ -978,11 +1013,11 @@ unsafe initialize registerBuiltinAttribute {
 }
 
 private unsafe def blockCommandExpandersForUnsafe' (x : Name) : DocElabM (Array (BlockCommandExpander × Option String × Option SigDoc)) := do
-  let expanders := blockCommandExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
+  let expanders := blockCommandExpanderExt.getState (← getEnv) |>.allEntries.find? x |>.getD #[]
   expanders.mapM fun n => do
     let e ← evalConst BlockCommandExpander n
     let doc? ← findDocString? (← getEnv) n
-    let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
+    let sig := expanderSignatureExt.getState (← getEnv) |>.allEntries.find? n
     return (e, doc?, sig)
 
 private unsafe def blockCommandExpandersForUnsafe'' (x : Name) : DocElabM (Array BlockCommandExpander) := do