diff --git a/src/lean_dojo/data_extraction/lean.py b/src/lean_dojo/data_extraction/lean.py index 3f8d87e..122cf19 100644 --- a/src/lean_dojo/data_extraction/lean.py +++ b/src/lean_dojo/data_extraction/lean.py @@ -519,7 +519,7 @@ def get_dependencies( for name, repo in self._parse_lakefile_dependencies(lakefile["content"]): if name not in deps: deps[name] = repo - for dd_name, dd_repo in repo._get_lean4_dependencies().items(): + for dd_name, dd_repo in repo.get_dependencies().items(): deps[dd_name] = dd_repo return deps