From 14c4fac2835047803790ffadd38fec82f2433f26 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Mon, 30 Dec 2024 13:03:42 +0100
Subject: [PATCH] warning when projections already exists

---
 Mathlib/Tactic/Simps/Basic.lean |  6 ++++--
 MathlibTest/Simps.lean          | 10 ++++++++++
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/Simps/Basic.lean b/Mathlib/Tactic/Simps/Basic.lean
index 9bff6a59a5119..70c206828e7ae 100644
--- a/Mathlib/Tactic/Simps/Basic.lean
+++ b/Mathlib/Tactic/Simps/Basic.lean
@@ -783,8 +783,10 @@ def getRawProjections (stx : Syntax) (str : Name) (traceIfExists : Bool := false
     -- We always print the projections when they already exists and are called by
     -- `initialize_simps_projections`.
     withOptions (· |>.updateBool `trace.simps.verbose (traceIfExists || ·)) <| do
-      trace[simps.debug]
-        projectionsInfo data.2.toList "Already found projection information for structure" str
+      trace[simps.verbose]
+        projectionsInfo data.2.toList "The projections for this structure have already been \
+        initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.\n\
+        Generated projections for" str
     return data
   trace[simps.verbose] "generating projection information for structure {str}."
   trace[simps.debug] "Applying the rules {rules}."
diff --git a/MathlibTest/Simps.lean b/MathlibTest/Simps.lean
index 2c3e0d2f69483..ca8895702a44f 100644
--- a/MathlibTest/Simps.lean
+++ b/MathlibTest/Simps.lean
@@ -41,6 +41,16 @@ def Foo2.Simps.elim (α : Type _) : Foo2 α → α × α := fun x ↦ (x.elim.1,
 
 initialize_simps_projections Foo2
 
+
+/--
+info: [simps.verbose] The projections for this structure have already been initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.
+    Generated projections for Foo2:
+    Projection elim: fun α x => (x.elim.1, x.elim.2)
+-/
+#guard_msgs in
+initialize_simps_projections Foo2
+
+
 @[simps]
 def Foo2.foo2 : Foo2 Nat := ⟨(0, 0)⟩