From a5ac950b5416dc49c2ce555f3575c0968aef9fd8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Sep 2022 16:58:45 -0700 Subject: [PATCH] chore: increase max recursion depth for compiler --- src/Lean/Compiler/LCNF/Main.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 02daee075b..2c4b02ef78 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -56,7 +56,13 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do namespace PassManager -def run (declNames : Array Name) : CompilerM (Array Decl) := do +def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDepth 8192 do + /- + Note: we need to increase the recursion depth because we currently do to save phase1 + declarations in .olean files. Then, we have to recursively compile all dependencies, + and it often creates a very deep recursion. + Moreover, some declarations get very big during simplification. + -/ let declNames ← declNames.filterM (shouldGenerateCode ·) if declNames.isEmpty then return #[] let mut decls ← declNames.mapM toDecl