unreachableTactic linter not suppressed by `#guard_msgs`

Stream: batteries

[Kim Morrison]

Current in test/lint_unreachableTactic.lean we have:

/--
warning: this tactic is never executed
note: this linter can be disabled with `set_option linter.unreachableTactic false`
-/
#guard_msgs in
example : 1 = 1 := by
  rfl <;> simp

Here #guard_msgs is successfully checking the emitted warning, however unlike every other case, it doesn't actually suppress the warning.

This means this file is the sole "noisy" test in Batteries. Can we fix this? (I'm guessing it is a problem in unreachableTactic, rather than guard_msgs, but haven't looked.) @Mario Carneiro

[Damiano Testa]

This may not be everyone's opinion of an elegant solution, but I found that sometimes this works:

set_option linter.multiGoal false in
 #guard_msgs(drop warning) in
 set_option linter.multiGoal true in
 /--
 warning: 'rfl' leaves 1 goal 'Lean.Parser.Tactic.tacticRfl'
 note: this linter can be disabled with `set_option linter.multiGoal false`
 -/
 -- the linter allows `iterate` and `repeat'`, but continues to lint.
 #guard_msgs in
<Actual test>

[Kim Morrison]

That'll do for me, thanks! batteries#798

[Kyle Miller]

@Kim Morrison This is a known issue with #guard_msgs, that linters are run on #guard_msgs itself (linters are run twice, once on the command inside #guard_msgs, and once again on the whole #guard_msgs command). The workaround for the unused variables linter was to add #guard_msgs as an exception, but this is not general solution for all linters.

[Kyle Miller]

Damiano's idea is a good workaround.

[Kim Morrison]

I've updated the comment, thanks.

[Kyle Miller]

If there were some protocol to be able to disable these lines for #guard_msgs then this would be solved once and for all.