split prints unhelpful message when failing

[nomeata]

The split tactic can fail without much indication of why it’s failing. Moreover,
it insists that tracing can help, but it doesn’t necessarily, and it keeps suggesting to use the option when it is already set, which causes seriously bad vibes when the user is likely already frustrated when the tactic doesn’t work:

/--
error: tactic 'split' failed, consider using `set_option trace.split.failure true`
n : Nat
⊢ Nat.casesOn n True fun x => True
-/
#guard_msgs in
example (n : Nat) : n.casesOn True (fun _ => True) := by
  set_option trace.split.failure true in
  split

So At the least the suggestion should be turned off when the tracing option is set. And maybe there is some how-hanging fruit for making the message a bit more helpful.

Versions

Lean 4.15.0-nightly-2024-11-26

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.