From 475bd65c90fcc876fb4847a21418012fe7741bc8 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 28 Jul 2025 10:36:43 -0700 Subject: [PATCH] perf: during specialization, don't abstract all local fun decls under binders (#9596) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `isUnderBinder` check is intended to avoid inlining repeated computations into specializations, but this doesn’t apply to local function decls whose bodies are already delayed. --- src/Lean/Compiler/LCNF/Closure.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean index 7d780d5afc..51bed27fba 100644 --- a/src/Lean/Compiler/LCNF/Closure.lean +++ b/src/Lean/Compiler/LCNF/Closure.lean @@ -136,7 +136,7 @@ mutual if ctx.inScope fvarId then /- We only collect the variables in the scope of the function application being specialized. -/ if let some funDecl ← findFunDecl? fvarId then - if ctx.isUnderBinder || ctx.abstract funDecl.fvarId then + if ctx.abstract funDecl.fvarId then modify fun s => { s with params := s.params.push <| { funDecl with borrow := false } } else collectFunDecl funDecl