perf: remove unused argument to ExternEntry.opaque (#11066)

This used to create quite a few unique objects in public .olean
This commit is contained in:
Sebastian Ullrich 2025-11-03 18:26:32 +01:00 committed by GitHub
parent 00e29075f3
commit e4fb780f8a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 6 additions and 6 deletions

View file

@ -18,7 +18,7 @@ inductive ExternEntry where
| inline (backend : Name) (pattern : String)
| standard (backend : Name) (fn : String)
/-- Call to a Lean function without exported IR. -/
| opaque (fn : Name)
| opaque
deriving BEq, Hashable
/--

View file

@ -132,7 +132,7 @@ builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
if let some (.str _ s) := getExportNameFor? env f then
return .extern f xs ty { entries := [.standard `all s] }
else
return .extern f xs ty { entries := [.opaque f] }
return .extern f xs ty { entries := [.opaque] }
| d => some d
else entries
-- Written to on codegen environment branch but accessed from other elaboration branches when

View file

@ -433,7 +433,7 @@ def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
emitLhs z
let decl ← getDecl f
match decl with
| .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque _], .. }) .. =>
| .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque], .. }) .. =>
emitCName f
if ys.size > 0 then
let (ys, _) := ys.zip ps |>.filter (fun (_, p) => !p.ty.isVoid) |>.unzip

View file

@ -679,7 +679,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
| some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
| some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
| some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
| some (ExternEntry.opaque _) => unreachable!
| some ExternEntry.opaque => unreachable!
| _ => throw s!"Failed to emit extern application '{f}'."
def getFunIdTy (f : FunId) : M llvmctx (LLVM.LLVMType llvmctx) := do
@ -754,7 +754,7 @@ def emitFullApp (builder : LLVM.Builder llvmctx)
let (__zty, zslot) ← emitLhsSlot_ z
let decl ← getDecl f
match decl with
| .fdecl .. | .extern _ _ _ { entries := [.opaque _] } =>
| .fdecl .. | .extern _ _ _ { entries := [.opaque] } =>
if ys.size > 0 then
let fv ← getOrAddFunIdValue builder f
let ys ← ys.mapM (fun y => do

View file

@ -114,7 +114,7 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) : IO DeclExt
if isDeclTransparent env phase decl.name then
some decl
else
some { decl with value := .extern { entries := [.opaque decl.name] } }
some { decl with value := .extern { entries := [.opaque] } }
return entries
statsFn := fun s =>
let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1)