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

…h the option of the same name. (#235)

### Description:

We rename `Tactic.sym.debug` to `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`)

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? Yes

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Co-authored-by: Shilpi Goel <[email protected]>

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.lean

@@ -15,7 +15,7 @@ open Lean
 open Lean.Meta Lean.Elab.Tactic
 
 open AxEffects SymContext
-open Sym (withTraceNode withVerboseTraceNode)
+open Sym (withTraceNode withInfoTraceNode)
 
 /-- A wrapper around `evalTactic` that traces the passed tactic script,
 executes those tactics, and then traces the new goal state -/
@@ -52,7 +52,7 @@ to add a new local hypothesis in terms of `w` and `write_mem`
 -/
 def stepiTac (stepiEq : Expr) (hStep : Name) : SymReaderM Unit := fun ctx =>
   withMainContext' <|
-  withVerboseTraceNode m!"stepiTac: {stepiEq}" (tag := "stepiTac") <| do
+  withInfoTraceNode m!"stepiTac: {stepiEq}" (tag := "stepiTac") <| do
     let pc := (Nat.toDigits 16 ctx.pc.toNat).asString
     --  ^^ The PC in hex
     let stepLemma := Name.str ctx.program s!"stepi_eq_0x{pc}"
@@ -185,7 +185,7 @@ def explodeStep (hStep : Expr) : SymM Unit :=
     eff ← eff.withField (← c.effects.getField .ERR).proof
 
     if let some hSp := c.effects.stackAlignmentProof? then
-      withVerboseTraceNode m!"discharging side conditions" <| do
+      withInfoTraceNode m!"discharging side conditions" <| do
         for subGoal in eff.sideConditions do
           trace[Tactic.sym] "attempting to discharge side-condition:\n  {subGoal}"
           let subGoal? ← do
@@ -239,7 +239,7 @@ def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
   let stateNumber ← getCurrentStateNumber
   withTraceNode m!"(sym1): simulating step {stateNumber}" (tag:="sym1") <|
   withMainContext' do
-    withVerboseTraceNode "verbose context" (tag := "infoDump") <| do
+    withInfoTraceNode "verbose context" (tag := "infoDump") <| do
       traceSymContext
       trace[Tactic.sym] "Goal state:\n {← getMainGoal}"
 
@@ -300,7 +300,7 @@ def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
 - log a warning and return `m`, if `runSteps? = some m` and `m < n`, or
 - return `n` unchanged, otherwise  -/
 def ensureAtMostRunSteps (n : Nat) : SymM Nat := do
-  withVerboseTraceNode "" (tag := "ensureAtMostRunSteps") <| do
+  withInfoTraceNode "" (tag := "ensureAtMostRunSteps") <| do
     let ctx ← getThe SymContext
     match ctx.runSteps? with
     | none => pure n
@@ -319,7 +319,7 @@ def ensureAtMostRunSteps (n : Nat) : SymM Nat := do
 and throw a user-friendly error, pointing to `#genStepEqTheorems`,
 if it does not. -/
 def assertStepTheoremsGenerated : SymM Unit :=
-  withVerboseTraceNode "" (tag := "assertStepTheoremsGenerated") <| do
+  withInfoTraceNode "" (tag := "assertStepTheoremsGenerated") <| do
     let c ← getThe SymContext
     let pc := c.pc.toHexWithoutLeadingZeroes
     if !c.programInfo.instructions.contains c.pc then

Tactics/Sym/AxEffects.lean

@@ -14,7 +14,7 @@ import Tactics.Sym.MemoryEffects
 import Std.Data.HashMap
 
 open Lean Meta
-open Sym (withTraceNode withVerboseTraceNode)
+open Sym (withTraceNode withInfoTraceNode)
 
 /-- A reflected `ArmState` field, see `AxEffects.fields` for more context -/
 structure AxEffects.FieldEffect where
@@ -431,7 +431,7 @@ private def assertIsDefEq (e expected : Expr) : MetaM Unit := do
 
 /-- Given an expression `e : ArmState`,
 which is a sequence of `w`/`write_mem`s to `eff.currentState`,
-return an `AxEffects` where `e` is the new `currentState`. 
+return an `AxEffects` where `e` is the new `currentState`.
 
 See also `updateWithExpr`, which is a wrapper around `updateWithExprAux` which adds a top-level trace node.
 -/

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.

Tactics/Sym/Context.lean

@@ -34,7 +34,7 @@ and is likely to be deprecated and removed in the near future. -/
 
 open Lean Meta Elab.Tactic
 open BitVec
-open Sym (withTraceNode withVerboseTraceNode)
+open Sym (withTraceNode withInfoTraceNode)
 
 /-- A `SymContext` collects the names of various variables/hypotheses in
 the local context required for symbolic evaluation -/
@@ -159,7 +159,7 @@ def program : Name := c.programInfo.name
 /-- Find the local declaration that corresponds to a given name,
 or throw an error if no local variable of that name exists -/
 def findFromUserName (name : Name) : MetaM LocalDecl :=
-  withVerboseTraceNode m!"[findFromUserName] {name}" <| do
+  withInfoTraceNode m!"[findFromUserName] {name}" <| do
     let some decl := (← getLCtx).findFromUserName? name
       | throwError "Unknown local variable `{name}`"
     return decl
@@ -461,7 +461,7 @@ evaluation:
   * the `currentStateNumber` is incremented
 -/
 def prepareForNextStep : SymM Unit := do
-  withVerboseTraceNode "prepareForNextStep" (tag := "prepareForNextStep") <| do
+  withInfoTraceNode "prepareForNextStep" (tag := "prepareForNextStep") <| do
     let pc ← do
       let { value, ..} ← AxEffects.getFieldM .PC
       try