update

lean-dojo · Sep 6, 2024 · c1efbf6 · c1efbf6
1 parent 6d0795a
commit c1efbf6
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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]