bug fix

Author: durant42040

lean_dojo_v2/lean_dojo/__init__.py

@@ -1,7 +1,3 @@
-import os
-
-from loguru import logger
-
 from lean_dojo_v2.utils.constants import __version__
 
 from .data_extraction.dataset import generate_benchmark
@@ -13,17 +9,3 @@
     TracedTactic,
     TracedTheorem,
 )
-from .interaction.dojo import (
-    CommandState,
-    Dojo,
-    DojoCrashError,
-    DojoInitError,
-    DojoTacticTimeoutError,
-    LeanError,
-    ProofFinished,
-    ProofGivenUp,
-    TacticResult,
-    TacticState,
-    check_proof,
-)
-from .interaction.parse_goals import Declaration, Goal, parse_goals

lean_dojo_v2/lean_dojo/data_extraction/trace.py

@@ -10,7 +10,6 @@
 from contextlib import contextmanager
 from multiprocessing import Process
 from pathlib import Path
-from subprocess import CalledProcessError
 from time import monotonic, sleep
 from typing import Generator, List, Optional, Union