Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: improve to_additive warning message #20199

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+15 −4
Open

fix: improve to_additive warning message #20199

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion Mathlib/Tactic/ToAdditive/Frontend.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1183,9 +1183,11 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
if linter.existingAttributeWarning.get (← getOptions) then
let appliedAttrs ← getAllSimpAttrs src
if appliedAttrs.size > 0 then
let appliedAttrs := ", ".intercalate (appliedAttrs.toList.map toString)
-- Note: we're not bothering to print the correct attribute arguments.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you clarify this comment? I'm not quite sure I understand

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If someone writes @[simp↓, to_additive], then the suggestion will be @[to_additive (attr := simp)], forgetting the ↓. Since this is just a suggestion, I don't think this is a big deal.

Linter.logLintIf linter.existingAttributeWarning stx m!"\
The source declaration {src} was given the simp-attribute(s) {appliedAttrs} before \
calling @[{thisAttr}]. The preferred method is to use \
calling @[{thisAttr}]. The preferred method is to use something like \
`@[{thisAttr} (attr := {appliedAttrs})]` to apply the attribute to both \
{src} and the target declaration {tgt}."
warnAttr stx Lean.Elab.Tactic.Ext.extExtension
Expand Down
15 changes: 12 additions & 3 deletions MathlibTest/toAdditive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
import Mathlib.Algebra.Group.Defs
import Mathlib.Lean.Exception
import Mathlib.Tactic.ReduceModChar.Ext
import Qq.MetaM
open Qq Lean Meta Elab Command ToAdditive

Expand Down Expand Up @@ -109,9 +110,6 @@ lemma foo15 {α β : Type u} [my_has_pow α β] (x : α) (y : β) : foo14 x y =
@[to_additive (reorder := 1 2, 4 5) bar16]
lemma foo16 {α β : Type u} [my_has_pow α β] (x : α) (y : β) : foo14 x y = (x ^ y) ^ y := foo15 x y

initialize testExt : SimpExtension ←
registerSimpAttr `simp_test "test"

@[to_additive bar17]
def foo17 [Group α] (x : α) : α := x * 1

Expand Down Expand Up @@ -424,3 +422,14 @@ run_cmd do
unless findTranslation? (← getEnv) `localize.r == some `add_localize.r do throwError "1"
unless findTranslation? (← getEnv) `localize == some `add_localize do throwError "2"
unless findTranslation? (← getEnv) `localize.s == some `add_localize.s do throwError "3"

/--
warning: The source declaration one_eq_one was given the simp-attribute(s) reduce_mod_char, simp before calling @[to_additive]. The preferred method is to use something like `@[to_additive (attr := reduce_mod_char, simp)]` to apply the attribute to both one_eq_one and the target declaration zero_eq_zero.
note: this linter can be disabled with `set_option linter.existingAttributeWarning false`
-/
#guard_msgs in
@[simp, reduce_mod_char, to_additive]
lemma one_eq_one {α : Type*} [One α] : (1 : α) = 1 := rfl

@[to_additive (attr := reduce_mod_char, simp)]
lemma one_eq_one' {α : Type*} [One α] : (1 : α) = 1 := rfl
Loading