From 7f4d673d33fd062f5f59f87c60b11ada4e64638b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Jul 2025 16:41:49 +0200
Subject: [PATCH] perf: make `builtin_initialize` backing def private (#9540)

---
 src/Lean/Elab/Declaration.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index c96e15cb56..7e83a64501 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -343,7 +343,10 @@ def elabMutual : CommandElab := fun stx => do
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let attrs := (attrs?.map (·.getElems)).getD #[]
       let attrs := attrs.push (← `(Lean.Parser.Term.attrInstance| $attrId:ident))
-      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
+      -- `[builtin_init]` can be private as it is used for local codegen only but `[init]` must be
+      -- available for the interpreter.
+      let privTk? := guard (attrId.getId == `builtin_init) *> some .missing
+      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $[private%$privTk?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
   | _ => throwUnsupportedSyntax
 
 builtin_initialize