Skip to content

Commit 901340b

Browse files
scholzhannahscholzhannah
committed
feat: more informative output messages in the flexible linter (leanprover-community#39296)
The current output messages in the flexible linter are: - If the stained location is a hypothesis: `'exact h' uses 'h'!` - If the stained location is the goal: `'exact Nat.le_succ_of_le h' uses '⊢'!` I think the first is not very informative and the second is additionally confusing. So this PR changes them to read: - For a hypothesis: `'exact h' uses 'h', which was modified by the flexible tactic 'simp' on line 40!` - And for the goal: `'exact Nat.le_succ_of_le h' modifies the current goal, which was modified by the flexible tactic 'simp_all' on line 56!` I also added some more explanation to the messages in the case that all the hypotheses and the goal were stained by `simp at *`.
1 parent 0e09f45 commit 901340b

3 files changed

Lines changed: 187 additions & 42 deletions

File tree

‎Mathlib/Tactic/Linter/FlexibleLinter.lean‎

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -522,8 +522,12 @@ def flexibleLinter : Linter where run := withSetOptionIn fun _stx => do
522522
let suggestion? ← liftCoreM <| generateSimpSuggestion stainData stainStx
523523
-- Emit warning and suggestion
524524
let msg := match stainStx.getKind with
525-
| ``Lean.Parser.Tactic.simp =>
526-
m!"`{stainStr}` is a flexible tactic modifying `{d}`. \
525+
| ``Lean.Parser.Tactic.simp => match d with
526+
| .wildcard => m!"`{stainStr}` is a flexible tactic that potentially modifies all \
527+
hypotheses and the current goal with a wildcard `*`. \
528+
Try `simp?` and use the suggested `simp only [...]`. \
529+
Alternatively, use `suffices` to explicitly state the simplified form."
530+
| _ => m!"`{stainStr}` is a flexible tactic modifying `{d}`. \
527531
Try `simp?` and use the suggested `simp only [...]`. \
528532
Alternatively, use `suffices` to explicitly state the simplified form."
529533
| ``Lean.Parser.Tactic.simpAll =>
@@ -539,7 +543,18 @@ def flexibleLinter : Linter where run := withSetOptionIn fun _stx => do
539543
if let some suggStx := suggestion? then
540544
liftCoreM <| Lean.Meta.Tactic.TryThis.addSuggestion stainStx
541545
{ suggestion := .tsyntax (kind := `tactic) ⟨suggStx⟩ } (origSpan? := stainStx)
542-
logInfoAt s m!"`{s}` uses `{d}`!"
546+
let fm ← getFileMap
547+
let stainLine? := stainStx.getPos?.map (Position.line ∘ fm.toPosition)
548+
let lineStr := if let some line := stainLine? then s!" on line {line}" else ""
549+
let atomStr := match stainStx[0] with
550+
| .atom _ val => "the flexible tactic " ++ m!"`{val}`"
551+
| _ => "a flexible tactic"
552+
logInfoAt s <| match d with
553+
| .name _ => m!"`{.group s}`\nuses `{d}`, which was modified by {atomStr}{lineStr}!"
554+
| .goal =>
555+
m!"`{.group s}`\nmodifies the current goal, which was modified by {atomStr}{lineStr}!"
556+
| .wildcard => m!"`{.group s}`\nuses a rigid tactic. Previously, {atomStr}, which \
557+
potentially modified all hypotheses and the goal with a wildcard `*`, was used{lineStr}."
543558

544559
initialize addLinter flexibleLinter
545560

‎MathlibTest/Linter/Flexible/Basic.lean‎

Lines changed: 160 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,12 @@ set_option linter.unusedVariables false
1414
1515
This file contains basic tests for the flexible linter, which do not require any advanced imports.
1616
Anything which requires groups, rings or algebraic structures is considered advanced, and
17-
tests for these can be found in `MathlibTest/ImportHeavyFlexibleLinter.lean`
17+
tests for these can be found in `MathlibTest/Linter/Flexible/ImportHeavy.lean`
1818
19+
TODO: make output message appear only once for wildcard
1920
-/
2021

22+
2123
def n : Nat := 1
2224
def m : Nat := 1
2325

@@ -27,18 +29,33 @@ example : n = m := by
2729
simp [n]
2830
simp [m]
2931

32+
-- the given line number is correct
3033
/--
3134
warning: `simp at h` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
3235
3336
Note: This linter can be disabled with `set_option linter.flexible false`
3437
---
35-
info: `exact h` uses `h`!
38+
info: `exact h`
39+
uses `h`, which was modified by the flexible tactic `simp` on line 43!
3640
-/
3741
#guard_msgs in
3842
example (h : 0 + 0 = 0) : True := by
3943
simp at h
4044
try exact h
4145

46+
/--
47+
warning: `simp at h` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
48+
49+
Note: This linter can be disabled with `set_option linter.flexible false`
50+
---
51+
info: `exact h`
52+
uses `h`, which was modified by the flexible tactic `simp` on line
53+
-/
54+
#guard_msgs (substring := true) in
55+
example (h : 0 + 0 = 0) : True := by
56+
simp at h
57+
try exact h
58+
4259
/--
4360
warning: `simp_all` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
4461
@@ -47,13 +64,106 @@ Note: This linter can be disabled with `set_option linter.flexible false`
4764
info: Try this:
4865
[apply] simp_all only [Nat.add_zero]
4966
---
50-
info: `exact Nat.le_succ_of_le h` uses `⊢`!
67+
info: `exact Nat.le_succ_of_le h`
68+
modifies the current goal, which was modified by the flexible tactic `simp_all` on line
5169
-/
52-
#guard_msgs in
70+
#guard_msgs (substring := true) in
5371
example {a b : Nat} (h : a ≤ b) : a + 0 ≤ b + 1 := by
5472
simp_all
5573
exact Nat.le_succ_of_le h
5674

75+
/--
76+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
77+
78+
Note: This linter can be disabled with `set_option linter.flexible false`
79+
---
80+
info: Try this:
81+
[apply] simp only [Nat.add_zero] at *
82+
---
83+
info: `exact Nat.le_succ_of_le h`
84+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 98.
85+
---
86+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
87+
88+
Note: This linter can be disabled with `set_option linter.flexible false`
89+
---
90+
info: Try this:
91+
[apply] simp only [Nat.add_zero] at *
92+
---
93+
info: `exact Nat.le_succ_of_le h`
94+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line
95+
-/
96+
#guard_msgs (substring := true) in
97+
example {a b : Nat} (h : a ≤ b) : a + 0 ≤ b + 1 := by
98+
simp at *
99+
exact Nat.le_succ_of_le h
100+
101+
/--
102+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
103+
104+
Note: This linter can be disabled with `set_option linter.flexible false`
105+
---
106+
info: `exact h2`
107+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 118.
108+
---
109+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
110+
111+
Note: This linter can be disabled with `set_option linter.flexible false`
112+
---
113+
info: `exact h2`
114+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line
115+
-/
116+
#guard_msgs (substring := true) in
117+
example {a b : Nat} (h1 : 0 + 0 = 0) (h2 : a ≤ b) : a ≤ b := by
118+
simp at *
119+
exact h2
120+
121+
/--
122+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
123+
124+
Note: This linter can be disabled with `set_option linter.flexible false`
125+
---
126+
info: `exact h2`
127+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 138.
128+
---
129+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
130+
131+
Note: This linter can be disabled with `set_option linter.flexible false`
132+
---
133+
info: `exact h2`
134+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line
135+
-/
136+
#guard_msgs (substring := true) in
137+
example {a b : Nat} (h1 : 0 + 0 = 0) (h2 : a ≤ b) : a ≤ b := by
138+
simp at *
139+
exact h2
140+
141+
/--
142+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
143+
144+
Note: This linter can be disabled with `set_option linter.flexible false`
145+
---
146+
info: Try this:
147+
[apply] simp only [Nat.add_zero] at *
148+
---
149+
info: `exact h`
150+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 164.
151+
---
152+
warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
153+
154+
Note: This linter can be disabled with `set_option linter.flexible false`
155+
---
156+
info: Try this:
157+
[apply] simp only [Nat.add_zero] at *
158+
---
159+
info: `exact h`
160+
uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line
161+
-/
162+
#guard_msgs (substring := true) in
163+
example {a b : Nat} (h : a = b) : a + 0 = b := by
164+
simp at *
165+
exact h
166+
57167
-- `subst` does not use the goal
58168
#guard_msgs in
59169
example {a b : Nat} (h : a = b) : a + 0 = b := by
@@ -78,7 +188,8 @@ Note: This linter can be disabled with `set_option linter.flexible false`
78188
info: Try this:
79189
[apply] simp only [Nat.add_zero]
80190
---
81-
info: `assumption` uses `⊢`!
191+
info: `assumption`
192+
modifies the current goal, which was modified by the flexible tactic `simp` on line 206!
82193
---
83194
warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
84195
@@ -87,9 +198,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
87198
info: Try this:
88199
[apply] simp only [Nat.add_zero]
89200
---
90-
info: `assumption` uses `⊢`!
201+
info: `assumption`
202+
modifies the current goal, which was modified by the flexible tactic `simp` on line
91203
-/
92-
#guard_msgs in
204+
#guard_msgs (substring := true) in
93205
example {a b : Nat} (h : a = b) : a + 0 = b := by
94206
simp
95207
induction a <;> assumption
@@ -99,9 +211,10 @@ warning: `simp at h` is a flexible tactic modifying `h`. Try `simp?` and use the
99211
100212
Note: This linter can be disabled with `set_option linter.flexible false`
101213
---
102-
info: `exact h` uses `h`!
214+
info: `exact h`
215+
uses `h`, which was modified by the flexible tactic `simp` on line
103216
-/
104-
#guard_msgs in
217+
#guard_msgs (substring := true) in
105218
example (h : 0 = 0 ∨ 0 = 0) : True := by
106219
cases h <;>
107220
rename_i h <;>
@@ -117,7 +230,8 @@ Note: This linter can be disabled with `set_option linter.flexible false`
117230
info: Try this:
118231
[apply] simp only [Nat.zero_ne_one, and_self]
119232
---
120-
info: `on_goal 2 => · contradiction` uses `⊢`!
233+
info: `on_goal 2 => · contradiction`
234+
modifies the current goal, which was modified by the flexible tactic `simp` on line 248!
121235
---
122236
warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
123237
@@ -126,9 +240,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
126240
info: Try this:
127241
[apply] simp only [Nat.zero_ne_one, and_self]
128242
---
129-
info: `contradiction` uses `⊢`!
243+
info: `contradiction`
244+
modifies the current goal, which was modified by the flexible tactic `simp` on line
130245
-/
131-
#guard_msgs in
246+
#guard_msgs (substring := true) in
132247
example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
133248
cases h <;> simp
134249
on_goal 2 => · contradiction
@@ -146,7 +261,8 @@ Note: This linter can be disabled with `set_option linter.flexible false`
146261
info: Try this:
147262
[apply] simp only [Nat.zero_ne_one, and_self]
148263
---
149-
info: `contradiction` uses `⊢`!
264+
info: `contradiction`
265+
modifies the current goal, which was modified by the flexible tactic `simp` on line 279!
150266
---
151267
warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
152268
@@ -155,9 +271,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
155271
info: Try this:
156272
[apply] simp only [Nat.zero_ne_one, and_self]
157273
---
158-
info: `contradiction` uses `⊢`!
274+
info: `contradiction`
275+
modifies the current goal, which was modified by the flexible tactic `simp` on line
159276
-/
160-
#guard_msgs in
277+
#guard_msgs (substring := true) in
161278
example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
162279
cases h <;> simp
163280
· contradiction
@@ -168,15 +285,17 @@ warning: `simp at h k` is a flexible tactic modifying `k`. Try `simp?` and use t
168285
169286
Note: This linter can be disabled with `set_option linter.flexible false`
170287
---
171-
info: `rw [← Classical.not_not (a := True)] at k` uses `k`!
288+
info: `rw [← Classical.not_not (a := True)] at k`
289+
uses `k`, which was modified by the flexible tactic `simp` on line 301!
172290
---
173291
warning: `simp at h k` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
174292
175293
Note: This linter can be disabled with `set_option linter.flexible false`
176294
---
177-
info: `rw [← Classical.not_not (a := True)] at h` uses `h`!
295+
info: `rw [← Classical.not_not (a := True)] at h`
296+
uses `h`, which was modified by the flexible tactic `simp` on line
178297
-/
179-
#guard_msgs in
298+
#guard_msgs (substring := true) in
180299
-- `simp at h` stains `h` but not other locations
181300
example {h : 0 = 0} {k : 1 = 1} : True := by
182301
simp at h k;
@@ -201,9 +320,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
201320
info: Try this:
202321
[apply] simp only [Nat.add_zero]
203322
---
204-
info: `exact h.symm` uses `⊢`!
323+
info: `exact h.symm`
324+
modifies the current goal, which was modified by the flexible tactic `simp` on line
205325
-/
206-
#guard_msgs in
326+
#guard_msgs (substring := true) in
207327
-- `congr` is allowed after `simp`, but "passes along the stain".
208328
example {a b : Nat} (h : a = b) : a + b + 0 = b + a := by
209329
simp
@@ -248,9 +368,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
248368
info: Try this:
249369
[apply] simp only [Nat.zero_ne_one, and_self]
250370
---
251-
info: `contradiction` uses `⊢`!
371+
info: `contradiction`
372+
modifies the current goal, which was modified by the flexible tactic `simp` on line
252373
-/
253-
#guard_msgs in
374+
#guard_msgs (substring := true) in
254375
example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
255376
cases h <;> simp
256377
· simp_all
@@ -277,9 +398,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
277398
info: Try this:
278399
[apply] simp only [not_true_eq_false, not_false_eq_true] at h
279400
---
280-
info: `rw [← Classical.not_not (a := True)] at h` uses `h`!
401+
info: `rw [← Classical.not_not (a := True)] at h`
402+
uses `h`, which was modified by the flexible tactic `simp` on line
281403
-/
282-
#guard_msgs in
404+
#guard_msgs (substring := true) in
283405
-- `simp at h` stains `h` but not other locations
284406
example {h : 0 = 0} {k : 1 = 1} : ¬ ¬ True := by
285407
simp at h
@@ -294,15 +416,17 @@ warning: `simp at h k` is a flexible tactic modifying `k`. Try `simp?` and use t
294416
295417
Note: This linter can be disabled with `set_option linter.flexible false`
296418
---
297-
info: `rw [← Classical.not_not (a := True)] at k` uses `k`!
419+
info: `rw [← Classical.not_not (a := True)] at k`
420+
uses `k`, which was modified by the flexible tactic `simp` on line 432!
298421
---
299422
warning: `simp at h k` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
300423
301424
Note: This linter can be disabled with `set_option linter.flexible false`
302425
---
303-
info: `rw [← Classical.not_not (a := True)] at h` uses `h`!
426+
info: `rw [← Classical.not_not (a := True)] at h`
427+
uses `h`, which was modified by the flexible tactic `simp` on line
304428
-/
305-
#guard_msgs in
429+
#guard_msgs (substring := true) in
306430
-- `simp at h` stains `h` but not other locations
307431
example {h : 0 = 0} {k : 1 = 1} : True := by
308432
simp at h k
@@ -317,9 +441,10 @@ warning: `simp at h` is a flexible tactic modifying `h`. Try `simp?` and use the
317441
318442
Note: This linter can be disabled with `set_option linter.flexible false`
319443
---
320-
info: `rw [← Classical.not_not (a := True)] at h` uses `h`!
444+
info: `rw [← Classical.not_not (a := True)] at h`
445+
uses `h`, which was modified by the flexible tactic `simp` on line
321446
-/
322-
#guard_msgs in
447+
#guard_msgs (substring := true) in
323448
-- `simp at h` stains `h` but not other locations
324449
example {h : 0 = 0} : True := by
325450
simp at h
@@ -336,9 +461,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
336461
info: Try this:
337462
[apply] simp only [Nat.zero_ne_one]
338463
---
339-
info: `rwa [← Classical.not_not (a := False)]` uses `⊢`!
464+
info: `rwa [← Classical.not_not (a := False)]`
465+
modifies the current goal, which was modified by the flexible tactic `simp` on line
340466
-/
341-
#guard_msgs in
467+
#guard_msgs (substring := true) in
342468
example {h : False} : 0 = 1 := by
343469
simp
344470
rw [← Classical.not_not (a := False)] at h
@@ -353,9 +479,10 @@ Note: This linter can be disabled with `set_option linter.flexible false`
353479
info: Try this:
354480
[apply] simp only [Nat.zero_ne_one]
355481
---
356-
info: `rwa [← Classical.not_not (a := False)]` uses `⊢`!
482+
info: `rwa [← Classical.not_not (a := False)]`
483+
modifies the current goal, which was modified by the flexible tactic `simp` on line
357484
-/
358-
#guard_msgs in
485+
#guard_msgs (substring := true) in
359486
example {h : False} : 0 = 1 ∧ 0 = 1 := by
360487
constructor
361488
· simpa

0 commit comments

Comments
 (0)