chore: increase max recursion depth for compiler

This commit is contained in:
Leonardo de Moura 2022-09-20 16:58:45 -07:00
parent 990b031871
commit a5ac950b54

View file

@ -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