Inconsistent behavior between `simp_all` and `simp [*]`

Stream: general

[Asei Inoue]

this simp_all throw an error: (failed with a nested error)

example (_h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp

  simp_all

And this simp [*] does not raise an error.

example (_h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp

  simp [*]

However, both simp_all and simp [*] are failing for the same reason: there is a bad simp lemma in the local context. Given that the reason for failure is the same, I think it is strange that their behavior differs in whether or not they produce an error.

[Asei Inoue]

In v4.26.0, the behaviors of the two were consistent. I believe this is a bug in v4.27.0-rc1—what do you think?

[Artie Khovanov]

simp_all is very different to simp [*] at *. It's a much more powerful tactic that does things simp does not.

[Asei Inoue]

I know that simp_all and simp [*] are different.
the problem is, it is specific to v4.27.0-rc1
why this change is made?

[Kim Morrison]

@Asei Inoue you could use the new lean-bisect to in lean#11727 to identify which PR changed the behaviour.

[Jakub Nowak]

That's probably some simp confluence bug.

/--
error: Tactic `simp` failed with a nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
example (_h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp
  simp_all