docstrings on builtin simprocs

[nomeata]

Consider

-- import Lean
set_option linter.unusedSimpArgs false
example : True := by simp [BitVec.reduceEq]

hovering over the simproc it just says

A simp lemma specification is:

    optional ↑ or ↓ to specify use before or after entering the subterm
    optional ← to use the lemma backward
    thm for the theorem to rewrite with

but if I add import Lean I see the more helpful

BitVec.reduceEq : Lean.Meta.Simp.Simproc

Simplification procedure for = on BitVecs.

import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

So somehow builtin simprocs don't get their docstrings show. Smells a bit like #8432, but my attempt at fixing this using

diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean
index f188250d14..759c1a1a57 100644
--- a/src/Init/Simproc.lean
+++ b/src/Init/Simproc.lean
@@ -122,13 +122,13 @@ macro_rules
 macro_rules
   | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
     let simprocType := `Lean.Meta.Simp.Simproc
-    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+    `($[$doc?:docComment]? @[builtin_doc] def $n:ident : $(mkIdent simprocType) := $body
       builtin_simproc_pattern% $pattern => $n)
 
 macro_rules
   | `($[$doc?:docComment]? builtin_dsimproc_decl $n:ident ($pattern:term) := $body) => do
     let simprocType := `Lean.Meta.Simp.DSimproc
-    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+    `($[$doc?:docComment]? @[builtin_doc] def $n:ident : $(mkIdent simprocType) := $body
       builtin_simproc_pattern% $pattern => $n)

did not help.

Version

Lean 4.24.0-nightly-2025-09-14