add example

Author: durant42040

examples/data_generation/discover_github.py

@@ -0,0 +1,16 @@
+"""
+Example script for discovering popular Lean 4 repositories on Github. 
+The repositories are saved at <RAID_DIR>/<DATA_DIR>/repo_info_compatible.json
+
+Usage: python examples/data_generation/discover_github.py
+"""
+
+from lean_dojo_v2.database import DynamicDatabase
+
+database = DynamicDatabase()
+
+database.discover_repositories(
+    num_repos=5,
+    curriculum_learning=True,
+    build_deps=False,
+)

lean_dojo_v2/database/dynamic_database.py

@@ -516,6 +516,7 @@ def discover_repositories(
         self,
         num_repos: int,
         curriculum_learning: bool,
+        build_deps: bool = True,
     ) -> List[LeanGitRepo]:
         """
         Initialize the database and discover repositories.
@@ -536,7 +537,9 @@ def discover_repositories(
 
         for repo in lean_git_repos:
             logger.info(f"Processing {repo.url}")
-            traced_repo = self.trace_repository(repo.url, repo.commit)
+            traced_repo = self.trace_repository(
+                repo.url, repo.commit, build_deps=build_deps
+            )
             if traced_repo:
                 self.add_repository(traced_repo)
                 logger.info(f"Successfully added repo {traced_repo.url}")

lean_dojo_v2/lean_dojo/data_extraction/lean.py

@@ -626,7 +626,6 @@ def exists(self) -> bool:
                 repo.commit(self.commit)
                 if repo.head.commit.hexsha != self.commit:
                     self.repo.git.checkout(self.commit)
-                    print(self.repo.working_dir, self.commit)
                 return True
             except BadName:
                 logger.warning(

lean_dojo_v2/utils/git.py

@@ -35,6 +35,8 @@ def clone_repo(repo_url: str) -> Tuple[str, str]:
     """
     repo_name = "/".join(repo_url.split("/")[-2:]).replace(".git", "")
     RAID_DIR = os.environ.get("RAID_DIR")
+    if not RAID_DIR:
+        RAID_DIR = os.path.join(os.getcwd(), "raid")
 
     logger.info(f"Cloning {repo_url}")
     logger.info(f"Repo name: {repo_name}")

lean_dojo_v2/utils/lean.py

@@ -22,13 +22,13 @@ def get_lean4_version_from_config(toolchain: str) -> str:
 
 def is_supported_version(v: str) -> bool:
     """
-    Check if ``v`` is at least `v4.3.0` and at most `v4.24.0`.
+    Check if ``v`` is at least `v4.3.0` and at most `v4.30.0`.
     Note: Lean versions are generally not backwards-compatible. Also, the Lean FRO
     keeps bumping the default versions of repos to the latest version, which is
     not necessarily the latest stable version. So, we need to be careful about
     what we choose to support.
     """
-    max_version = 24
+    max_version = 30
     min_version = 3
     if not v.startswith("v"):
         return False