From 80224c72c96f518f2f832c3678217b3a67cea3cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 22 Nov 2025 00:21:40 +0100 Subject: [PATCH] perf: improve specializer cache keys (#11310) This PR makes the specializer (correctly) share more cache keys across invocations, causing us to produce less code bloat. We observed that in functions with lots of specialization, sometimes cache keys are defeq but not BEq because one has unused let decls (introduced by specialization) that the other doesn't. This PR resolves this conflict by erasing unused let decls from specializer cache keys. --- src/Lean/Compiler/LCNF/Specialize.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index fd3b081034..a2ee730cd5 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -238,6 +238,7 @@ def mkKey (params : Array Param) (decls : Array CodeDecl) (body : LetValue) : Co let key := ToExpr.run do ToExpr.withParams params do ToExpr.mkLambdaM params (← ToExpr.abstractM body) + let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key return normLevelParams key open Internalize in