Merge pull request #75 from euclidgame/time_out

Fix Missing `TimeoutError` by Replacing with `DojoTacticTimeoutError`
lean-dojo · Jan 30, 2025 · fd6d99c · fd6d99c
2 parents b5c1e5b + 4f71dd1
commit fd6d99c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/prover/proof_search.py b/prover/proof_search.py
@@ -14,7 +14,6 @@
     LeanGitRepo,
     TacticState,
     LeanError,
-    TimeoutError,
     ProofFinished,
     ProofGivenUp,
     DojoInitError,
@@ -256,7 +255,7 @@ def _run_tactic(
                 result_node = ProofFinishedNode(response)
             elif type(response) in (
                 LeanError,
-                TimeoutError,
+                DojoTacticTimeoutError,
                 ProofGivenUp,
             ):
                 result_node = ErrorNode(response)
@@ -295,7 +294,7 @@ def check_invariants(self):
                 assert self.root.status == Status.PROVED
             elif type(response) in (
                 LeanError,
-                TimeoutError,
+                DojoTacticTimeoutError,
                 ProofGivenUp,
             ):
                 assert isinstance(node, ErrorNode)

diff --git a/prover/search_tree.py b/prover/search_tree.py
@@ -6,7 +6,7 @@
 from lean_dojo import (
     TacticState,
     LeanError,
-    TimeoutError,
+    DojoTacticTimeoutError,
     ProofGivenUp,
     ProofFinished,
 )
@@ -52,7 +52,7 @@ class ProofFinishedNode(Node):
 
 @dataclass
 class ErrorNode(Node):
-    inner: Union[LeanError, TimeoutError, ProofGivenUp]
+    inner: Union[LeanError, DojoTacticTimeoutError, ProofGivenUp]
     status = Status.FAILED
     distance_to_proof = math.inf
     is_terminal = True