From 7bbcfdf71210da742fdbc34ad269bf80ae5b1bdd Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 17 Apr 2025 14:46:51 -0700 Subject: [PATCH] fix: modify eager lambda lifting heuristics to match the old compiler (#8007) This PR changes eager lambda lifting heuristics in the new compiler to match the old compiler, which ensures that inlining/specializing monadic code does not accidentally create mutual tail recursion that the code generator can't handle. --- src/Lean/Compiler/LCNF/LambdaLifting.lean | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/Lean/Compiler/LCNF/LambdaLifting.lean b/src/Lean/Compiler/LCNF/LambdaLifting.lean index 05878409f5..2a9a465a1d 100644 --- a/src/Lean/Compiler/LCNF/LambdaLifting.lean +++ b/src/Lean/Compiler/LCNF/LambdaLifting.lean @@ -178,16 +178,8 @@ def eagerLambdaLifting : Pass where name := `eagerLambdaLifting run := fun decls => do decls.foldlM (init := #[]) fun decls decl => do - if (← Meta.isInstance decl.name) then - /- - Recall that we lambda lift local functions in instances to control code blowup, and make sure they are cheap to inline. - It is not worth to lift tiny ones. TODO: evaluate whether we should add a compiler option to control the min size. - - Recall that when performing eager lambda lifting in instances, we progatate the `[inline]` annotations to the new auxiliary functions. - - Note: we have tried `if decl.inlineable then return decls.push decl`, but it didn't help in our preliminary experiments. - -/ - return decls ++ (← decl.lambdaLifting (liftInstParamOnly := false) (suffix := `_elam) (inheritInlineAttrs := true) (minSize := 3)) + if decl.inlineAttr || (← Meta.isInstance decl.name) then + return decls.push decl else return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (suffix := `_elam))