chore: include generation in grind.internalize trace message

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -364,7 +364,7 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
     propagateEtaStruct e generation
 where
   go : GoalM Unit := do
-    trace_goal[grind.internalize] "{e}"
+    trace_goal[grind.internalize] "[{generation}] {e}"
     match e with
     | .bvar .. => unreachable!
     | .sort .. => return ()

tests/lean/run/grind_implies.lean

@@ -2,9 +2,9 @@ set_option trace.grind.eqc true
 set_option trace.grind.internalize true
 
 /--
-trace: [grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
+trace: [grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
 [grind.eqc] (p → q) = True
 [grind.eqc] p = True
 [grind.eqc] (p → q) = q
@@ -15,9 +15,9 @@ example (p q : Prop) : (p → q) → p → q := by
   grind
 
 /--
-trace: [grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
+trace: [grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
 [grind.eqc] (p → q) = True
 [grind.eqc] q = False
 [grind.eqc] p = False
@@ -28,12 +28,12 @@ example (p q : Prop) : (p → q) → ¬q → ¬p := by
   grind
 
 /--
-trace: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
-[grind.internalize] r
+trace: [grind.internalize] [0] (p → q) = r
+[grind.internalize] [0] Prop
+[grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
+[grind.internalize] [0] r
 [grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] p = False
@@ -46,12 +46,12 @@ example (p q : Prop) : (p → q) = r → ¬p → r := by
 
 
 /--
-trace: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
-[grind.internalize] r
+trace: [grind.internalize] [0] (p → q) = r
+[grind.internalize] [0] Prop
+[grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
+[grind.internalize] [0] r
 [grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = True
@@ -63,12 +63,12 @@ example (p q : Prop) : (p → q) = r → q → r := by
   grind
 
 /--
-trace: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
-[grind.internalize] r
+trace: [grind.internalize] [0] (p → q) = r
+[grind.internalize] [0] Prop
+[grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
+[grind.internalize] [0] r
 [grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
@@ -81,12 +81,12 @@ example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by
   grind
 
 /--
-trace: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
-[grind.internalize] p
-[grind.internalize] q
-[grind.internalize] r
+trace: [grind.internalize] [0] (p → q) = r
+[grind.internalize] [0] Prop
+[grind.internalize] [0] p → q
+[grind.internalize] [0] p
+[grind.internalize] [0] q
+[grind.internalize] [0] r
 [grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False

tests/lean/run/grind_pattern2.lean

@@ -40,17 +40,17 @@ grind_pattern fooThm => foo x [a, b]
 
 
 /--
-trace: [grind.internalize] foo x y
-[grind.internalize] [a, b]
-[grind.internalize] Nat
-[grind.internalize] a
-[grind.internalize] [b]
-[grind.internalize] b
-[grind.internalize] []
+trace: [grind.internalize] [0] foo x y
+[grind.internalize] [0] [a, b]
+[grind.internalize] [0] Nat
+[grind.internalize] [0] a
+[grind.internalize] [0] [b]
+[grind.internalize] [0] b
+[grind.internalize] [0] []
 [grind.ematch] activated `fooThm`, [foo #0 `[[a, b]]]
-[grind.internalize] x
-[grind.internalize] y
-[grind.internalize] z
+[grind.internalize] [0] x
+[grind.internalize] [0] y
+[grind.internalize] [0] z
 -/
 #guard_msgs (trace) in
 set_option trace.grind.internalize true in