From 0e3e1353e2e62563bbd4c6ecce0c5b127873d314 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Aug 2022 14:17:54 -0700
Subject: [PATCH] feat: new `Compiler` trace classes

---
 src/Lean/Compiler/Main.lean | 12 ++++++++----
 tests/lean/run/lcnf1.lean   |  2 +-
 tests/lean/run/lcnf2.lean   |  2 +-
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean
index 984d864e65..03143bbb74 100644
--- a/src/Lean/Compiler/Main.lean
+++ b/src/Lean/Compiler/Main.lean
@@ -37,11 +37,12 @@ A checkpoint in code generation to print all declarations in between
 compiler passes in order to ease debugging.
 The trace can be viewed with `set_option trace.Compiler.step true`.
 -/
-def checkpoint (step : Name) (decls : Array Decl) (cfg : Check.Config := {}): CoreM Unit := do
-  trace[Compiler.step] "{step}"
+def checkpoint (stepName : Name) (decls : Array Decl) (cfg : Check.Config := {}): CoreM Unit := do
   for decl in decls do
     withOptions (fun opts => opts.setBool `pp.motives.pi false) do
-      trace[Compiler.step] "{decl.name} : {decl.type} :=\n{decl.value}"
+      let clsName := `Compiler ++ stepName
+      if (← Lean.isTracingEnabledFor clsName) then
+        Lean.addTrace clsName m!"{decl.name} : {decl.type} :=\n{decl.value}"
       decl.check cfg
 
 @[export lean_compile_stage1]
@@ -69,6 +70,9 @@ def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "co
 
 builtin_initialize
   registerTraceClass `Compiler
-  registerTraceClass `Compiler.step
+  registerTraceClass `Compiler.init (inherited := true)
+  registerTraceClass `Compiler.terminalCases (inherited := true)
+  registerTraceClass `Compiler.simp (inherited := true)
+  registerTraceClass `Compiler.cse (inherited := true)
 
 end Lean.Compiler
diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean
index dc87a411fe..cba6cc39d1 100644
--- a/tests/lean/run/lcnf1.lean
+++ b/tests/lean/run/lcnf1.lean
@@ -44,7 +44,7 @@ def Vec.head : Vec α (n+1) → α
 #eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
 
 set_option profiler true
-set_option trace.Compiler.step true
+set_option trace.Compiler true
 #eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
 
 def foo (a b : Nat) :=
diff --git a/tests/lean/run/lcnf2.lean b/tests/lean/run/lcnf2.lean
index e367f40b94..607af19cb2 100644
--- a/tests/lean/run/lcnf2.lean
+++ b/tests/lean/run/lcnf2.lean
@@ -20,7 +20,7 @@ def g (x : Nat) : Bool :=
   | none => true
   | some _  => false
 
-set_option trace.Compiler.step true
+set_option trace.Compiler true
 #eval Compiler.compile #[``g]