From fa17ea27159e65ee76a5e72df917e603e528b765 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 9 Aug 2025 16:48:43 -0700
Subject: [PATCH] chore: include generation in `grind.internalize` trace
 message (#9812)

---
 src/Lean/Meta/Tactic/Grind/Internalize.lean |  2 +-
 tests/lean/run/grind_implies.lean           | 60 ++++++++++-----------
 tests/lean/run/grind_pattern2.lean          | 20 +++----
 3 files changed, 41 insertions(+), 41 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 09a44aa70e..3d51d79f5c 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/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 ()
diff --git a/tests/lean/run/grind_implies.lean b/tests/lean/run/grind_implies.lean
index ca350f73f3..353dfe8015 100644
--- a/tests/lean/run/grind_implies.lean
+++ b/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
diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean
index 72eb4dbd60..0b16cab693 100644
--- a/tests/lean/run/grind_pattern2.lean
+++ b/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