bug fix

Author: durant42040

lean_dojo_v2/lean_agent/database/dynamic_database.py

@@ -482,7 +482,7 @@ def trace_repository(
         if (
             total_theorems < 3 * BATCH_SIZE
         ):  # Should be enough theorems for train/val/test
-            logger.info(f"Not enough theorems found in {url}")
+            logger.info(f"Not enough theorems found in {repo.url}")
             return None
 
         config = repo.get_config("lean-toolchain")

lean_dojo_v2/lean_dojo/data_extraction/trace.py

@@ -168,12 +168,12 @@ def _trace(repo: LeanGitRepo, build_deps: bool) -> None:
             packages_path = Path("lake-packages")
             build_path = Path("build")
 
+        shutil.copytree(
+            Path(lean_prefix), str(packages_path / "lean4"), dirs_exist_ok=True
+        )
 
+        # Modify dependency files to replace 'import all' with 'public import all'
         if build_deps:
-            shutil.copytree(
-                Path(lean_prefix), str(packages_path / "lean4"), dirs_exist_ok=True
-            )
-            # Modify dependency files to replace 'import all' with 'public import all'
             _modify_dependency_files(packages_path)
 
         # Run ExtractData.lean to extract ASTs, tactic states, and premise information.
@@ -300,4 +300,4 @@ def trace(
         dst_dir.mkdir(parents=True)
         shutil.copytree(cached_path, dst_dir / cached_path.name, dirs_exist_ok=True)
 
-    return traced_repo
+    return traced_repo