From 8e6cb25cbfc38beeb60aa2dfb8c6d82376eb3f8c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Oct 2022 19:47:05 -0700 Subject: [PATCH] chore: temporarily disable eager lambda lifting We need a better heuristic for deciding which functions in instances should be eagerly lambda lifted. Otherwise, it will have to keep chasing which instances we have to annotate with `[inline]`. --- src/Lean/Compiler/LCNF/Passes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index b687124cf7..c50acf1ff5 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -50,7 +50,7 @@ def builtinPassManager : PassManager := { pullFunDecls, reduceJpArity, simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurrence := 1), - eagerLambdaLifting, + -- eagerLambdaLifting, specialize, simp (occurrence := 2), cse,