simp says tooling

Stream: mathlib4

[Floris van Doorn]

I just had a PR (#12556) where I needed to fix some occurrences of the simp says tactics. I do like the information in these tactics, but it would be much nicer if the current tooling for it is improved.

• There were occurrences of t1 says t2 where both t1 and t2 succeeded, but the syntax produced by t1 changed. Of course CI should flag these cases, but it would be nice if CI continues building all files despite this "error".
• When locally fixing the mismatches, I ran a tactic like simp? [hb] at hA₃ says, and this resulted in the following syntax, that doesn't parse because of the newline before hA₃ (it's not in a greater column than the previous line).

      simp? [hb]  at
          hA₃ says simp only [CharP.cast_eq_zero, zero_add, ne_eq, one_ne_zero, not_false_eq_true,
          div_self, ENNReal.coe_one, hb, ENNReal.coe_zero, one_mul, nonpos_iff_eq_zero,
          ENNReal.coe_eq_zero] at hA₃

• Of course even better would be if a bot automatically PRs a fix (if the original tactic t1 still works), but that is probably trickier.

[Mario Carneiro]

When locally fixing the mismatches, I ran a tactic like simp? [hb] at hA₃ says, and this resulted in the following syntax, that doesn't parse because of the newline before hA₃ (it's not in a greater column than the previous line).

It looks like it is on a greater column though?

[Mario Carneiro]

the double space before at looks weird though, and certainly the line break is not well placed and would be best positioned after says

[Floris van Doorn]

The says command indeed produces double spaces. And the greater column is presumably measured from the perspective of where the at is...

import Mathlib.Tactic.Common

example (x y : Nat) (h : x - x = y) : False := by
  simp? at h says  -- simp?  at h says simp only [Nat.sub_self] at h
                        -- ^^ double space
example (x y : Nat) (h : x - x = y) : False := by
  simp? [Nat.sub_self] at h says
  -- simp? [Nat.sub_self]  at h says simp only [Nat.sub_self] at h
                      -- ^^ double space

example (x y : Nat) (h : x - x = y) : False := by
  simp at
        h -- fine
  simp at
    h  -- expected '*' or checkColGt

[Mario Carneiro]

I tested your example and noticed something else funny: the first example produces two Try this suggestions, one with simp? says and the other one with only simp only .... There is only one message produced but two try this widgets and two code actions