From c1efbf66f64175c5a7562b7fdf8b348aa31ad084 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@meta.com>
Date: Fri, 6 Sep 2024 13:05:10 +0000
Subject: [PATCH] update

---
 src/lean_dojo/__init__.py                    |  1 -
 src/lean_dojo/data_extraction/traced_data.py | 10 +++++++---
 src/lean_dojo/interaction/dojo.py            |  8 +-------
 3 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/lean_dojo/__init__.py b/src/lean_dojo/__init__.py
index 5024a5de..3abdce71 100644
--- a/src/lean_dojo/__init__.py
+++ b/src/lean_dojo/__init__.py
@@ -16,7 +16,6 @@
     CommandState,
     TacticState,
     LeanError,
-    TimeoutError,
     TacticResult,
     DojoCrashError,
     DojoTacticTimeoutError,
diff --git a/src/lean_dojo/data_extraction/traced_data.py b/src/lean_dojo/data_extraction/traced_data.py
index 26af478e..c7fa9b50 100644
--- a/src/lean_dojo/data_extraction/traced_data.py
+++ b/src/lean_dojo/data_extraction/traced_data.py
@@ -545,9 +545,13 @@ def _from_lean4_traced_file(
         data = json.load(json_path.open())
 
         data["module_paths"] = []
-        for line in (
-            json_path.with_suffix("").with_suffix("").with_suffix(".dep_paths").open()
-        ):
+        deps_path = json_path.with_suffix("").with_suffix("").with_suffix(".dep_paths")
+        if not deps_path.exists():
+            import pdb
+
+            pdb.set_trace()
+
+        for line in deps_path.open():
             line = line.strip()
             if line == "":
                 break
diff --git a/src/lean_dojo/interaction/dojo.py b/src/lean_dojo/interaction/dojo.py
index b8ab0fb3..09121dac 100644
--- a/src/lean_dojo/interaction/dojo.py
+++ b/src/lean_dojo/interaction/dojo.py
@@ -57,20 +57,14 @@ class LeanError:
     error: str
 
 
-@dataclass(frozen=True)
-class TimeoutError:
-    error: str
-
-
 TacticResult = Union[
     TacticState,
     ProofFinished,
     LeanError,
-    TimeoutError,
     ProofGivenUp,
 ]
 
-CommandResult = Union[CommandState, LeanError, TimeoutError]
+CommandResult = Union[CommandState, LeanError]
 
 State = Union[CommandState, TacticState]