Fix toml parsing

src/lean_dojo/data_extraction/lean.py

@@ -709,8 +709,10 @@ def _parse_deps(
                 url = url[:-4]
             if url.startswith("git@"):
                 url = "https://" + url[4:].replace(":", "/")
-
-            rev = m["rev"]  # type: ignore
+            try:
+                rev = m["rev"]  # type: ignore
+            except KeyError:
+                rev = None
             if rev is None:
                 commit = get_latest_commit(url)
             elif len(rev) == 40 and _COMMIT_REGEX.fullmatch(rev):
@@ -730,25 +732,29 @@ def _parse_lakefile_toml_dependencies(
         self, path: Union[str, Path, None]
     ) -> List[Tuple[str, "LeanGitRepo"]]:
         lakefile = (
-            self.get_config("lakefile.toml")["content"]
+            self.get_config("lakefile.toml")
             if path is None
             else (Path(path) / "lakefile.toml").open().read()
         )
-        matches = dict()
-
-        for req in _LAKEFILE_TOML_REQUIREMENT_REGEX.finditer(lakefile):
-            for line in req.group().strip().splitlines():
-                key, value = line.split("=")
-                key = key.strip()
-                value = value.strip()
-                if key == "path":
-                    raise ValueError("Local dependencies are not supported.")
-                if key == "git":
-                    matches["url"] = value
-                if key == "rev":
-                    matches["rev"] = value
-                if key == "name":
-                    matches["name"] = value
+        # Parsing worked
+        if isinstance(lakefile, dict) and "require" in lakefile:
+            matches = lakefile["require"]
+        else:
+            if "content" in lakefile:
+                lakefile = lakefile["content"]
+            matches = []
+            for req in _LAKEFILE_TOML_REQUIREMENT_REGEX.finditer(lakefile):
+                match = {}
+                for line in req.group().strip().splitlines():
+                    key, value = line.split("=")
+                    match[key.strip()] = value.strip()
+                matches.append(match)
+        for match in matches:
+            if "path" in match:
+                raise ValueError("Local dependencies are not supported.")
+            if "git" in match:
+                match["url"] = match["git"]
+                del match["git"]
 
         return self._parse_deps(matches)
 

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()