From 4de5f3c42941364b67e470aa36295a4eb42af8ec Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 22:47:11 -0600 Subject: [PATCH 1/4] Added config files for packaging. --- src/itp_interface/main/config/__init__.py | 0 src/itp_interface/main/config/benchmark/__init__.py | 0 src/itp_interface/main/config/env_settings/__init__.py | 0 src/itp_interface/main/config/repo/__init__.py | 0 src/itp_interface/main/config/run_settings/__init__.py | 0 5 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 src/itp_interface/main/config/__init__.py create mode 100644 src/itp_interface/main/config/benchmark/__init__.py create mode 100644 src/itp_interface/main/config/env_settings/__init__.py create mode 100644 src/itp_interface/main/config/repo/__init__.py create mode 100644 src/itp_interface/main/config/run_settings/__init__.py diff --git a/src/itp_interface/main/config/__init__.py b/src/itp_interface/main/config/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/itp_interface/main/config/benchmark/__init__.py b/src/itp_interface/main/config/benchmark/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/itp_interface/main/config/env_settings/__init__.py b/src/itp_interface/main/config/env_settings/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/itp_interface/main/config/repo/__init__.py b/src/itp_interface/main/config/repo/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/itp_interface/main/config/run_settings/__init__.py b/src/itp_interface/main/config/run_settings/__init__.py new file mode 100644 index 0000000..e69de29 From a65f0edb1ebc7f71025410ad7e324c1dd4f14b42 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 22:47:29 -0600 Subject: [PATCH 2/4] Updated version number and added data gen command. --- pyproject.toml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index bc40253..c3b5278 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.1.0" +version = "1.1.1" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] @@ -52,4 +52,5 @@ Issues = "https://github.com/trishullab/itp-interface/issues" [project.scripts] install-itp-interface = "itp_interface.main.install:install_itp_interface" -install-lean-repl = "itp_interface.main.install:install_lean_repl" \ No newline at end of file +install-lean-repl = "itp_interface.main.install:install_lean_repl" +run-itp-data-gen = "itp_interface.main.run_tool:main" \ No newline at end of file From 9be563fec9ad18d1eb48cd7ca612cf42e363a8b8 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 22:47:57 -0600 Subject: [PATCH 3/4] Fixed readme. --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index a1fc510..1029a31 100644 --- a/README.md +++ b/README.md @@ -26,9 +26,9 @@ install-itp-interface >NOTE: These steps are only tested on Linux. For Windows, you can use WSL. These steps will not setup the Coq interface. # Full Setup for Coq and Lean: -1. Install OCaml first. Use the instructions here: https://opam.ocaml.org/doc/Install.html . The opam version used in this project is 2.1.3 (OCaml 4.14.0). Note that OCaml officially only supports Linux installations. One can use WSL on Windows machines. +1. Install OCaml first. Use the instructions here: https://opam.ocaml.org/doc/Install.html. Note that OCaml officially only supports Linux installations. One can use WSL on Windows machines. -2. Run the following to install Coq on Linux. The Coq version used in this project is <= 8.15. +2. Run the following to install Coq on Linux. ``` sudo apt install build-essential unzip bubblewrap sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) @@ -195,15 +195,15 @@ action = ProofAction( 1.a. You need to run the following command to generate sample proof step data for Lean 4: ``` -python src/itp_interface/main/run_tool.py --config-name simple_lean_data_gen +python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name simple_lean_data_gen ``` -Check the `simple_lean_data_gen.yaml` configuration in the `src/itp_interface/configs` 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/config` 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 src/itp_interface/main/run_tool.py --config-name simple_coq_data_gen +python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name simple_coq_data_gen ``` -Check the `simple_coq_data_gen.yaml` configuration in the `src/itp_interface/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. +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. ## 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. \ No newline at end of file From 3d963dec80971ec71b52f4de9e8d55943f63ef4e Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 9 Feb 2025 22:48:51 -0600 Subject: [PATCH 4/4] Added paper citation to README. --- README.md | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 1029a31..bae16f6 100644 --- a/README.md +++ b/README.md @@ -206,4 +206,20 @@ python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name 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. ## 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. \ No newline at end of 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/config/repo/coq_repos.yaml` file. + +## Our Paper: + +For more details, please refer to our paper: [ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving](https://arxiv.org/abs/2502.04671). + +```bibtex +@misc{thakur2025proofwala, + title={${\rm P{\small ROOF}W{\small ALA}}$: Multilingual Proof Data Synthesis and Theorem-Proving}, + author={Amitayush Thakur and George Tsoukalas and Greg Durrett and Swarat Chaudhuri}, + year={2025}, + eprint={2502.04671}, + archivePrefix={arXiv}, + primaryClass={cs.AI}, + url={https://arxiv.org/abs/2502.04671}, +} +``` \ No newline at end of file