Set a custom timeout for each tactic

Stream: general

[Pranav cs22b015]

I am designing a custom tactic within which I invoke existing tactics. I wish to add a timeout to these tactics individually, such that if tactic A fails or times out within, say, 100000 heartbeats, then I try tactic B. Is there a way to create such a custom tactic?

My current implementation is as shown below, but it seems to be buggy

def salImpl (maxHeartbeats : Nat := 100000) : TacticM Unit := do
  -- Helper function to run tactic with timeout
  let runWithTimeout (tac : TSyntax `tactic) : TacticM Unit := do
    withOptions (fun opts => opts.setNat `maxHeartbeats maxHeartbeats) do
      evalTactic tac

  -- Try strategy 1: dsimp + grind
  try
    runWithTimeout (← `(tactic| dsimp <;> grind))
    return ()
  catch _ =>
    -- Try strategy 2: blaster
    try
      runWithTimeout (← `(tactic| blaster))
      return ()

[Henrik Böving]

Heartbeat timeouts cannot be caught with ordinary try catch statements (on purpose). You need to wrap your computation in tryCatchRuntimeEx

[Pranav cs22b015]

Thanks, have updated the code to this

def salImpl (maxHeartbeats : Nat := 100000) : TacticM Unit := do
  -- Helper function to run tactic with timeout, fails if goals remain
  let runAndCheck (tac : TSyntax `tactic) (name : String) : TacticM Unit := do
    let savedState ← saveState
    withOptions (fun opts => opts.setNat `maxHeartbeats maxHeartbeats) do
      evalTactic tac
    let goals ← getGoals
    if goals.isEmpty then
      IO.println s!"sal: {name} succeeded"
    else
      savedState.restore
      throwError "goals remain"

  let tac1 ← `(tactic| dsimp <;> grind)
  let tac2 ← `(tactic| blaster)

  -- Try strategy 1: dsimp
  tryCatchRuntimeEx
    (runAndCheck tac1 "Strategy 1 (dsimp <;> grind)")
    fun _ =>
      -- Try strategy 2: blaster
        (runAndCheck tac2 "Strategy 2 (blaster)")

But, this is still unreliable. It sometimes fails with the (kernel) deterministic timeout error, instead of trying out the next strategy. Any suggestions/fixes?