false positive of linter.style.multiGoal

Stream: mathlib4

[Asei Inoue]

import Mathlib.Tactic

set_option linter.style.multiGoal true

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  ring_nf

  generalize n * m = x

  /-
  There are 2 unclosed goals before 'linarith' and at least one remaining goal afterwards.
  Please focus on the current goal, for instance using `·` (typed as "\.").
  note: this linter can be disabled with `set_option linter.style.multiGoal false`
  -/
  fail_if_success linarith

  omega

[Asei Inoue]

There is only one unclosed goals before linarith.

[Damiano Testa]

I'll look at this when I'm at a computer, but my initial reaction would be that the linter should ignore fail_if_success and friends.

[Damiano Testa]

Also, thanks for the report!

[Damiano Testa]

I'm also curious to understand why the linter thinks that there are two goals before linarith.

[Damiano Testa]

I think that I know what is going on: the linter is "doubling up" as the unusedTactic linter (and merging the two was on my list anyway, once they were both in mathlib).

The reason why it reports that there are 2 goals, rather than only one, is that the logic of the "metavariable-tracking" makes it look for goals before and after that are equal, assume that they were not the target of the tactic, so that there must have been another somewhere (hinging on the unusedTactic linter for taking care of "useless" tactics) and therefore report one more goal.

[Damiano Testa]

Briefly, I will silence the linter on fail_if_success and the other similar tactics, since this is what it should do anyway. If I actually merge the multi-goal and unused tactic linter, that silencing will be the same that is already in place for the unused tactic.

[Damiano Testa]

Btw, this is already enough to show the same issue:

import Mathlib.Tactic.Linter.Multigoal

example : True := by
  fail_if_success done
  exact .intro

[Damiano Testa]

#18063