feat(Tactic/Translate): warn when adding a docstring to an existing declaration (leanprover-community#41883)

Author: gasparattila

Mathlib/Algebra/Free.lean

@@ -319,7 +319,7 @@ inductive AddMagma.AssocRel (α : Type u) [Add α] : α → α → Prop
   | left : ∀ w x y z, AddMagma.AssocRel α (w + (x + y + z)) (w + (x + (y + z)))
 
 /-- Associativity relations for a magma. -/
-@[to_additive AddMagma.AssocRel /-- Associativity relations for an additive magma. -/]
+@[to_additive AddMagma.AssocRel]
 inductive Magma.AssocRel (α : Type u) [Mul α] : α → α → Prop
   | intro : ∀ x y z, Magma.AssocRel α (x * y * z) (x * (y * z))
   | left : ∀ w x y z, Magma.AssocRel α (w * (x * y * z)) (w * (x * (y * z)))

Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean

@@ -94,11 +94,7 @@ class _root_.AddAction.IsMultiplyPreprimitive
 pretransitive and if, when `n ≥ 1`, for every set `s` of cardinality
 `n - 1`, the action of `fixingSubgroup M s` on the complement of `s`
 is preprimitive. -/
-@[mk_iff, to_additive existing
-/-- A group action is `n`-multiply preprimitive  if it is `n`-multiply
-pretransitive and if, when `n ≥ 1`, for every set `s` of cardinality
-`n - 1`, the action of `fixingSubgroup M s` on the complement of `s`
-is preprimitive. -/]
+@[mk_iff, to_additive existing]
 class IsMultiplyPreprimitive (M α : Type*) [Group M] [MulAction M α] (n : ℕ) where
   /-- An `n`-preprimitive action is `n`-pretransitive. -/
   isMultiplyPretransitive (M α n) : IsMultiplyPretransitive M α n

Mathlib/Tactic/Translate/Core.lean

@@ -1275,6 +1275,12 @@ partial def addTranslationAttr (t : TranslateData) (src : Name) (cfg : Config)
     -- tgt doesn't exist, so let's make it
     transformDeclRec t cfg src tgt src reorder cfg.rename
   if let some doc := cfg.doc then
+    if alreadyExists then
+      logWarningAt doc <|
+        if (← findInternalDocString? (← getEnv) tgt).isSome then
+          m!"The target declaration `{.ofConstName tgt}` already has a docstring."
+        else
+          m!"This docstring should be added directly to `{.ofConstName tgt}`."
     -- TODO: `Syntax.missing` means we do not add binders to the context,
     -- so the docstring is going to have incomplete syntax highlighting.
     addDocString tgt Syntax.missing doc |>.run'.run'

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -53,7 +53,7 @@ over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A
 
 When you extend this structure,
 make sure to extend `ContinuousMapClass` and/or `MonoidHomClass`, if needed. -/
-@[to_additive /-- The type of continuous additive monoid homomorphisms from `A` to `B`. -/]
+@[to_additive]
 structure ContinuousMonoidHom extends A →* B, C(A, B)
 
 /-- Reinterpret a `ContinuousMonoidHom` as a `MonoidHom`. -/
@@ -306,8 +306,7 @@ structure ContinuousAddEquiv [Add G] [Add H] extends G ≃+ H, G ≃ₜ H
 
 /-- The structure of two-sided continuous isomorphisms between groups.
 Note that both the map and its inverse have to be continuous. -/
-@[to_additive /-- The structure of two-sided continuous isomorphisms between additive groups.
-Note that both the map and its inverse have to be continuous. -/]
+@[to_additive]
 structure ContinuousMulEquiv [Mul G] [Mul H] extends G ≃* H, G ≃ₜ H
 
 /-- The homeomorphism induced from a two-sided continuous isomorphism of groups. -/

Mathlib/Topology/Algebra/OpenSubgroup.lean

@@ -450,6 +450,8 @@ open scoped Pointwise
 
 variable {G : Type*} [TopologicalSpace G]
 
+/-- For a set `W`, `T` is a neighborhood of `0` which is open, stable under negation and satisfies
+`T + W ⊆ W`. -/
 structure IsTopologicalAddGroup.addNegClosureNhd (T W : Set G) [AddGroup G] : Prop where
   nhds : T ∈ 𝓝 0
   neg : -T = T
@@ -458,9 +460,7 @@ structure IsTopologicalAddGroup.addNegClosureNhd (T W : Set G) [AddGroup G] : Pr
 
 /-- For a set `W`, `T` is a neighborhood of `1` which is open, stable under inverse and satisfies
 `T * W ⊆ W`. -/
-@[to_additive
-/-- For a set `W`, `T` is a neighborhood of `0` which is open, stable under negation and satisfies
-`T + W ⊆ W`. -/]
+@[to_additive]
 structure IsTopologicalGroup.mulInvClosureNhd (T W : Set G) [Group G] : Prop where
   nhds : T ∈ 𝓝 1
   inv : T⁻¹ = T

MathlibTest/Attribute/ToAdditive/Basic.lean

@@ -1023,3 +1023,52 @@ info: @add_comm_alias : ∀ {G : Type u_1} [inst : AddCommMagma G] (a b : G), a
 -/
 #guard_msgs in
 #check @add_comm_alias
+
+/-! Warning when adding docstrings to existing declarations -/
+
+namespace ExistingDeclDocstring
+
+/-- Existing docstring -/
+opaque add (G : Type*) [AddGroup G] : Prop
+
+/-- warning: The target declaration `add` already has a docstring. -/
+#guard_msgs in
+@[to_additive existing /-- New docstring -/]
+opaque mul (G : Type*) [Group G] : Prop
+
+/-- warning: The target declaration `self` already has a docstring. -/
+#guard_msgs in
+/-- Existing docstring -/
+@[to_additive self (reorder := x y) /-- New docstring -/]
+opaque self (x y : Nat) : Prop
+
+/-- Existing docstring -/
+structure addStruct (G : Type*) [AddGroup G] where
+
+/-- warning: The target declaration `addStruct` already has a docstring. -/
+#guard_msgs in
+@[to_additive /-- New docstring -/]
+structure mulStruct (G : Type*) [Group G] where
+
+-- Examples with no pre-existing docstring
+
+opaque add' (G : Type*) [AddGroup G] : Prop
+
+/-- warning: This docstring should be added directly to `add'`. -/
+#guard_msgs in
+@[to_additive existing /-- New docstring -/]
+opaque mul' (G : Type*) [Group G] : Prop
+
+/-- warning: This docstring should be added directly to `self'`. -/
+#guard_msgs in
+@[to_additive self (reorder := x y) /-- New docstring -/]
+opaque self' (x y : Nat) : Prop
+
+structure addStruct' (G : Type*) [AddGroup G] where
+
+/-- warning: This docstring should be added directly to `addStruct'`. -/
+#guard_msgs in
+@[to_additive /-- New docstring -/]
+structure mulStruct' (G : Type*) [Group G] where
+
+end ExistingDeclDocstring