diff --git a/src/lean_dojo/__init__.py b/src/lean_dojo/__init__.py index 5024a5d..3abdce7 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 26af478..c7fa9b5 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 b8ab0fb..09121da 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]