Subsequent Tactics on a State Always Result in DojoTacticTimeoutError After an Initial Timeout

[Edmund-Lai]

Description
When executing a tactic on a certain state results in a DojoTacticTimeoutError, any subsequent tactic executed on the same state—regardless of whether the tactic is correct—also results in a DojoTacticTimeoutError.

A simple example to reproduce the issue is as follows:

from lean_dojo import *

repo = LeanGitRepo(
  url='https://github.com/yangky11/miniF2F-lean4',
  commit='9903cb7062a8f85acc04cc7c694a629c8f13a044',
)
theorem = Theorem(repo, "MiniF2F/Test.lean", "mathd_numbertheory_582")

with Dojo(theorem, 30) as (dojo, init_state):
  print(init_state)
  try:
    result = dojo.run_tac(init_state, "simp_all [Nat.add_mod, Nat.mul_mod, Nat.mod_mod]")
  except DojoTacticTimeoutError:
    print("Timeout")
  result = dojo.run_tac(init_state, "omega")
  print(result)

In this example, omega is a correct tactic for the given state, but it fails to execute properly.

I suspect this might be caused by Lean continuing to process the previous tactic without properly handling the new one. Could you please confirm if this is the case and whether there is a solution to address this issue? Thanks!

Platform Information

• OS: Ubuntu 20.04
• Python: 3.11.10
• elan: 3.1.1
• Lake version: 5.0.0-410fab7
• LeanDojo: 2.2.0

[yangky11]

Hi, this is expected since DojoTacticTimeoutError is not an error that you can recover from. For example, if a tactic runs forever, as far as I know, there is no way for Lean to interrupt the tactic.

[Edmund-Lai]

Thank you for your reply!