add data generation examples

Author: durant42040

examples/data_generation/discover_github.py

@@ -0,0 +1,20 @@
+"""
+Example script for generating dataset from a Lean 4 GitHub repository. 
+The data is saved at <RAID_DIR>/<DATA_DIR>/<repo.name>_<repo.commit>.
+e.g. LeanDojo-v2/raid/data/lean4-example_005de00d03f1aaa32cb2923d5e3cbaf0b954a192
+
+Usage: python examples/data_generation/trace_github.py
+"""
+
+from lean_dojo_v2.database import DynamicDatabase
+
+url = "https://github.com/durant42040/lean4-example"
+commit = "005de00d03f1aaa32cb2923d5e3cbaf0b954a192"
+
+database = DynamicDatabase()
+
+database.trace_repository(
+    url=url,
+    commit=commit,
+    build_deps=False,
+)

examples/data_generation/trace_github.py

@@ -0,0 +1,21 @@
+"""
+Example script for generating dataset from a local Lean 4 repository. 
+The data is saved at <RAID_DIR>/<DATA_DIR>/<repo.name>_<repo.commit>.
+e.g. LeanDojo-v2/raid/data/lean4-example_005de00d03f1aaa32cb2923d5e3cbaf0b954a192
+
+Usage: python examples/data_generation/trace_local.py
+"""
+
+from lean_dojo_v2.database import DynamicDatabase
+
+# path = "path/to/lean4-example"
+path = "/Users/electron/Code/lean4-example"
+commit = "005de00d03f1aaa32cb2923d5e3cbaf0b954a192"
+
+database = DynamicDatabase()
+
+database.trace_repository(
+    url=path,
+    commit=commit,
+    build_deps=False,
+)

examples/data_generation/trace_local.py

@@ -5,7 +5,7 @@
 from loguru import logger
 from pantograph import Server
 
-from lean_dojo_v2.database.dynamic_database import DynamicDatabase
+from lean_dojo_v2.database import DynamicDatabase
 from lean_dojo_v2.lean_dojo.data_extraction.lean import LeanGitRepo
 from lean_dojo_v2.lean_dojo.data_extraction.trace import get_traced_repo_path
 from lean_dojo_v2.utils.constants import DATA_DIR, RAID_DIR

lean_dojo_v2/agent/base_agent.py

@@ -624,7 +624,10 @@ def exists(self) -> bool:
             repo = self.repo  # git repo
             try:
                 repo.commit(self.commit)
-                return repo.head.commit.hexsha == 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(
                     f"Commit {self.commit} does not exist in this repository."

lean_dojo_v2/lean_dojo/data_extraction/lean.py

@@ -12,7 +12,7 @@
 from transformers import AutoModelForCausalLM, AutoTokenizer
 from trl import GRPOConfig
 
-from lean_dojo_v2.database.dynamic_database import DynamicDatabase
+from lean_dojo_v2.database import DynamicDatabase
 from lean_dojo_v2.lean_dojo.data_extraction.lean import LeanGitRepo
 from lean_dojo_v2.utils import remove_marks
 from lean_dojo_v2.utils.constants import DATA_DIR, RAID_DIR

lean_dojo_v2/trainer/grpo_trainer.py

@@ -9,7 +9,7 @@
 from pytorch_lightning import seed_everything
 from tqdm import tqdm
 
-from lean_dojo_v2.database.dynamic_database import DynamicDatabase
+from lean_dojo_v2.database import DynamicDatabase
 from lean_dojo_v2.database.models.repository import Repository
 from lean_dojo_v2.lean_agent.config import TrainingConfig
 from lean_dojo_v2.lean_agent.retrieval.datamodule import RetrievalDataModule

lean_dojo_v2/trainer/retrieval_trainer.py

@@ -13,7 +13,7 @@
 from transformers import AutoModelForCausalLM, AutoTokenizer
 from trl import SFTConfig
 
-from lean_dojo_v2.database.dynamic_database import DynamicDatabase
+from lean_dojo_v2.database import DynamicDatabase
 from lean_dojo_v2.lean_dojo.data_extraction.lean import LeanGitRepo
 from lean_dojo_v2.utils import remove_marks
 from lean_dojo_v2.utils.constants import DATA_DIR, RAID_DIR