Checking proper TC failure

Stream: lean4

[Tomas Skrivan]

Is there a way to check for proper TC failure? There is #check_failure but that succeeds even on a timeout error. I'm working and debugging rather complicated set of classes and I often accidentally write an instance that causes an infinite loop and I no longer have a proper TC failure. I would love to have unit test that checks for proper failures in some basic cases.

[Tomas Skrivan]

After a long time I got back to this. Here is my attempt:

import Lean
open Lean Elab Command Term Meta

syntax (name := check_tc_failure) "#check_tc_failure" term : command

@[commandElab check_tc_failure]
def checkTCFailureImpl : CommandElab := fun stx => do
  try
    let _ ← liftTermElabM (withoutErrToSorry (elabTerm stx[1] none))
    logError "Unexpected success!"
  catch e =>
    logInfo "FAILURE"
    logInfo s!"{← e.toMessageData.toString}"

class C (n : Nat)
instance : C 0 := ⟨⟩
def funC (n : Nat) [C n] := n

-- This behaves as expected
#check_tc_failure funC 0
#check_tc_failure funC 1

class D (n : Nat)
instance {n} [D (n+1)] : D n := ⟨⟩
def funD (n : Nat) [D n] := n

-- I want this to fail as it reaches max heartbeats
#check_tc_failure (funD 0)

class E (n m : Nat)
instance [E n m] [E n (m+1)] : E (n+1) m := ⟨⟩
def funE (n m : Nat) [E n m] := n+m

-- This should fail because we are hitting maxSize
#check_tc_failure funE 7 0

-- This should succeed as we have searched through everything
set_option synthInstance.maxSize 300 in
#check_tc_failure funE 7 0

However, I still do not know how to figure out if there was a proper failure/reaching max heartbeat/reaching max size. I could check the string of the error but I do not like that.