maxHeartbeats issue when migrating from v4.13.0 to v4.14.0

Stream: lean4

[Yicheng Qian]

I'm doing evaluation on a proof search procedure written in Lean. There are thousands of test cases, so I would like to allocate 51200 heartbeats to each test case, while effectively setting maxheartbeat to infinity outside of individual test cases. Timeout exceptions thrown by individual cases should be caught in the main loop and should not cause the test to terminate.
The following code prints Exception caught in v4.13.0 (which means that timeout exception of the individual test case is caught), while it throws error (deterministic) timeout at `isDefEq`, maximum number of heartbeats (51200) has been reached in v 4.14.0

def one_test_case (id : Nat) := do
  let mut w := #[]
  for _ in [0:100000000] do
    let b ← Lean.Meta.MetaM.run' <| Lean.Meta.isDefEq (mkApp2 (.const ``Nat.add []) (.lit (.natVal 1)) (.lit (.natVal 1))) (.lit (.natVal 2))
    w := w.push b

def all_test_cases : CoreM Unit :=
  try
    for i in [0:100] do
      withCurrHeartbeats <|
        withReader (fun ctx => {ctx with maxHeartbeats := 51200 * 1000}) <|
          one_test_case i
  catch e =>
    IO.println "Exception caught"

set_option maxHeartbeats 10000000
#eval all_test_cases

[Henrik Böving]

You need to use docs#Lean.Core.tryCatchRuntimeEx to catch heartbeat exceptions, see the issues linked in docs#Lean.Core.tryCatch as to why that is

[Yicheng Qian]

Thanks! It works now.

def one_test_case (id : Nat) := do
  let mut w := #[]
  for _ in [0:100000000] do
    let b ← Lean.Meta.MetaM.run' <| Lean.Meta.isDefEq (mkApp2 (.const ``Nat.add []) (.lit (.natVal 1)) (.lit (.natVal 1))) (.lit (.natVal 2))
    w := w.push b

def all_test_cases : CoreM Unit :=
  Lean.Core.tryCatchRuntimeEx (do
    for i in [0:100] do
      withCurrHeartbeats <|
        withReader (fun ctx => {ctx with maxHeartbeats := 51200 * 1000}) <|
          one_test_case i)
  (fun e => IO.println "Exception caught")

set_option maxHeartbeats 10000000
#eval all_test_cases

[Eric Wieser]

You're seeing the effect of lean4#5565 being fixed