diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 0390bbcfad..0e915b5798 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase) occurrence := occurrence phase := phase name := name - run := fun xs => xs.mapM run + run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl end Pass diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index 03507d87f3..52d358f5ab 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -217,6 +217,8 @@ Simplify `code` -/ partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do incVisited + if (← get).visited % 128 == 0 then + checkSystem "LCNF simp" match code with | .let decl k => let baseDecl := decl