hint only suggests the first line of a suggestion

Stream: mathlib4

[Julian Berman]

The hint tactic seems to drop all but the first line of any suggestions. A minimal reproducer is below, but really this will happen any time a tactic (e.g. simp(_all)) emits multiple lines in its suggestion:

import Lean.Meta.Tactic.TryThis
import Mathlib.Tactic.Hint

namespace Lean.Meta.Tactic.TryThis
open Lean Elab Tactic

elab "suggestion" : tactic => do
  addSuggestion (← getRef) { suggestion := "\n  trivial" }

register_hint suggestion

example : 37 = 37 := by suggestion -- works fine, inserts trivial on a new line
example : 37 = 37 := by hint -- empty replacement

end Lean.Meta.Tactic.TryThis

[Kim Morrison]

PR welcome. :-) Hopefully the problem is at the Mathlib end.

[Eric Wieser]

I have a fix for this

[Eric Wieser]

#19756, I have no idea why that code was even there

[Eric Wieser]

The right solution here would probably be to inspect the infotrees created by running the tactic, but I have no idea how to do that