says tactic does not work in v4.24.0-rc1

Stream: general

[Asei Inoue]

import Mathlib.Tactic

set_option says.verify true

variable {X Y Z : Type}

open Function

example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by
  rw [Injective]
  aesop? says
    intro a₁ a₂ a
    apply hgfinj
    simp_all only [comp_apply]

This code did work in v4.23.0, but does not work in v4.24.0-rc1.
How to fix this?

[Asei Inoue]

Error message says:

Failed to parse tactic output:

  intro a₁ a₂ a
apply hgfinj
simp_all only [comp_apply]

<input>:4:0: expected end of input

[Aaron Liu]

interesting

[Asei Inoue]

regression of says?

[Aaron Liu]

does it work with multiline suggestions from other tactics

[Kim Morrison]

I think the indenting of the try this suggestions has changed, and someone needs to update says to accommodate this?

[Asei Inoue]

I’m having trouble updating my project because of this bug.

[Kim Morrison]

#29930

[Asei Inoue]

@Kim Morrison Thank you!!!

[Asei Inoue]

I've found another says problem in v4.24.0-rc1

import Mathlib.Tactic

set_option says.verify true

example {n : Nat} : n - n + n = n := by
  /- failed to parse tactic output -/
  ring says ring_nf
  omega