rw? small regression in v4.8.0-rc1

Stream: mathlib4

[Asei Inoue]

The following code success in Lean v4.7.0 and mathlib tagged v4.7.0, but fails in Lean v4.8.0-rc1

import Mathlib.Tactic

set_option says.verify true

variable (n m : Nat)

example (h : n + m = 0) : n = 0 ↔ m = 0 := by
  rw? says
    rw [propext (eq_zero_iff_eq_zero_of_add_eq_zero h)]

[Ruben Van de Velde]

rw? was reimplemented in core, as I understand it, so no longer mathlib's fault :)

[Asei Inoue]

@Ruben Van de Velde Oh, you are right.

[Asei Inoue]

This is not so much a bug... However, it is a phenomenon that I thought developers should be aware of, so I submitted it.

[Asei Inoue]

I don't think there was a using syntax in rw?.

[Kim Morrison]

Can you open an issue?

[Asei Inoue]

I will try to find an example without mathlib dependencies before opening an issue.

[Asei Inoue]

rw? is in mathlib4 tagged v4.7.0?

[Asei Inoue]

I get an "unknown tactic" error on rw?

[Damiano Testa]

v4.7.0 is a vintage edition from the day before yesterday. :smile:

[Asei Inoue]

@Damiano Testa What do you mean? rw? is in Lean v4.7.0?

[Asei Inoue]

I submitted an issue.

https://github.com/leanprover/lean4/issues/4062

[Damiano Testa]

I was just joking about the fact that Mathlib is on v4.8.0 since yesterday. :smile:

[Asei Inoue]

@Kim Morrison issue is here https://github.com/leanprover/lean4/issues/4062

[Kim Morrison]

Please remove the says, that is obscuring the actual output.

[Asei Inoue]

@Kim Morrison done!