Add configuration tracing

Lean/Egg/Tactic/Basic.lean

@@ -106,6 +106,7 @@ elab "egg " mod:egg_cfg_mod rws:egg_rws base:(egg_base)? guides:(egg_guides)? :
   let goal ← getMainGoal
   let mod  ← Config.Modifier.parse mod
   let cfg := (← Config.fromOptions).modify mod
+  cfg.trace `egg.config
   goal.withContext do
     let amb     ← getAmbientMVars
     let goal    ← parseGoal goal base

Lean/Egg/Tactic/Config/Modifier.lean

@@ -53,7 +53,7 @@ syntax egg_cfg_mod := (Parser.Tactic.config)?
 section Elab
 
 private unsafe def evalUnsafe (e : Expr) : TermElabM Modifier :=
-    Meta.evalExpr' (safety := .unsafe) Modifier ``Modifier e
+  Meta.evalExpr' (safety := .unsafe) Modifier ``Modifier e
 
 @[implemented_by evalUnsafe]
 private opaque eval (e : Expr) : TermElabM Modifier

Lean/Egg/Tactic/Trace.lean

@@ -4,11 +4,17 @@ open Lean Meta Elab Tactic Std Format
 
 initialize registerTraceClass `egg
 initialize registerTraceClass `egg.rewrites (inherited := true)
+initialize registerTraceClass `egg.config (inherited := true)
 initialize registerTraceClass `egg.frontend (inherited := true)
 initialize registerTraceClass `egg.reconstruction (inherited := true)
 
 namespace Egg
 
+def Config.Debug.ExitPoint.format : Config.Debug.ExitPoint → Format
+  | .none        => "None"
+  | .beforeEqSat => "Before Equality Saturation"
+  | .beforeProof => "Before Proof Reconstruction"
+
 nonrec def MVars.format (mvars : MVars) : MetaM Format := do
   let expr := format <| ← mvars.expr.toList.mapM (ppExpr <| Expr.mvar ·)
   let tc   := format <| ← mvars.tc.toList.mapM   (ppExpr <| Expr.mvar ·)
@@ -45,6 +51,29 @@ def Rewrite.Encoded.trace (rw : Rewrite.Encoded) (cls : Name) : TacticM Unit :=
     Lean.trace cls fun _ => m!"LHS: {rw.lhs}"
     Lean.trace cls fun _ => m!"RHS: {rw.rhs}"
 
+def Config.trace (cfg : Config) (cls : Name) : TacticM Unit := do
+  let toEmoji (b : Bool) := if b then "✅" else "❌"
+  withTraceNode cls (fun _ => return "Configuration") do
+    Lean.trace cls fun _ => m!"{toEmoji cfg.genTcProjRws} Generate Type Class Projection Rewrites"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.genTcSpecRws} Generate Type Class Specialization Rewrites"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.genNatLitRws} Enable Definitional Natural Number Literal Rewrites"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.genBetaRw} Enable β-Reduction"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.genEtaRw} Enable η-Reduction"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.blockInvalidMatches} Block Invalid Matches"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.shiftCapturedBVars} Correct BVar Indices"
+    Lean.trace cls fun _ => m!"{toEmoji cfg.optimizeExpl} Optimize Explanation Length"
+    withTraceNode cls (fun _ => return "Encoding") (collapsed := false) do
+      Lean.trace cls fun _ => m!"{toEmoji cfg.betaReduceRws} β-Reduce Rewrites"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.etaReduceRws} η-Reduces Rewrites"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.eraseProofs} Erase Proofs"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.eraseLambdaDomains} Erase λ's Domains"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.eraseForallDomains} Erase ∀'s Domains"
+    withTraceNode cls (fun _ => return "Debug") (collapsed := false) do
+      Lean.trace cls fun _ => m!"Exit Point: {cfg.exitPoint.format}"
+      Lean.trace cls fun _ => m!"E-Graph Visualization Export Path: {cfg.vizPath.getD "None"}"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.traceSubstitutions} Trace Substitutions"
+      Lean.trace cls fun _ => m!"{toEmoji cfg.traceBVarCorrection} Trace BVar Index Correction"
+
 def Request.trace (req : Request) : TacticM Unit := do
   withTraceNode `egg.frontend (fun _ => return "Request") do
     withTraceNode `egg.frontend (fun _ => return "Goal") (collapsed := false) do