From 9328271dd0e3710fcc7224db4eddaa79d2b9c8fc Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 23 Jul 2025 11:50:29 +0200
Subject: [PATCH] perf: do not export LCNF decls of closed terms (#9484)

This was only necessary when `isDeclMeta` and `isDeclPublic` were
intertwined
---
 src/Lean/Compiler/LCNF/Passes.lean     |  3 +--
 src/Lean/Compiler/LCNF/Visibility.lean | 13 +++++--------
 2 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index 1f91664bd5..9b22447b09 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -111,10 +111,9 @@ def builtinPassManager : PassManager := {
     extendJoinPointContext (phase := .mono) (occurrence := 1),
     simp (occurrence := 5) (phase := .mono),
     cse (occurrence := 2) (phase := .mono),
+    Pass.inferVisibility .mono,
     saveMono,  -- End of mono phase
     extractClosed,
-    -- should come last so it can see all created decls
-    Pass.inferVisibility .mono
   ]
 }
 
diff --git a/src/Lean/Compiler/LCNF/Visibility.lean b/src/Lean/Compiler/LCNF/Visibility.lean
index fdfc882499..fc136c0f3d 100644
--- a/src/Lean/Compiler/LCNF/Visibility.lean
+++ b/src/Lean/Compiler/LCNF/Visibility.lean
@@ -35,28 +35,25 @@ private def isBodyRelevant (decl : Decl) : CompilerM Bool := do
 partial def inferVisibility (phase : Phase) (decls : Array Decl) : CompilerM Unit := do
   if !(← getEnv).header.isModule then
     return
-  -- We want to visit closed term decls as well but they are not found by `getDecl`, so make sure to
-  -- always search in `decls` first.
-  let locals := decls.foldl (init := {}) fun l d => l.insert d.name d
   for decl in decls do
     if `_at_ ∈ decl.name.components then  -- TODO: don't?
       trace[Compiler.inferVisibility] m!"Marking {decl.name} as transparent because it is a specialization"
-      markPublic locals decl
+      markPublic decl
     else if (← getEnv).setExporting true |>.contains decl.name then
       trace[Compiler.inferVisibility] m!"Marking {decl.name} as opaque because it is a public def"
-      markPublic locals decl
+      markPublic decl
 where
-  markPublic (locals : NameMap Decl) (decl : Decl) : CompilerM Unit := do
+  markPublic (decl : Decl) : CompilerM Unit := do
     modifyEnv (setDeclPublic · decl.name)
     if (← isBodyRelevant decl) && !isDeclTransparent (← getEnv) phase decl.name then
       trace[Compiler.inferVisibility] m!"Marking {decl.name} as transparent because it is opaque and its body looks relevant"
       modifyEnv (setDeclTransparent · phase decl.name)
       decl.value.forCodeM fun code =>
         for ref in collectUsedDecls code do
-          if let some refDecl ← pure (locals.find? ref) <||> getLocalDecl? ref then
+          if let some refDecl ← getLocalDecl? ref then
             if !isDeclPublic (← getEnv) ref then
               trace[Compiler.inferVisibility] m!"Marking {ref} as opaque because it is used by transparent {decl.name}"
-              markPublic locals refDecl
+              markPublic refDecl
 
 builtin_initialize
   registerTraceClass `Compiler.inferVisibility