perf: do not export opaque bodies (#10119)

In particular, do not export `partial` bodies

src/Init/Dynamic.lean

@@ -14,7 +14,8 @@ public section
 open Lean
 
 -- Implementation detail of TypeName, since classes cannot be opaque
-private opaque TypeNameData (α : Type u) : NonemptyType.{0} :=
+-- TODO: should be private; #10098
+opaque TypeNameData (α : Type u) : NonemptyType.{0} :=
   ⟨Name, inferInstance⟩
 
 /--

src/Lean/AddDecl.lean

@@ -94,6 +94,10 @@ def addDecl (decl : Declaration) : CoreM Unit := do
       if (← getEnv).header.isModule && !(← getEnv).isExporting then
         exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
       pure (defn.name, .defnInfo defn, .defn)
+    | .opaqueDecl op =>
+      if (← getEnv).header.isModule && !(← getEnv).isExporting then
+        exportedInfo? := some <| .axiomInfo { op with }
+      pure (op.name, .opaqueInfo op, .opaque)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← doAdd)
 

src/Lean/Compiler/IR/EmitC.lean

@@ -102,9 +102,7 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
   let env ← getEnv
   if ps.isEmpty then
     if isExternal then emit "extern "
-    -- The first half is a pre-module system approximation, we keep it around for the benefit of
-    -- unported code.
-    else if isClosedTermName env decl.name || !Compiler.LCNF.isDeclPublic env decl.name then emit "static "
+    else if isClosedTermName env decl.name then emit "static "
     else emit "LEAN_EXPORT "
   else
     if !isExternal then emit "LEAN_EXPORT "

tests/bench/identifier_completion.lean

@@ -3,12 +3,10 @@ import Lean.AddDecl
 
 open Lean
 
-set_option debug.skipKernelTC true
-
 def buildSyntheticEnv : Lean.CoreM Unit := do
   for i in [0:100000] do
     let name := s!"Long.And.Hopefully.Unique.Name.foo{i}".toName
-    addDecl <| Declaration.opaqueDecl {
+    let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl {
       name := name
       levelParams := []
       type := .const `Nat []
@@ -16,6 +14,7 @@ def buildSyntheticEnv : Lean.CoreM Unit := do
       isUnsafe := false
       all := [name]
     }
+    setEnv env'
     addDocStringCore name "A synthetic doc-string"
 
 #eval buildSyntheticEnv

tests/bench/identifier_completion_didOpen.log

@@ -1,3 +1,3 @@
-Content-Length: 996
+Content-Length: 1041
 
-{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":952,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\nset_option debug.skipKernelTC true\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n  for i in [0:100000] do\n    let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n    addDecl <| Declaration.opaqueDecl {\n      name := name\n      levelParams := []\n      type := .const `Nat []\n      value := .const `Nat.zero []\n      isUnsafe := false\n      all := [name]\n    }\n    addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}}
+{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n  for i in [0:100000] do\n    let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n    let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl {\n      name := name\n      levelParams := []\n      type := .const `Nat []\n      value := .const `Nat.zero []\n      isUnsafe := false\n      all := [name]\n    }\n    setEnv env'\n    addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}}

tests/bench/identifier_completion_runner.lean

@@ -2,7 +2,7 @@ import Lean.Data.Lsp
 open IO Lean Lsp
 
 def mkCompletionRequest (id : Nat) : JsonRpc.Request Json :=
-  let param := Json.parse r#"{"textDocument":{"uri":"file:///home/mhuisi/Lean/lean4/tests/bench/identifier_completion.lean"},"position":{"line":25,"character":40},"context":{"triggerKind":1}}"#
+  let param := Json.parse r#"{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean"},"position":{"line":24,"character":40},"context":{"triggerKind":1}}"#
   let param := param.toOption.get!
   { id, method := "textDocument/completion", param }
 

tests/lean/run/printStructure.lean

@@ -59,9 +59,9 @@ constructor:
 info: class TypeName.{u} (α : Type u) : Type
 number of parameters: 1
 fields:
-  private TypeName.data✝ : (TypeNameData✝ α).type
+  private TypeName.data✝ : (TypeNameData α).type
 constructor:
-  private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α
+  private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData α).type) : TypeName α
 -/
 #guard_msgs in
 #print TypeName