Fixed config duplication bug.

.github/workflows/github-build-actions.yaml

@@ -75,9 +75,16 @@ jobs:
       - name: List repository files (debug step)
         run: find . -type f
 
-      - name: Run tests
+      - name: Run Simple Env Test
         shell: bash
         run: |
           eval $(opam env)
           source $HOME/.elan/env
-          python src/test/simple_env_test.py
+          python src/test/simple_env_test.py
+
+      - name: Run Data Gen Test
+        shell: bash
+        run: |
+          eval $(opam env)
+          source $HOME/.elan/env
+          python src/test/simple_data_gen_test.py

README.md

@@ -193,20 +193,22 @@ action = ProofAction(
 
 ## Generating Proof Step Data:
 
+>NOTE: Make sure that you have installed the `itp-interface` package before running the following commands.
+
 1.a. You need to run the following command to generate sample proof step data for Lean 4:
 ```
-python run-itp-data-gen --config-dir src/itp_interface/main/config  --config-name simple_lean_data_gen
+run-itp-data-gen --config-dir src/itp_interface/main/configs  --config-name simple_lean_data_gen
 ```
-Check the `simple_lean_data_gen.yaml` configuration in the `src/itp_interface/main/config` directory for more details. These config files are based on the `hydra` library (see [here](https://hydra.cc/docs/intro/)).
+Check the `simple_lean_data_gen.yaml` configuration in the `src/itp_interface/main/configs` directory for more details. These config files are based on the `hydra` library (see [here](https://hydra.cc/docs/intro/)).
 
 1.b. You need to run the following command to generate sample proof step data for Coq:
 ```
-python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name simple_coq_data_gen
+run-itp-data-gen --config-dir src/itp_interface/main/configs --config-name simple_coq_data_gen
 ```
-Check the `simple_coq_data_gen.yaml` configuration in the `src/itp_interface/main/config` directory for more details about where the generated data is stored and where the different ITP (Coq and Lean) projects are located in the file system.
+Check the `simple_coq_data_gen.yaml` configuration in the `src/itp_interface/main/configs` directory for more details about where the generated data is stored and where the different ITP (Coq and Lean) projects are located in the file system.
 
 ## Important Note:
-The ITP projects must be built before running proof step data generation. Make sure that the switch is set correctly while generating data for Coq projects because the Coq projects can be using different versions of Coq. Instructions for Coq project setup are listed in `src/itp_interface/main/config/repo/coq_repos.yaml` file.
+The ITP projects must be built before running proof step data generation. Make sure that the switch is set correctly while generating data for Coq projects because the Coq projects can be using different versions of Coq. Instructions for Coq project setup are listed in `src/itp_interface/main/configs/repo/coq_repos.yaml` file.
 
 ## Our Paper:
 

pyproject.toml

@@ -5,7 +5,7 @@ requires = [
 build-backend = "hatchling.build"
 [project]
 name = "itp_interface"
-version = "1.1.1"
+version = "1.1.2"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]

src/itp_interface/main/config/benchmark/simple_benchmark_lean.yaml → src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml

@@ -6,7 +6,7 @@ few_shot_metadata_filename_for_retrieval:
 dfs_data_path_for_retrieval: 
 dfs_metadata_filename_for_retrieval: 
 datasets:
-  - project: data/test/lean4_proj
+  - project: src/data/test/lean4_proj
     files:
       - path: Lean4Proj/Basic.lean
         theorems: "*"

src/itp_interface/main/run_tool.py

@@ -420,17 +420,19 @@ def run_data_generation(experiment: Experiments, log_dir: str, logger: logging.L
             time.sleep(10)
     logger.info(f"Finished running experiment: \n{experiment.to_json(indent=4)}")
 
-@hydra.main(config_path="config", config_name="experiments", version_base="1.2")
+@hydra.main(config_path="configs", config_name="simple_lean_data_gen", version_base="1.2")
 def main(cfg):
     os.environ["PYTHONPATH"] = f"{root_dir}:{os.environ.get('PYTHONPATH', '')}"
     # RayUtils.init_ray(num_of_cpus=cfg.run_settings.pool_size, object_store_memory_in_gb=100)
     experiment = parse_config(cfg)
-    os.chdir(root_dir)
+    # os.chdir(root_dir)
     # top_level_dir = os.path.dirname(root_dir)
     # top_level_dir = os.path.dirname(top_level_dir)
     # os.chdir(top_level_dir)
     log_dir = ".log/data_generation/benchmark/{}/{}".format(experiment.benchmark.name, time.strftime("%Y%m%d-%H%M%S"))
     os.makedirs(log_dir, exist_ok=True)
+    abs_path = os.path.abspath(log_dir)
+    print(f"Log Dir: {abs_path}")
     log_path = os.path.join(log_dir, "eval.log")
     logger = setup_logger(__name__, log_path, logging.INFO, '%(asctime)s - %(name)s - %(levelname)s - %(message)s')
     logger.info(f"Pid: {os.getpid()}")