From 23be59b747f6730606df3061557ba96fbc56da27 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Aug 2022 00:10:56 -0700 Subject: [PATCH] chore: add `Compiler.stat` trace option --- src/Lean/Compiler/Main.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean index bfec18c8a2..4e4afff8ce 100644 --- a/src/Lean/Compiler/Main.lean +++ b/src/Lean/Compiler/Main.lean @@ -60,6 +60,7 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do let decls ← decls.mapM (·.cse) checkpoint `cse decls saveStage1Decls decls + decls.forM fun decl => do trace[Compiler.stat] "{decl.name}: {← getLCNFSize decl.value}" return decls /-- @@ -71,6 +72,7 @@ def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "co builtin_initialize registerTraceClass `Compiler + registerTraceClass `Compiler.stat registerTraceClass `Compiler.init (inherited := true) registerTraceClass `Compiler.terminalCases (inherited := true) registerTraceClass `Compiler.simp (inherited := true)