From d7acf1f844955f808389ef27e6e6ca0fa83dc9d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Aug 2022 16:22:09 -0700 Subject: [PATCH] feat: add `Compiler.jp` trace class --- 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 03143bbb74..bfec18c8a2 100644 --- a/src/Lean/Compiler/Main.lean +++ b/src/Lean/Compiler/Main.lean @@ -53,6 +53,7 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do checkpoint `init decls { terminalCasesOnly := false } let decls ← decls.mapM (·.terminalCases) checkpoint `terminalCases decls + decls.forM fun decl => do trace[Compiler.jp] "{decl.name}: {(← JoinPoints.JoinPointFinder.findJoinPoints decl.value |>.run' {})}" let decls ← decls.mapM (·.simp) checkpoint `simp decls -- Remark: add simplification step here, `cse` is useful after simplification @@ -74,5 +75,6 @@ builtin_initialize registerTraceClass `Compiler.terminalCases (inherited := true) registerTraceClass `Compiler.simp (inherited := true) registerTraceClass `Compiler.cse (inherited := true) + registerTraceClass `Compiler.jp end Lean.Compiler