From 6c7554ba6ff30f60e25e364eef340543d34fa253 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 10 Feb 2025 01:10:28 -0600 Subject: [PATCH 1/4] Fixed config duplication --- src/itp_interface/main/{config => configs}/__init__.py | 0 src/itp_interface/main/{config => configs}/afp_data_gen.yaml | 0 .../main/{config => configs}/benchmark/CompCert.yaml | 0 src/itp_interface/main/{config => configs}/benchmark/GeoCoq.yaml | 0 src/itp_interface/main/{config => configs}/benchmark/UniMath.yaml | 0 src/itp_interface/main/{config => configs}/benchmark/__init__.py | 0 .../main/{config => configs}/benchmark/afp_isabelle.yaml | 0 .../main/{config => configs}/benchmark/agent_proverbot_hard.yaml | 0 .../main/{config => configs}/benchmark/category-theory.yaml | 0 .../main/{config => configs}/benchmark/compcert_118_subset.yaml | 0 .../main/{config => configs}/benchmark/compcert_benchmark.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_hard.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_hard_1.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_hard_2.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_hard_3.yaml | 0 .../benchmark/compcert_benchmark_hard_7_per_cent.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_test.yaml | 0 .../{config => configs}/benchmark/compcert_benchmark_train.yaml | 0 .../benchmark/leandojo_novel_premises_test.yaml | 0 .../benchmark/leandojo_novel_premises_train.yaml | 0 .../benchmark/leandojo_novel_premises_val.yaml | 0 .../main/{config => configs}/benchmark/leandojo_random.yaml | 0 .../main/{config => configs}/benchmark/leandojo_random_test.yaml | 0 .../main/{config => configs}/benchmark/leandojo_random_train.yaml | 0 .../main/{config => configs}/benchmark/leandojo_random_val.yaml | 0 .../main/{config => configs}/benchmark/math-comp.yaml | 0 .../main/{config => configs}/benchmark/miniF2F_test.yaml | 0 .../main/{config => configs}/benchmark/miniF2F_test_aime.yaml | 0 .../main/{config => configs}/benchmark/miniF2F_test_algebra.yaml | 0 .../main/{config => configs}/benchmark/miniF2F_test_amc12.yaml | 0 .../{config => configs}/benchmark/miniF2F_test_few_shot_hard.yaml | 0 .../main/{config => configs}/benchmark/miniF2F_test_imo.yaml | 0 .../{config => configs}/benchmark/miniF2F_test_induction.yaml | 0 .../{config => configs}/benchmark/miniF2F_test_mathd_algebra.yaml | 0 .../benchmark/miniF2F_test_mathd_algebra_hard.yaml | 0 .../benchmark/miniF2F_test_mathd_numbertheory.yaml | 0 .../{config => configs}/benchmark/miniF2F_test_numbertheory.yaml | 0 .../{config => configs}/benchmark/minicompcert_benchmark_1.yaml | 0 .../main/{config => configs}/benchmark/proverbot_hard.yaml | 0 .../main/{config => configs}/benchmark/re_prover.yaml | 0 .../main/{config => configs}/benchmark/re_prover_hard.yaml | 0 .../main/{config => configs}/benchmark/re_prover_very_hard.yaml | 0 .../{config => configs}/benchmark/reprover_with_retrieval.yaml | 0 .../benchmark/reprover_with_retrieval_hard.yaml | 0 .../benchmark/reprover_with_retrieval_neg.yaml | 0 .../main/{config => configs}/benchmark/simple_benchmark_1.yaml | 0 .../main/{config => configs}/benchmark/simple_benchmark_8.yaml | 0 .../main/{config => configs}/benchmark/simple_benchmark_9.yaml | 0 .../{config => configs}/benchmark/simple_benchmark_isabelle.yaml | 0 .../main/{config => configs}/benchmark/simple_benchmark_lean.yaml | 0 .../benchmark/simple_benchmark_lean_training_data.yaml | 0 .../{config => configs}/benchmark/simple_rl_benchmark_lean.yaml | 0 .../main/{config => configs}/benchmark/stack_machine.yaml | 0 .../main/{config => configs}/benchmark/stack_machine_hard.yaml | 0 .../main/{config => configs}/category_theory_data_gen.yaml | 0 .../main/{config => configs}/category_theory_data_gen_random.yaml | 0 .../main/{config => configs}/compcert_data_gen_test.yaml | 0 .../main/{config => configs}/compcert_data_gen_train.yaml | 0 .../main/{config => configs}/env_settings/__init__.py | 0 .../main/{config => configs}/env_settings/bm25_retrieval.yaml | 0 .../{config => configs}/env_settings/bm25_retrieval_no_dfns.yaml | 0 .../env_settings/bm25_retrieval_only_local_no_dfns.yaml | 0 .../env_settings/bm25_retrieval_with_print.yaml | 0 .../env_settings/bm25_retrieval_with_print_only_local.yaml | 0 .../bm25_retrieval_with_print_only_local_no_dfns.yaml | 0 .../main/{config => configs}/env_settings/no_retrieval.yaml | 0 src/itp_interface/main/{config => configs}/experiments.yaml | 0 src/itp_interface/main/{config => configs}/geo_coq_data_gen.yaml | 0 .../main/{config => configs}/geo_coq_data_gen_random.yaml | 0 .../main/{config => configs}/leandojo_random_data_gen.yaml | 0 .../main/{config => configs}/math_comp_data_gen.yaml | 0 .../main/{config => configs}/math_comp_data_gen_random.yaml | 0 src/itp_interface/main/{config => configs}/mathlib_data_gen.yaml | 0 src/itp_interface/main/{config => configs}/repo/__init__.py | 0 src/itp_interface/main/{config => configs}/repo/coq_repos.yaml | 0 .../main/{config => configs}/run_settings/__init__.py | 0 .../run_settings/default_coq_data_generation_transforms.yaml | 0 .../run_settings/default_isabelle_data_generation_transforms.yaml | 0 .../run_settings/default_lean4_data_generation_transforms.yaml | 0 .../run_settings/default_lean_data_generation_transforms.yaml | 0 .../main/{config => configs}/simple_coq_data_gen.yaml | 0 .../main/{config => configs}/simple_coq_data_gen_random.yaml | 0 .../main/{config => configs}/simple_lean_data_gen.yaml | 0 .../main/{config => configs}/simple_rl_lean_data_gen.yaml | 0 src/itp_interface/main/{config => configs}/uni_math_data_gen.yaml | 0 85 files changed, 0 insertions(+), 0 deletions(-) rename src/itp_interface/main/{config => configs}/__init__.py (100%) rename src/itp_interface/main/{config => configs}/afp_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/CompCert.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/GeoCoq.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/UniMath.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/__init__.py (100%) rename src/itp_interface/main/{config => configs}/benchmark/afp_isabelle.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/agent_proverbot_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/category-theory.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_118_subset.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_hard_1.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_hard_2.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_hard_3.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_hard_7_per_cent.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_test.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/compcert_benchmark_train.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_novel_premises_test.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_novel_premises_train.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_novel_premises_val.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_random.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_random_test.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_random_train.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/leandojo_random_val.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/math-comp.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_aime.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_algebra.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_amc12.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_few_shot_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_imo.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_induction.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_mathd_algebra.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_mathd_algebra_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_mathd_numbertheory.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/miniF2F_test_numbertheory.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/minicompcert_benchmark_1.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/proverbot_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/re_prover.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/re_prover_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/re_prover_very_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/reprover_with_retrieval.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/reprover_with_retrieval_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/reprover_with_retrieval_neg.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_1.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_8.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_9.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_isabelle.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_lean.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_benchmark_lean_training_data.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/simple_rl_benchmark_lean.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/stack_machine.yaml (100%) rename src/itp_interface/main/{config => configs}/benchmark/stack_machine_hard.yaml (100%) rename src/itp_interface/main/{config => configs}/category_theory_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/category_theory_data_gen_random.yaml (100%) rename src/itp_interface/main/{config => configs}/compcert_data_gen_test.yaml (100%) rename src/itp_interface/main/{config => configs}/compcert_data_gen_train.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/__init__.py (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval_no_dfns.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval_only_local_no_dfns.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval_with_print.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval_with_print_only_local.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml (100%) rename src/itp_interface/main/{config => configs}/env_settings/no_retrieval.yaml (100%) rename src/itp_interface/main/{config => configs}/experiments.yaml (100%) rename src/itp_interface/main/{config => configs}/geo_coq_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/geo_coq_data_gen_random.yaml (100%) rename src/itp_interface/main/{config => configs}/leandojo_random_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/math_comp_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/math_comp_data_gen_random.yaml (100%) rename src/itp_interface/main/{config => configs}/mathlib_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/repo/__init__.py (100%) rename src/itp_interface/main/{config => configs}/repo/coq_repos.yaml (100%) rename src/itp_interface/main/{config => configs}/run_settings/__init__.py (100%) rename src/itp_interface/main/{config => configs}/run_settings/default_coq_data_generation_transforms.yaml (100%) rename src/itp_interface/main/{config => configs}/run_settings/default_isabelle_data_generation_transforms.yaml (100%) rename src/itp_interface/main/{config => configs}/run_settings/default_lean4_data_generation_transforms.yaml (100%) rename src/itp_interface/main/{config => configs}/run_settings/default_lean_data_generation_transforms.yaml (100%) rename src/itp_interface/main/{config => configs}/simple_coq_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/simple_coq_data_gen_random.yaml (100%) rename src/itp_interface/main/{config => configs}/simple_lean_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/simple_rl_lean_data_gen.yaml (100%) rename src/itp_interface/main/{config => configs}/uni_math_data_gen.yaml (100%) diff --git a/src/itp_interface/main/config/__init__.py b/src/itp_interface/main/configs/__init__.py similarity index 100% rename from src/itp_interface/main/config/__init__.py rename to src/itp_interface/main/configs/__init__.py diff --git a/src/itp_interface/main/config/afp_data_gen.yaml b/src/itp_interface/main/configs/afp_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/afp_data_gen.yaml rename to src/itp_interface/main/configs/afp_data_gen.yaml diff --git a/src/itp_interface/main/config/benchmark/CompCert.yaml b/src/itp_interface/main/configs/benchmark/CompCert.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/CompCert.yaml rename to src/itp_interface/main/configs/benchmark/CompCert.yaml diff --git a/src/itp_interface/main/config/benchmark/GeoCoq.yaml b/src/itp_interface/main/configs/benchmark/GeoCoq.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/GeoCoq.yaml rename to src/itp_interface/main/configs/benchmark/GeoCoq.yaml diff --git a/src/itp_interface/main/config/benchmark/UniMath.yaml b/src/itp_interface/main/configs/benchmark/UniMath.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/UniMath.yaml rename to src/itp_interface/main/configs/benchmark/UniMath.yaml diff --git a/src/itp_interface/main/config/benchmark/__init__.py b/src/itp_interface/main/configs/benchmark/__init__.py similarity index 100% rename from src/itp_interface/main/config/benchmark/__init__.py rename to src/itp_interface/main/configs/benchmark/__init__.py diff --git a/src/itp_interface/main/config/benchmark/afp_isabelle.yaml b/src/itp_interface/main/configs/benchmark/afp_isabelle.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/afp_isabelle.yaml rename to src/itp_interface/main/configs/benchmark/afp_isabelle.yaml diff --git a/src/itp_interface/main/config/benchmark/agent_proverbot_hard.yaml b/src/itp_interface/main/configs/benchmark/agent_proverbot_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/agent_proverbot_hard.yaml rename to src/itp_interface/main/configs/benchmark/agent_proverbot_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/category-theory.yaml b/src/itp_interface/main/configs/benchmark/category-theory.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/category-theory.yaml rename to src/itp_interface/main/configs/benchmark/category-theory.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_118_subset.yaml b/src/itp_interface/main/configs/benchmark/compcert_118_subset.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_118_subset.yaml rename to src/itp_interface/main/configs/benchmark/compcert_118_subset.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_hard.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_hard.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_hard_1.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_1.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_hard_1.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_1.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_hard_2.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_2.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_hard_2.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_2.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_hard_3.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_3.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_hard_3.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_3.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_hard_7_per_cent.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_7_per_cent.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_hard_7_per_cent.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_hard_7_per_cent.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_test.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_test.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_test.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_test.yaml diff --git a/src/itp_interface/main/config/benchmark/compcert_benchmark_train.yaml b/src/itp_interface/main/configs/benchmark/compcert_benchmark_train.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/compcert_benchmark_train.yaml rename to src/itp_interface/main/configs/benchmark/compcert_benchmark_train.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_novel_premises_test.yaml b/src/itp_interface/main/configs/benchmark/leandojo_novel_premises_test.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_novel_premises_test.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_novel_premises_test.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_novel_premises_train.yaml b/src/itp_interface/main/configs/benchmark/leandojo_novel_premises_train.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_novel_premises_train.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_novel_premises_train.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_novel_premises_val.yaml b/src/itp_interface/main/configs/benchmark/leandojo_novel_premises_val.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_novel_premises_val.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_novel_premises_val.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_random.yaml b/src/itp_interface/main/configs/benchmark/leandojo_random.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_random.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_random.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_random_test.yaml b/src/itp_interface/main/configs/benchmark/leandojo_random_test.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_random_test.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_random_test.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_random_train.yaml b/src/itp_interface/main/configs/benchmark/leandojo_random_train.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_random_train.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_random_train.yaml diff --git a/src/itp_interface/main/config/benchmark/leandojo_random_val.yaml b/src/itp_interface/main/configs/benchmark/leandojo_random_val.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/leandojo_random_val.yaml rename to src/itp_interface/main/configs/benchmark/leandojo_random_val.yaml diff --git a/src/itp_interface/main/config/benchmark/math-comp.yaml b/src/itp_interface/main/configs/benchmark/math-comp.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/math-comp.yaml rename to src/itp_interface/main/configs/benchmark/math-comp.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_aime.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_aime.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_aime.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_aime.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_algebra.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_algebra.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_algebra.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_algebra.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_amc12.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_amc12.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_amc12.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_amc12.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_few_shot_hard.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_few_shot_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_few_shot_hard.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_few_shot_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_imo.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_imo.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_imo.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_imo.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_induction.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_induction.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_induction.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_induction.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_mathd_algebra.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_mathd_algebra.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_mathd_algebra_hard.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_mathd_algebra_hard.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_algebra_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_mathd_numbertheory.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_numbertheory.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_mathd_numbertheory.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_mathd_numbertheory.yaml diff --git a/src/itp_interface/main/config/benchmark/miniF2F_test_numbertheory.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_test_numbertheory.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/miniF2F_test_numbertheory.yaml rename to src/itp_interface/main/configs/benchmark/miniF2F_test_numbertheory.yaml diff --git a/src/itp_interface/main/config/benchmark/minicompcert_benchmark_1.yaml b/src/itp_interface/main/configs/benchmark/minicompcert_benchmark_1.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/minicompcert_benchmark_1.yaml rename to src/itp_interface/main/configs/benchmark/minicompcert_benchmark_1.yaml diff --git a/src/itp_interface/main/config/benchmark/proverbot_hard.yaml b/src/itp_interface/main/configs/benchmark/proverbot_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/proverbot_hard.yaml rename to src/itp_interface/main/configs/benchmark/proverbot_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/re_prover.yaml b/src/itp_interface/main/configs/benchmark/re_prover.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/re_prover.yaml rename to src/itp_interface/main/configs/benchmark/re_prover.yaml diff --git a/src/itp_interface/main/config/benchmark/re_prover_hard.yaml b/src/itp_interface/main/configs/benchmark/re_prover_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/re_prover_hard.yaml rename to src/itp_interface/main/configs/benchmark/re_prover_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/re_prover_very_hard.yaml b/src/itp_interface/main/configs/benchmark/re_prover_very_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/re_prover_very_hard.yaml rename to src/itp_interface/main/configs/benchmark/re_prover_very_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/reprover_with_retrieval.yaml b/src/itp_interface/main/configs/benchmark/reprover_with_retrieval.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/reprover_with_retrieval.yaml rename to src/itp_interface/main/configs/benchmark/reprover_with_retrieval.yaml diff --git a/src/itp_interface/main/config/benchmark/reprover_with_retrieval_hard.yaml b/src/itp_interface/main/configs/benchmark/reprover_with_retrieval_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/reprover_with_retrieval_hard.yaml rename to src/itp_interface/main/configs/benchmark/reprover_with_retrieval_hard.yaml diff --git a/src/itp_interface/main/config/benchmark/reprover_with_retrieval_neg.yaml b/src/itp_interface/main/configs/benchmark/reprover_with_retrieval_neg.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/reprover_with_retrieval_neg.yaml rename to src/itp_interface/main/configs/benchmark/reprover_with_retrieval_neg.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_1.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_1.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_1.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_1.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_8.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_8.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_8.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_8.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_9.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_9.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_9.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_9.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_isabelle.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_isabelle.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_isabelle.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_isabelle.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_lean.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_lean.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_benchmark_lean_training_data.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_lean_training_data.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_benchmark_lean_training_data.yaml rename to src/itp_interface/main/configs/benchmark/simple_benchmark_lean_training_data.yaml diff --git a/src/itp_interface/main/config/benchmark/simple_rl_benchmark_lean.yaml b/src/itp_interface/main/configs/benchmark/simple_rl_benchmark_lean.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/simple_rl_benchmark_lean.yaml rename to src/itp_interface/main/configs/benchmark/simple_rl_benchmark_lean.yaml diff --git a/src/itp_interface/main/config/benchmark/stack_machine.yaml b/src/itp_interface/main/configs/benchmark/stack_machine.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/stack_machine.yaml rename to src/itp_interface/main/configs/benchmark/stack_machine.yaml diff --git a/src/itp_interface/main/config/benchmark/stack_machine_hard.yaml b/src/itp_interface/main/configs/benchmark/stack_machine_hard.yaml similarity index 100% rename from src/itp_interface/main/config/benchmark/stack_machine_hard.yaml rename to src/itp_interface/main/configs/benchmark/stack_machine_hard.yaml diff --git a/src/itp_interface/main/config/category_theory_data_gen.yaml b/src/itp_interface/main/configs/category_theory_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/category_theory_data_gen.yaml rename to src/itp_interface/main/configs/category_theory_data_gen.yaml diff --git a/src/itp_interface/main/config/category_theory_data_gen_random.yaml b/src/itp_interface/main/configs/category_theory_data_gen_random.yaml similarity index 100% rename from src/itp_interface/main/config/category_theory_data_gen_random.yaml rename to src/itp_interface/main/configs/category_theory_data_gen_random.yaml diff --git a/src/itp_interface/main/config/compcert_data_gen_test.yaml b/src/itp_interface/main/configs/compcert_data_gen_test.yaml similarity index 100% rename from src/itp_interface/main/config/compcert_data_gen_test.yaml rename to src/itp_interface/main/configs/compcert_data_gen_test.yaml diff --git a/src/itp_interface/main/config/compcert_data_gen_train.yaml b/src/itp_interface/main/configs/compcert_data_gen_train.yaml similarity index 100% rename from src/itp_interface/main/config/compcert_data_gen_train.yaml rename to src/itp_interface/main/configs/compcert_data_gen_train.yaml diff --git a/src/itp_interface/main/config/env_settings/__init__.py b/src/itp_interface/main/configs/env_settings/__init__.py similarity index 100% rename from src/itp_interface/main/config/env_settings/__init__.py rename to src/itp_interface/main/configs/env_settings/__init__.py diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval.yaml diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval_no_dfns.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval_no_dfns.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval_no_dfns.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval_no_dfns.yaml diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval_only_local_no_dfns.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval_only_local_no_dfns.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval_only_local_no_dfns.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval_only_local_no_dfns.yaml diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval_with_print.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval_with_print.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print.yaml diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval_with_print_only_local.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval_with_print_only_local.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local.yaml diff --git a/src/itp_interface/main/config/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml b/src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml rename to src/itp_interface/main/configs/env_settings/bm25_retrieval_with_print_only_local_no_dfns.yaml diff --git a/src/itp_interface/main/config/env_settings/no_retrieval.yaml b/src/itp_interface/main/configs/env_settings/no_retrieval.yaml similarity index 100% rename from src/itp_interface/main/config/env_settings/no_retrieval.yaml rename to src/itp_interface/main/configs/env_settings/no_retrieval.yaml diff --git a/src/itp_interface/main/config/experiments.yaml b/src/itp_interface/main/configs/experiments.yaml similarity index 100% rename from src/itp_interface/main/config/experiments.yaml rename to src/itp_interface/main/configs/experiments.yaml diff --git a/src/itp_interface/main/config/geo_coq_data_gen.yaml b/src/itp_interface/main/configs/geo_coq_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/geo_coq_data_gen.yaml rename to src/itp_interface/main/configs/geo_coq_data_gen.yaml diff --git a/src/itp_interface/main/config/geo_coq_data_gen_random.yaml b/src/itp_interface/main/configs/geo_coq_data_gen_random.yaml similarity index 100% rename from src/itp_interface/main/config/geo_coq_data_gen_random.yaml rename to src/itp_interface/main/configs/geo_coq_data_gen_random.yaml diff --git a/src/itp_interface/main/config/leandojo_random_data_gen.yaml b/src/itp_interface/main/configs/leandojo_random_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/leandojo_random_data_gen.yaml rename to src/itp_interface/main/configs/leandojo_random_data_gen.yaml diff --git a/src/itp_interface/main/config/math_comp_data_gen.yaml b/src/itp_interface/main/configs/math_comp_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/math_comp_data_gen.yaml rename to src/itp_interface/main/configs/math_comp_data_gen.yaml diff --git a/src/itp_interface/main/config/math_comp_data_gen_random.yaml b/src/itp_interface/main/configs/math_comp_data_gen_random.yaml similarity index 100% rename from src/itp_interface/main/config/math_comp_data_gen_random.yaml rename to src/itp_interface/main/configs/math_comp_data_gen_random.yaml diff --git a/src/itp_interface/main/config/mathlib_data_gen.yaml b/src/itp_interface/main/configs/mathlib_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/mathlib_data_gen.yaml rename to src/itp_interface/main/configs/mathlib_data_gen.yaml diff --git a/src/itp_interface/main/config/repo/__init__.py b/src/itp_interface/main/configs/repo/__init__.py similarity index 100% rename from src/itp_interface/main/config/repo/__init__.py rename to src/itp_interface/main/configs/repo/__init__.py diff --git a/src/itp_interface/main/config/repo/coq_repos.yaml b/src/itp_interface/main/configs/repo/coq_repos.yaml similarity index 100% rename from src/itp_interface/main/config/repo/coq_repos.yaml rename to src/itp_interface/main/configs/repo/coq_repos.yaml diff --git a/src/itp_interface/main/config/run_settings/__init__.py b/src/itp_interface/main/configs/run_settings/__init__.py similarity index 100% rename from src/itp_interface/main/config/run_settings/__init__.py rename to src/itp_interface/main/configs/run_settings/__init__.py diff --git a/src/itp_interface/main/config/run_settings/default_coq_data_generation_transforms.yaml b/src/itp_interface/main/configs/run_settings/default_coq_data_generation_transforms.yaml similarity index 100% rename from src/itp_interface/main/config/run_settings/default_coq_data_generation_transforms.yaml rename to src/itp_interface/main/configs/run_settings/default_coq_data_generation_transforms.yaml diff --git a/src/itp_interface/main/config/run_settings/default_isabelle_data_generation_transforms.yaml b/src/itp_interface/main/configs/run_settings/default_isabelle_data_generation_transforms.yaml similarity index 100% rename from src/itp_interface/main/config/run_settings/default_isabelle_data_generation_transforms.yaml rename to src/itp_interface/main/configs/run_settings/default_isabelle_data_generation_transforms.yaml diff --git a/src/itp_interface/main/config/run_settings/default_lean4_data_generation_transforms.yaml b/src/itp_interface/main/configs/run_settings/default_lean4_data_generation_transforms.yaml similarity index 100% rename from src/itp_interface/main/config/run_settings/default_lean4_data_generation_transforms.yaml rename to src/itp_interface/main/configs/run_settings/default_lean4_data_generation_transforms.yaml diff --git a/src/itp_interface/main/config/run_settings/default_lean_data_generation_transforms.yaml b/src/itp_interface/main/configs/run_settings/default_lean_data_generation_transforms.yaml similarity index 100% rename from src/itp_interface/main/config/run_settings/default_lean_data_generation_transforms.yaml rename to src/itp_interface/main/configs/run_settings/default_lean_data_generation_transforms.yaml diff --git a/src/itp_interface/main/config/simple_coq_data_gen.yaml b/src/itp_interface/main/configs/simple_coq_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/simple_coq_data_gen.yaml rename to src/itp_interface/main/configs/simple_coq_data_gen.yaml diff --git a/src/itp_interface/main/config/simple_coq_data_gen_random.yaml b/src/itp_interface/main/configs/simple_coq_data_gen_random.yaml similarity index 100% rename from src/itp_interface/main/config/simple_coq_data_gen_random.yaml rename to src/itp_interface/main/configs/simple_coq_data_gen_random.yaml diff --git a/src/itp_interface/main/config/simple_lean_data_gen.yaml b/src/itp_interface/main/configs/simple_lean_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/simple_lean_data_gen.yaml rename to src/itp_interface/main/configs/simple_lean_data_gen.yaml diff --git a/src/itp_interface/main/config/simple_rl_lean_data_gen.yaml b/src/itp_interface/main/configs/simple_rl_lean_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/simple_rl_lean_data_gen.yaml rename to src/itp_interface/main/configs/simple_rl_lean_data_gen.yaml diff --git a/src/itp_interface/main/config/uni_math_data_gen.yaml b/src/itp_interface/main/configs/uni_math_data_gen.yaml similarity index 100% rename from src/itp_interface/main/config/uni_math_data_gen.yaml rename to src/itp_interface/main/configs/uni_math_data_gen.yaml From d789010d657cad98d3e112b322eae9529a70cc1a Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 10 Feb 2025 01:11:03 -0600 Subject: [PATCH 2/4] Removed unecessary files. --- src/itp_interface/main/run_tool.py | 2 +- src/itp_interface/tools/coq_build_tool.py | 319 ------------------ src/itp_interface/tools/coq_raw_proofs.py | 193 ----------- .../tools/coq_training_data_generator.py | 5 - .../tools/run_data_generation_transforms.py | 1 - 5 files changed, 1 insertion(+), 519 deletions(-) delete mode 100644 src/itp_interface/tools/coq_build_tool.py delete mode 100644 src/itp_interface/tools/coq_raw_proofs.py diff --git a/src/itp_interface/main/run_tool.py b/src/itp_interface/main/run_tool.py index 8e71d21..269f1b9 100644 --- a/src/itp_interface/main/run_tool.py +++ b/src/itp_interface/main/run_tool.py @@ -420,7 +420,7 @@ 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="experiments", 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) diff --git a/src/itp_interface/tools/coq_build_tool.py b/src/itp_interface/tools/coq_build_tool.py deleted file mode 100644 index 46f4fa3..0000000 --- a/src/itp_interface/tools/coq_build_tool.py +++ /dev/null @@ -1,319 +0,0 @@ -#!/usr/bin/env python3 - -import sys -root_dir = f"{__file__.split('itp_interface')[0]}" -if root_dir not in sys.path: - sys.path.append(root_dir) -import os -import logging -import typing -import argparse -from dataclasses_json import dataclass_json -from dataclasses import dataclass, field -from itp_interface.tools.coq_executor import CoqExecutor -from itp_interface.tools.coq_build_spec import CoqBuildSpec -from torch.multiprocessing import Pool, set_start_method -from multiprocessing.pool import AsyncResult -from multiprocessing import Lock -global_locks: typing.Dict[str, Lock] = { - "train_lock": Lock(), # The lock has to be global because the lock needs to be shared across processes - "test_lock": Lock(), # The lock has to be global because the lock needs to be shared across processes -} -try: - set_start_method('spawn') -except RuntimeError: - pass - -@dataclass_json -@dataclass -class CoqRepoBuilder: - root: str - compilable_projects: typing.Set[str] = field(default_factory=set) - compilable_files: typing.List[str] = field(default_factory=list) - uncompilable_projects: typing.Set[str] = field(default_factory=set) - uncompilable_files: typing.List[str] = field(default_factory=list) - train_compilable_files: typing.List[str] = field(default_factory=list) - train_uncompilable_files: typing.List[str] = field(default_factory=list) - test_compilable_files: typing.List[str] = field(default_factory=list) - test_uncompilable_files: typing.List[str] = field(default_factory=list) - - def __post_init__(self): - self.logger = logging.getLogger(__name__) - self.transform = None - self.build_specs = None - self.build_disabled = False - self.projects_to_exclude = set() - self.log_error = False - - - def enable_error_loggging(self): - self.log_error = True - - def set_logger(self, logger: logging.Logger): - self.logger = logger - - def add_project_to_exclude(self, project_name: str): - self.projects_to_exclude.add(project_name) - - def set_build_spec(self, build_specs: typing.List[CoqBuildSpec]): - assert isinstance(build_specs, list), "build_specs must be a list" - assert all([isinstance(spec, CoqBuildSpec) for spec in build_specs]), "build_specs must be a list of CoqBuildSpec" - self.build_specs = build_specs - - def set_transform(self, transform: typing.Callable[[str, CoqExecutor], None]): - assert callable(transform), "transform must be a callable" - self.transform = transform - - def disable_build(self): - self.build_disabled = True - - def _compile_file(self, project_path: str, file_path: str): - global global_locks - t_compiled_files_successfully = True - if os.path.exists(file_path): - # Compile the file - try: - with CoqExecutor(project_path, file_path, suppress_error_log=self.log_error) as coq_exec: - coq_exec.run_to_finish() - self.logger.info(f"[PID: {os.getpid()}] Compiled {file_path} successfully") - except: - self.logger.warning(f"[PID: {os.getpid()}] Couldn't Compile {file_path}") - t_compiled_files_successfully = False - pass - else: - self.logger.warning(f"File {file_path} does not exist") - return t_compiled_files_successfully - - def build_from_spec(self, spec: CoqBuildSpec): - assert isinstance(spec, CoqBuildSpec), "spec must be a CoqBuildSpec" - if spec.project_name == '.': - spec.project_name = os.path.basename(os.path.normpath(self.root)) - project_path = self.root - else: - project_path = os.path.join(self.root, spec.project_name) - assert os.path.exists(project_path), f"Project {spec.project_name} does not exist (project_path: {project_path})" - if not self.build_disabled: - # Build the project - build_command = f"cd {project_path}" - if spec.switch is not None: - build_command += f" && eval \"$(opam env --set-switch --switch={spec.switch})\"" - if spec.build_command is not None: - build_command += f" && {spec.build_command}" - else: - build_command += f" && make" - self.logger.info(f"[START] Build Attempt for project {spec.project_name} with command {build_command}") - try: - error_code = os.system(build_command) - if error_code != 0: - self.uncompilable_projects.add(spec.project_name) - self.logger.warning(f"XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX>ERROR building project {spec.project_name} with command {build_command}Successfully compiled project {spec.project_name}<==============================") - except: - self.logger.error(f"XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX>FAILED to compile project {spec.project_name}Running transform over project {project}<==============================") - project_path = os.path.join(self.root, project) - # Use os.walk with sorted to ensure that the files are processed in the same order - for root, _, files in sorted(os.walk(project_path)): - for file in sorted(files): - file_path = os.path.join(root, file) - if file_path in self.compilable_files: - try: - with CoqExecutor(project_path, file_path, use_human_readable_proof_context=use_human_readable) as coq_exec: - project_id = project_path.replace('/', '.') - self.transform(project_id, coq_exec) - except: - self.logger.error(f"Got an exception while running transform over {file}") - self.logger.exception(f"Exception Log") - pass - - def run_local_transform(self, project_path: str, file_path: str, use_human_readable: bool, transform: typing.Callable[[str, CoqExecutor, typing.Callable[[], CoqExecutor]], None]): - try: - def _print_coq_callback(): - t_coq_exec = CoqExecutor(project_path, file_path, suppress_error_log=self.log_error, use_human_readable_proof_context=use_human_readable) - t_coq_exec.__enter__() - return t_coq_exec - self.logger.info(f"==============================>Running transform over file {file_path}<==============================") - with CoqExecutor(project_path, file_path, suppress_error_log=self.log_error, use_human_readable_proof_context=use_human_readable) as coq_exec: - project_id = project_path.replace('/', '.') - transform(project_id, coq_exec, _print_coq_callback) - self.logger.info(f"==============================>Successfully ran transform over file {file_path}<==============================") - except: - self.logger.warning(f"XXXXXXXXXXXXXXXXXXXXXXX>Failed in running transform over file {file_path} 0, "projects should not be empty" - assert isinstance(files, list), "files should be a list" - assert len(files) > 0, "files should not be empty" - assert len(projects) <= len(files) - - for project in sorted(projects): - self.logger.info(f"==============================>Running transform over project {project}<==============================") - project_path = os.path.join(self.root, project) - assert os.path.exists(project_path), f"project_path {project_path} does not exist" - some_files_processed = False - for file_path in sorted(files): - if file_path.startswith(project_path): - some_files_processed = True - - try: - def _print_coq_callback(): - t_coq_exec = CoqExecutor(project_path, file_path, suppress_error_log=self.log_error, use_human_readable_proof_context=use_human_readable) - t_coq_exec.__enter__() - return t_coq_exec - self.logger.info(f"==============================>Running transform over file {file_path}<==============================") - with CoqExecutor(project_path, file_path, suppress_error_log=self.log_error, use_human_readable_proof_context=use_human_readable) as coq_exec: - project_id = project_path.replace('/', '.') - transform(project_id, coq_exec, _print_coq_callback) - self.logger.info(f"==============================>Successfully ran transform over file {file_path}<==============================") - except: - self.logger.warning(f"XXXXXXXXXXXXXXXXXXXXXXX>Failed in running transform over file {file_path}No files processed for project {project}<==============================") - else: - self.logger.info(f"==============================>Finished transform over project {project}<==============================") - - def load_from_file(file_path: str): - assert os.path.exists(file_path), "file_path must be a valid path to a file" - json_text = None - with open(file_path, "r") as f: - json_text = f.read() - return CoqRepoBuilder.schema().loads(json_text) - -# nohup python3 src/tools/coq_build_tool.py --root_project data/benchmarks/CompCert --build_spec data/benchmarks/compcert_projs_splits.json --info_file data/benchmarks/compcert_projs_build.log.json --option build & -if __name__ == "__main__": - import time - os.chdir(root_dir) - current_time = time.strftime("%Y-%m-%d-%H-%M-%S", time.localtime()) - logging_dir = f".log/build_logs" - try: - os.mkdir(logging_dir) - except FileExistsError: - pass - log_file = f"{os.path.join(logging_dir, f'coq_build_tool_{current_time}.log')}" - with open(log_file, "w") as f: - f.write("") # Clear the file - logging.basicConfig(filename=log_file, filemode='w', level=logging.INFO) - logger = logging.getLogger(__name__) - parser = argparse.ArgumentParser() - parser.add_argument("--root_project", type=str, default="data/test/coq/custom_group_theory", help="The root folder of the coq project") - parser.add_argument("--build_spec", type=str, default="data/test/coq/custom_group_theory/grp_theory_splits.json", help="The file which has the build spec") - parser.add_argument("--info_file", type=str, default="data/test/coq/custom_group_theory/compilable_projects_info.log.json", help="The file which will have the info about the compilable projects") - parser.add_argument("--option", choices=["build", "load"], default="build", help="The option to run. Either build or load") - parser.add_argument("--projects_to_exclude", type=str, default=None, required=False) - parser.add_argument("--only_compile_files", type=bool, default=False, required=False) - args = parser.parse_args() - root_project = args.root_project - info_file = args.info_file - option = args.option - if option == "build": - builder = CoqRepoBuilder(root_project) - # Create build spec - with open(args.build_spec, 'r') as f: - build_specs = CoqBuildSpec.schema().loads(f.read(), many=True) - builder.set_build_spec(build_specs) - if args.projects_to_exclude is not None: - projects_to_exclude = args.projects_to_exclude.split(',') - for project in projects_to_exclude: - project = project.strip() - assert os.path.exists(os.path.join(root_project, project)), f"{project} is not a valid project" - builder.add_project_to_exclude(project) - if args.only_compile_files: - builder.disable_build() - builder.build_all() - with open(info_file, 'w') as f: - f.write(builder.serialize()) - elif option == "load": - builder = CoqRepoBuilder.load_from_file(info_file) - logger.info(builder.compilable_projects) - logger.info(builder.compilable_files) - logger.info(builder.uncompilable_projects) - logger.info(builder.uncompilable_files) - else: - raise Exception("Invalid option") \ No newline at end of file diff --git a/src/itp_interface/tools/coq_raw_proofs.py b/src/itp_interface/tools/coq_raw_proofs.py deleted file mode 100644 index b45c9c9..0000000 --- a/src/itp_interface/tools/coq_raw_proofs.py +++ /dev/null @@ -1,193 +0,0 @@ -#!/usr/bin/env python3 - -import sys - -root_dir = f"{__file__.split('itp_interface')[0]}" -if root_dir not in sys.path: - sys.path.append(root_dir) -import logging -import os -import typing -import ray -from itp_interface.tools.ray_utils import RayUtils -from itp_interface.tools.coq_parse_utils import CoqLineByLineReader -from itp_interface.tools.training_data_format import Goal, TrainingDataFormat, TrainingDataMetadataFormat -from itp_interface.tools.training_data import TrainingData -from itp_interface.tools.proof_exec_callback import ProofExecutorCallback -from itp_interface.tools.coq_build_tool import CoqRepoBuilder - -def extract_raw_proof(file_content: str, lemma_name: str) -> TrainingDataFormat: - # Find the first occurence of the lemma_name and then find the first occurence of "Qed." - # The proof is the text between the two - start_index = file_content.find(lemma_name) - assert start_index != -1, f"Lemma {lemma_name} not found in file" - end_index = file_content.find("Qed.", start_index) - assert end_index != -1, f"Lemma {lemma_name} does not have a proof" - lemma_proof = file_content[start_index:end_index + len("Qed.")] - line_reader = CoqLineByLineReader(file_content=lemma_proof) - # Just read the first line - statement = next(line_reader.instruction_step_generator()) - # Find the next occurence of '.' after the statement which is not in a comment or quotation - next_dot_index = lemma_proof.find(".", len(statement) - 1) # This may not always work but it is good enough for now - assert next_dot_index != -1, f"Lemma {lemma_name} does not have a statement" - proof = lemma_proof[next_dot_index + 1:] - goal = Goal(goal=statement) - training_data = TrainingDataFormat(start_goals=[goal], end_goals=[], proof_steps=[proof]) - return training_data - -@ray.remote -def get_proofs_in_file(coq_proof_exec_callback: ProofExecutorCallback, file_content: str, file_path: str) -> typing.List[TrainingDataFormat]: - training_data_collection : typing.List[TrainingDataFormat] = [] - failures = [] - with coq_proof_exec_callback.get_proof_executor() as main_executor: - while not main_executor.execution_complete: - assert not main_executor.is_in_proof_mode(), "main_executor must not be in proof mode" - _ = list(main_executor.run_till_next_lemma_return_exec_stmt()) - if main_executor.execution_complete: - break - lemma_name = main_executor.get_lemma_name_if_running() - if lemma_name is None: - _ = list(main_executor.run_to_finish_lemma_return_exec()) - - if main_executor.execution_complete: - break - else: - try: - tdf = extract_raw_proof(file_content, lemma_name) - training_data_collection.append(tdf) - main_executor.run_to_finish_lemma() - except Exception: - print(f"Failed to extract proof for lemma {lemma_name} in {file_path}") - _ = list(main_executor.run_to_finish_lemma_return_exec()) - failures.append(lemma_name) - continue - return file_path, training_data_collection, failures - -def dump_raw_proofs(repo_builder: CoqRepoBuilder, output_dir: str, logger: logging.Logger): - assert os.path.exists(output_dir), f"output_dir {output_dir} does not exist" - RayUtils.init_ray(num_of_cpus=20, object_store_memory_in_gb=100, memory_in_gb=1) - projects = repo_builder.compilable_projects - - def _log_proof_cnt(file_type: str, proof_cnt_in_file: int, file_path: str, failures: typing.List[str]): - logger.info(f"==============================>[{file_type}] Added proofs {proof_cnt_in_file} in {file_path} <==============================") - if len(failures) > 0: - logger.info(f"==============================>[{file_type}] Failed to extract proofs for {len(failures)} lemmas in {file_path} <==============================") - for lemma_name in failures: - logger.info(f"==============================>[{file_type}] Failed to extract proof for lemma {lemma_name} in {file_path} <==============================") - - def _get_next_files_callback(files): - _idx = 0 - sorted_files = sorted(files) - def _get_files(cnt: int): - nonlocal _idx - file_input = [] - for file_path in sorted_files[_idx:_idx + cnt]: - if file_path.startswith(project_path): - with open(file_path, 'r') as fd: - file_content = fd.read() - coq_proof_exec_callback = ProofExecutorCallback( - project_folder=project_path, - file_path=file_path, - use_hammer=False, - timeout_in_secs=60, - use_human_readable_proof_context=True, - suppress_error_log=True, - logger=logger) - file_input.append((coq_proof_exec_callback, file_content, file_path)) - _idx += cnt - return file_input - return _get_files - - def _get_file_op_remotes_callback(file_inputs): - return [get_proofs_in_file.remote(coq_proof_exec_callback, file_content, file_path) for coq_proof_exec_callback, file_content, file_path in file_inputs] - - def _transform_outputs_callback(training_data: TrainingData, file_type: str): - def _transform_outputs(results: typing.List[typing.List[TrainingDataFormat]]): - for file_path, training_data_collection, failures in results: - for tdf in training_data_collection: - training_data.merge(tdf) - _log_proof_cnt(file_type, len(training_data_collection), file_path, failures) - return _transform_outputs - - for project in sorted(projects): - project_proof_cnt = 0 - # Create temporary directory for each project - logger.info(f"==============================> Discovering files in project {project}<==============================") - project_path = os.path.join(repo_builder.root, project) - assert os.path.exists(project_path), f"project_path {project_path} does not exist" - files_type_map = { - "train": repo_builder.train_compilable_files, - "test": repo_builder.test_compilable_files, - } - for file_type, files in files_type_map.items(): - output_path = os.path.join(output_dir, project, file_type) - os.makedirs(output_path, exist_ok=True) - training_metadata = TrainingDataMetadataFormat(training_data_buffer_size=2500, data_filename_prefix="single_data_", lemma_ref_filename_prefix="single_lemma_ref_") - training_data = TrainingData(output_path, "single.meta.json", training_metadata) - RayUtils.ray_run_within_parallel_limits( - 10, - len(files), - _transform_outputs_callback(training_data, file_type), - _get_next_files_callback(files), - _get_file_op_remotes_callback, - logger=logger, - turn_off_logging=True) - logger.info(f"[{file_type}] Saving training data to {output_path}") - save_folder = training_data.save() - logger.info(f"[{file_type}] Saved training data to {save_folder}") - project_proof_cnt += len(training_data) - logger.info(f"==============================>[{file_type}] Added all {len(training_data)} proofs in project {project}<==============================") - logger.info(f"==============================> Added {project_proof_cnt} proofs in project {project}<==============================") - logger.info(f"==============================> Added proofs in all projects<==============================") - -def count_proofs(repo_builder: CoqRepoBuilder, logger: logging.Logger): - proof_cnt = 0 - projects = repo_builder.compilable_projects - for project in sorted(projects): - project_proof_cnt = 0 - # Create temporary directory for each project - logger.info(f"==============================> Discovering files in project {project}<==============================") - project_path = os.path.join(repo_builder.root, project) - assert os.path.exists(project_path), f"project_path {project_path} does not exist" - files_type_map = { - "train": repo_builder.train_compilable_files, - "test": repo_builder.test_compilable_files, - } - for file_type, files in files_type_map.items(): - file_type_cnt = 0 - for file_path in sorted(files): - current_proof_cnt = 0 - if file_path.startswith(project_path): - with open(file_path, 'r') as fd: - file_content = fd.read() - current_proof_cnt = file_content.count("Qed.") - logger.info(f"==============================>[{file_type}] Found {current_proof_cnt} proofs in file {file_path}<==============================") - proof_cnt += current_proof_cnt - file_type_cnt += current_proof_cnt - project_proof_cnt += current_proof_cnt - logger.info(f"==============================>[{file_type}] Found {file_type_cnt} proofs in project {project}<==============================") - logger.info(f"==============================> Found {project_proof_cnt} proofs in project {project}<==============================") - logger.info(f"==============================> Found {proof_cnt} proofs in all projects<==============================") - -if __name__ == "__main__": - import time - import argparse - os.chdir(root_dir) - current_time = time.strftime("%Y-%m-%d-%H-%M-%S", time.localtime()) - logging_dir = f".log/tools/coq_raw_proofs/{current_time}" - os.makedirs(logging_dir, exist_ok=True) - log_file = f"{os.path.join(logging_dir, f'coq_raw_proofs.log')}" - logging.basicConfig(filename=log_file, filemode='w', level=logging.INFO, format='%(asctime)s - %(name)s - %(levelname)s - %(message)s') - logger = logging.getLogger("ProofCounter") - logger.info(f"Process ID: {os.getpid()}") - repo_builder = CoqRepoBuilder(root_dir) - parser = argparse.ArgumentParser() - parser.add_argument("--info_file", type=str, default="data/test/coq/custom_group_theory/compilable_projects_info.log.json", help="The file which will have the info about the compilable projects") - parser.add_argument("--output_dir", type=str, default=".log/tools/coq_raw_proofs/data/test/coq/custom_group_theory", help="The directory where the raw proofs will be dumped") - args = parser.parse_args() - info_file = args.info_file - repo_builder : CoqRepoBuilder = CoqRepoBuilder.load_from_file(info_file) - output_dir = os.path.join(args.output_dir, current_time) - os.makedirs(output_dir, exist_ok=True) - # count_proofs(repo_builder, logger) - dump_raw_proofs(repo_builder, output_dir, logger) diff --git a/src/itp_interface/tools/coq_training_data_generator.py b/src/itp_interface/tools/coq_training_data_generator.py index 41786b2..910cea4 100644 --- a/src/itp_interface/tools/coq_training_data_generator.py +++ b/src/itp_interface/tools/coq_training_data_generator.py @@ -9,11 +9,6 @@ import logging import enum from itp_interface.tools.training_data_format import MergableCollection, TrainingDataFormat -from torch.multiprocessing import set_start_method -try: - set_start_method('spawn') -except RuntimeError: - pass logger = logging.getLogger("CoqTrainingGenerator") class TrainingDataGenerationType(enum.Enum): diff --git a/src/itp_interface/tools/run_data_generation_transforms.py b/src/itp_interface/tools/run_data_generation_transforms.py index a569004..36b75eb 100644 --- a/src/itp_interface/tools/run_data_generation_transforms.py +++ b/src/itp_interface/tools/run_data_generation_transforms.py @@ -14,7 +14,6 @@ import gc from itp_interface.tools.ray_utils import RayUtils from itp_interface.tools.training_data import TrainingData -from itp_interface.tools.coq_build_tool import CoqRepoBuilder from itp_interface.tools.coq_executor import CoqExecutor from itp_interface.tools.lean_cmd_executor import Lean3Executor from itp_interface.tools.lean4_sync_executor import Lean4SyncExecutor From 268404da222cc4fb81e9997a72f48e709e24f9f2 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 10 Feb 2025 01:11:12 -0600 Subject: [PATCH 3/4] Fixed README. --- README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index bae16f6..7b5d99b 100644 --- a/README.md +++ b/README.md @@ -195,18 +195,18 @@ action = ProofAction( 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: From abbeafa4c5b51b1453ade15866fce9d532d5c279 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 10 Feb 2025 01:52:09 -0600 Subject: [PATCH 4/4] Added data_gen test --- .github/workflows/github-build-actions.yaml | 11 +++- README.md | 2 + pyproject.toml | 2 +- .../benchmark/simple_benchmark_lean.yaml | 2 +- src/itp_interface/main/run_tool.py | 6 ++- src/test/simple_data_gen_test.py | 52 +++++++++++++++++++ 6 files changed, 69 insertions(+), 6 deletions(-) create mode 100644 src/test/simple_data_gen_test.py diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml index 07fb70d..96da286 100644 --- a/.github/workflows/github-build-actions.yaml +++ b/.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 \ No newline at end of file + 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 \ No newline at end of file diff --git a/README.md b/README.md index 7b5d99b..a0e0f76 100644 --- a/README.md +++ b/README.md @@ -193,6 +193,8 @@ 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: ``` run-itp-data-gen --config-dir src/itp_interface/main/configs --config-name simple_lean_data_gen diff --git a/pyproject.toml b/pyproject.toml index c3b5278..a6cbd0d 100644 --- a/pyproject.toml +++ b/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" }, ] diff --git a/src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml b/src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml index 59dd005..6d68f88 100644 --- a/src/itp_interface/main/configs/benchmark/simple_benchmark_lean.yaml +++ b/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: "*" \ No newline at end of file diff --git a/src/itp_interface/main/run_tool.py b/src/itp_interface/main/run_tool.py index 269f1b9..0346922 100644 --- a/src/itp_interface/main/run_tool.py +++ b/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="configs", 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()}") diff --git a/src/test/simple_data_gen_test.py b/src/test/simple_data_gen_test.py new file mode 100644 index 0000000..39a4afb --- /dev/null +++ b/src/test/simple_data_gen_test.py @@ -0,0 +1,52 @@ +import unittest +import os +import subprocess + +class TestDataGen(unittest.TestCase): + def test_proof_step_data_gen(self): + """ + Test that the 'run-itp-data-gen' command runs successfully with the given configuration. + """ + # Construct the command as a single string. + command = ( + "run-itp-data-gen --config-dir=src/itp_interface/main/configs " + "--config-name=simple_lean_data_gen.yaml" + ) + + try: + # Run the command using shell=True so that the shell does the PATH lookup. + result = subprocess.run( + command, + shell=True, + capture_output=True, + text=True, + timeout=700 + ) + except subprocess.TimeoutExpired as e: + self.fail(f"'run-itp-data-gen' command timed out: {e}") + except Exception as e: + self.fail(f"Error running 'proof-wala-search': {e}") + + # Check that the command exited with a return code of 0. + self.assertEqual( + result.returncode, 0, + msg=f"'run-itp-data-gen' failed with return code {result.returncode}. Stderr: {result.stderr}" + ) + + # Print all the files in the .log/data_generation/benchmark/simple_benchmark_lean + # directory to see what was generated. + # Do a list and pick the last folder in the list as per the sorted order + dirs = sorted(os.listdir(".log/data_generation/benchmark/simple_benchmark_lean")) + print(dirs) + last_dir = dirs[-1] + train_data = os.path.join(".log/data_generation/benchmark/simple_benchmark_lean", last_dir, "train") + data_gen_file = os.path.join(train_data, "local_data_0000000016.json") + print("Data Gen File:", data_gen_file) + with open(data_gen_file, "r") as f: + print(f.read()) + +def main(): + unittest.main() + +if __name__ == '__main__': + main() \ No newline at end of file