warning when projections already exists

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}."

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)⟩