refactor: rename Tactic.sym.debug traceclass to avoid confusion wit…

…h the option of the same name.

We pick `Tactic.sym.info` to be consistent with the `simp_mem.info` traceclass. Also, we rename `withVerboseTraceNode` to `withInfoTraceNode` to explicitly refer to the new name, and ensure it uses the right trace class (rather than the non-existent `Tactic.sym.verbose`)

Tactics/Attr.lean

@@ -13,7 +13,7 @@ initialize
   -- enable tracing for `sym_n` tactic and related components
   registerTraceClass `Tactic.sym
   -- enable verbose tracing
-  registerTraceClass `Tactic.sym.debug
+  registerTraceClass `Tactic.sym.info
 
   -- enable tracing for heartbeat usage of `sym_n`
   registerTraceClass `Tactic.sym.heartbeats

Tactics/Sym/Common.lean

@@ -15,17 +15,19 @@ variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadLiftT IO
   [MonadRef m] [AddMessageContext m] [MonadOptions m] {ε : Type}
   [MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
 
+/-- Add a trace node with the `Tactic.sym` trace class -/
 def withTraceNode (msg : MessageData) (k : m α)
     (collapsed : Bool := true)
     (tag : String := "")
     : m α := do
   Lean.withTraceNode `Tactic.sym (fun _ => pure msg) k collapsed tag
 
-def withVerboseTraceNode (msg : MessageData) (k : m α)
+/-- Add a trace node with the `Tactic.sym.info` trace class -/
+def withInfoTraceNode (msg : MessageData) (k : m α)
     (collapsed : Bool := true)
     (tag : String := "")
     : m α := do
-  Lean.withTraceNode `Tactic.sym.verbose (fun _ => pure msg) k collapsed tag
+  Lean.withTraceNode `Tactic.sym.info (fun _ => pure msg) k collapsed tag
 
 /-- Create a trace note that folds `header` with `(NOTE: can be large)`,
 and prints `msg` under such a trace node.