Repr typeclass to eval custom types?

Stream: mathlib4

[Oscar Matemb ⚛️]

Hey everyone, quick question. So I’ve noticed that you now need to provide a Repr instance for the custom type in order for the result to display, even when forcing an eval. Previously, having a toString definition was enough, but now Lean complains about missing 'Lean.MetaEval' (which is implemented via Repr.
Was this change introduced recently? Is there a way to make eval use 'toString' automatically, or do we always need to provide a Repr typeclass for custom types now?

def BisectionResult.toString : BisectionResult → String
  | success root iter => s!"Root found: {root} (after {iter} iterations)"
  | invalidBounds reason => s!"Invalid bounds: {reason}"
  | maxIterationsReached approx iter => s!"Max iterations reached: best approximation {approx} (after {iter} iterations)"
  | numericalError reason => s!"Numerical error: {reason}"

-- note for zulip : recent lean; now requires repr typeclass to display eval results
-- for custom types
instance : Repr BisectionResult where
  reprPrec r _ := BisectionResult.toString r


instance : ToString BisectionResult where
  toString := BisectionResult.toString

-- Example usage and tests
def testFunction1 (x : Float) : Float := x * x - 2.0  -- Root at √2 ≈ 1.414

def testFunction2 (x : Float) : Float := x * x * x - x - 1.0  -- Root ≈ 1.324

def testFunction3 (x : Float) : Float := Float.sin x  -- Root at π ≈ 3.14159

-- Test cases
#eval! findRoot testFunction1 1.0 2.0  -- Should find √2
#eval! findRoot testFunction2 1.0 2.0  -- Should find real root of x³ - x - 1 = 0
#eval! findRoot testFunction3 3.0 4.0  -- Should find π

[Aaron Liu]

you can always #eval toString foobar instead of #eval foobar

[Kyle Miller]

It's supposed to use toString instances, though Repr is preferred. Even more preferred is ToExpr. I'd like to help, but without an #mwe I can't check.

[Oscar Matemb ⚛️]

I can't send one anymore, I have resolved the issue with termination. The question was mainly directed at understanding the timeline of when was this introduced

[Kyle Miller]

There were changes to #eval 11 months ago: #5627

What version of Lean are you using, and what version was "previously"? Lean.MetaEval has not existed since #5327, and the current version is able to use ToExpr, Repr, and ToString instances, depending on what's available, and it also tries deriving a ToExpr instance if there's no such instance.

Also, to my recollection, there never was such a change as the one you're describing, or at least #eval has been using Repr and ToString instances for over four years. I am guessing there were some subtle errors in your code preventing Lean.MetaEval from synthesizing; that's why a #mwe is essential.