Skip to content

Commit 80224c7

Browse files
authored
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.
1 parent 3a309ba commit 80224c7

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Lean/Compiler/LCNF/Specialize.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -238,6 +238,7 @@ def mkKey (params : Array Param) (decls : Array CodeDecl) (body : LetValue) : Co
238238
let key := ToExpr.run do
239239
ToExpr.withParams params do
240240
ToExpr.mkLambdaM params (← ToExpr.abstractM body)
241+
let key ← Meta.MetaM.run' <| Meta.transform (usedLetOnly := true) key
241242
return normLevelParams key
242243

243244
open Internalize in

0 commit comments

Comments
 (0)