Merge pull request #226 from jsimonrichard/simon/dojo-cache-option

Add build_deps option to dojo (enables caching with Dojo)

Author: yangky11

src/lean_dojo/interaction/dojo.py

@@ -204,6 +204,7 @@ def __init__(
         entry: Union[Theorem, Tuple[LeanGitRepo, Path, int]],
         timeout: int = 600,
         additional_imports: List[str] = [],
+        build_deps: bool = True,
     ):
         """Initialize Dojo.
 
@@ -217,6 +218,7 @@ def __init__(
         self.entry = entry
         self.timeout = timeout
         self.additional_imports = additional_imports
+        self.build_deps = build_deps
 
         if self.uses_tactics:
             assert isinstance(entry, Theorem)
@@ -241,7 +243,7 @@ def __enter__(self) -> Tuple["Dojo", State]:
         logger.debug(f"Initializing Dojo for {self.entry}")
 
         # Replace the human-written proof with a `repl` tactic.
-        traced_repo_path = get_traced_repo_path(self.repo)
+        traced_repo_path = get_traced_repo_path(self.repo, self.build_deps)
         repl_path = traced_repo_path / "Lean4Repl.lean"
         assert (
             repl_path.exists()