simp doesn't fail when it does nothing

[kbuzzard]

Prerequisites

• [ x ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

simp doesn't fail when it doesn't do anything.

Steps to Reproduce

example : False := by
  simp -- ⊢ False
  sorry

Expected behavior:

In Lean 3, we'd get an error simplify tactic failed to simplify

Actual behavior:

The tactic call succeeds and does nothing; there are no errors.

Reproduces how often:

100%

Versions

Lean (version 4.0.0-nightly-2023-03-07, commit d4caf1f92248, Release)

Additional Information

This is a change from Lean 3, and right now I see no advantages; when this happens I either don't care, or I find it annoying. Of course maybe there are advantages which I'm not seeing. My gut feeling is that the user probably wants to know if a call to simp didn't actually do anything at all.

Example of when it's annoying: when trying to debug a simp call which used to work but now fails (perhaps because of a change in the simp set) one wants to start simp onlying with explicit subsets of lemmas which were being used, and get instant feedback about whether the goal is changing.

[kim-em]

Fixed in #2334 and #2336.