From 843887a3925384c4c0d4dfe2bf4c9de3582e685c Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 17:55:55 -0600 Subject: [PATCH 1/2] Fixed install dependencies vs build dependencies --- pyproject.toml | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 4c52eee..2725f30 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,24 @@ [build-system] requires = [ - "hatchling", + "hatchling" +] +build-backend = "hatchling.build" +[project] +name = "itp_interface" +version = "1.0.0" +authors = [ + { name="Amitayush Thakur", email="amitayush@utexas.edu" }, +] +description = "Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving." +readme = "README.md" +requires-python = ">=3.10" +classifiers = [ + "Programming Language :: Python :: 3", + "License :: OSI Approved :: MIT License", + "Operating System :: POSIX :: Linux", +] + +dependencies = [ "dataclasses-json==0.5.7", "numpy==1.23.2", "pexpect==4.8.0", @@ -24,21 +42,6 @@ requires = [ "urllib3>=2.0.7", "mathlibtools==1.3.2" ] -build-backend = "hatchling.build" -[project] -name = "itp_interface" -version = "1.0.0" -authors = [ - { name="Amitayush Thakur", email="amitayush@utexas.edu" }, -] -description = "Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving." -readme = "README.md" -requires-python = ">=3.10" -classifiers = [ - "Programming Language :: Python :: 3", - "License :: OSI Approved :: MIT License", - "Operating System :: POSIX :: Linux", -] [project.urls] Homepage = "https://github.com/trishullab/itp-interface" From cf414c691fe7b56ad09d81568a5212a31fea8ace Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sat, 8 Feb 2025 21:56:54 -0600 Subject: [PATCH 2/2] Added tests pyproject and added tests --- README.md | 148 ++++++++++++++++++++- pyproject.toml | 13 +- requirements.txt | 7 +- src/test/simpl_env_test.py | 256 +++++++++++++++++++++++++++++++++++++ tacc_requirements.txt | 7 +- 5 files changed, 417 insertions(+), 14 deletions(-) create mode 100644 src/test/simpl_env_test.py diff --git a/README.md b/README.md index 5640796..80abe48 100644 --- a/README.md +++ b/README.md @@ -39,13 +39,155 @@ export PATH="/home/$USER/.opam/default/bin:$PATH" 5. Run the commands for installing the Lean 4 interface as mentioned in [Quick Setup for Lean 4](#quick-setup-for-lean-4). -6. Change to the project root directory, and run the setup script i.e. `./src/scripts/setup.sh` from the root directory. - -7. Add the following to your `.bashrc` file for Lean: +6. Add the following to your `.bashrc` file for Lean: ``` export PATH="/home/$USER/.elan/bin:$PATH" ``` +## Running Simple Interactions: +1. Simple example for Lean 4 interaction: +```python +import os +from itp_interface.rl.proof_state import ProofState +from itp_interface.rl.proof_action import ProofAction +from itp_interface.rl.simple_proof_env import ProofEnv +from itp_interface.tools.proof_exec_callback import ProofExecutorCallback +from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy + +project_folder = "src/data/test/lean4_proj" +file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean" +# Code for building the Lean project +# cd src/data/test/lean4_proj && lake build +with os.popen(f"cd {project_folder} && lake build") as proc: + print("Building Lean4 project...") + print('-'*15 + 'Build Logs' + '-'*15) + print(proc.read()) + print('-'*15 + 'End Build Logs' + '-'*15) +# Skip the above code if the project is already built +language = ProofAction.Language.LEAN4 +theorem_name = "test3" +# theorem test3 (p q : Prop) (hp : p) (hq : q) +# : p ∧ q ∧ p := +proof_exec_callback = ProofExecutorCallback( + project_folder=project_folder, + file_path=file_path, + language=language, + always_use_retrieval=False, + keep_local_context=True +) +always_retrieve_thms = False +retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK +env = ProofEnv("test_lean4", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms) +proof_steps = [ + 'apply And.intro', + 'exact hp', + 'apply And.intro', + 'exact hq', + 'exact hp' +] +with env: + for proof_step in proof_steps: + action = ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, + tactics=[proof_step]) + state, _, next_state, _, done, info = env.step(action) + if info.error_message is not None: + print(f"Error: {info.error_message}") + # This prints StateChanged, StateUnchanged, Failed, or Done + print(info.progress) + print('-'*30) + if done: + print("Proof Finished!!") + else: + s1 : ProofState = state + s2 : ProofState = next_state + print(f"Current Goal:") + print('-'*30) + for goal in s1.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) + print(f"Action: {proof_step}") + print(f"="*30) + print(f"Next Goal:") + print('-'*30) + for goal in s2.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) +``` + +2. One can also backtrack the last proof action using the following code: +```python +action = ProofAction(ProofAction.ActionType.BACKTRACK, language) +state, _, next_state, _, done, info = env.step(action) +``` + +3. The code for Coq interaction is similar to the Lean 4 interaction. The only difference is the language used in the `ProofAction` object. The language for Coq is `ProofAction.Language.COQ`. We also need to make sure that the Coq project is **built** before running the code. Please note that it is important to install the **correct version of Coq and Coq LSP** for the Coq project. The following code snippet shows how to interact with Coq: +```python +project_folder = "src/data/test/coq/custom_group_theory/theories" +file_path = "src/data/test/coq/custom_group_theory/theories/grpthm.v" + +# IMPORTANT NOTE: The Coq project must be built before running the code. +# Create a switch for building the Coq project +if os.system("opam switch simple_grp_theory") != 0: + cmds = [ + 'opam switch create simple_grp_theory 4.14.1', + 'opam switch simple_grp_theory', + 'eval $(opam env)', + 'opam repo add coq-released https://coq.inria.fr/opam/released', + 'opam pin add -y coq 8.18.0', + 'opam pin add -y coq-lsp 0.1.8+8.18' + ] + final_cmd = ' && '.join(cmds) + os.system(final_cmd) +# IMPORTANT NOTE: Make sure to switch to the correct switch before running the code. +os.system("opam switch simple_grp_theory && eval $(opam env)") +# Clean the project +os.system(f"cd {project_folder} && make clean") +# Build the project +with os.popen(f"cd {project_folder} && make") as proc: + print("Building Coq project...") + print('-'*15 + 'Build Logs' + '-'*15) + print(proc.read()) + print('-'*15 + 'End Build Logs' + '-'*15) +# Skip the above code if the project is already built +language = ProofAction.Language.COQ # IMPORTANT NOTE: The language will change here to COQ +theorem_name = "algb_identity_sum" +# .... + +# IMPORTANT NOTE: As a result of language change, the `ProofExecutorCallback` object will also change. +proof_exec_callback = ProofExecutorCallback( + project_folder=project_folder, + file_path=file_path, + language=language, # The language will change here to COQ + always_use_retrieval=False, + keep_local_context=True +) + +# IMPORTANT NOTE: The proof steps will also change for Coq. +proof_steps = [ + 'intros.', + 'destruct a.', + '- reflexivity.', + '- reflexivity.' +] + +# IMPORTANT NOTE: As a result of language change, the `action` object will also change. +action = ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, # The language will change here to COQ + tactics=[proof_step] +) +``` + +4. See the file [src/test/simple_env_test.py](src/test/simple_env_test.py) for more examples for Lean 4 interaction and Coq interaction. + ## Generating Proof Step Data: 1.a. You need to run the following command to generate sample proof step data for Lean 4: diff --git a/pyproject.toml b/pyproject.toml index 2725f30..557bdcb 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,13 +5,13 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.0.0" +version = "1.1.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ] description = "Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving." readme = "README.md" -requires-python = ">=3.10" +requires-python = ">=3.10, <3.13" classifiers = [ "Programming Language :: Python :: 3", "License :: OSI Approved :: MIT License", @@ -20,7 +20,8 @@ classifiers = [ dependencies = [ "dataclasses-json==0.5.7", - "numpy==1.23.2", + "editdistance==0.8.1", + "numpy>=1.24.0", "pexpect==4.8.0", "sexpdata==1.0.0", "pampy==0.3.0", @@ -35,12 +36,14 @@ dependencies = [ "omegaconf>=2.0.1", "jsonlines==4.0.0", "soundfile==0.12.1", - "editdistance==0.6.2", "rank_bm25==0.2.2", "parglare==0.16.1", "psutil==5.9.8", "urllib3>=2.0.7", - "mathlibtools==1.3.2" + "mathlibtools==1.3.2", + "pylspclient==0.0.3", + "protobuf==3.20.1", + "grpcio==1.51.3" ] [project.urls] diff --git a/requirements.txt b/requirements.txt index 6a78bb7..0fbd10e 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,5 +1,5 @@ dataclasses-json==0.5.7 -numpy==1.23.2 +numpy>=1.24.0 pexpect==4.8.0 sexpdata==1.0.0 pampy==0.3.0 @@ -14,7 +14,7 @@ hydra-core>=1.0.0 omegaconf>=2.0.1 jsonlines==4.0.0 soundfile==0.12.1 -editdistance==0.6.2 +editdistance==0.8.1 rank_bm25==0.2.2 parglare==0.16.1 psutil==5.9.8 @@ -22,4 +22,5 @@ urllib3>=2.0.7 mathlibtools==1.3.2 pyyaml==6.0.1 pylspclient==0.0.3 -protobuf==3.20.1 \ No newline at end of file +protobuf==3.20.1 +grpcio==1.51.3 \ No newline at end of file diff --git a/src/test/simpl_env_test.py b/src/test/simpl_env_test.py new file mode 100644 index 0000000..03abd04 --- /dev/null +++ b/src/test/simpl_env_test.py @@ -0,0 +1,256 @@ +import unittest + +class Helper(): + def __init__(self): + self.current_switch = None + + def build_lean4_project(self, project_folder): + import os + # Build the project + with os.popen(f"cd {project_folder} && lake build") as proc: + print("Building Lean4 project...") + print('-'*15 + 'Build Logs' + '-'*15) + print(proc.read()) + print('-'*15 + 'End Build Logs' + '-'*15) + + def build_coq_project(self, project_folder): + import os + try: + with os.popen("opam switch show") as proc: + self.current_switch = proc.read().strip() + except: + self.current_switch = None + # Check if the switch exists + # opam switch create simple_grp_theory 4.14.1 + if os.system("opam switch simple_grp_theory") != 0: + cmds = [ + 'opam switch create simple_grp_theory 4.14.1', + 'opam switch simple_grp_theory', + 'eval $(opam env)', + 'opam repo add coq-released https://coq.inria.fr/opam/released', + 'opam pin add -y coq 8.18.0', + 'opam pin add -y coq-lsp 0.1.8+8.18' + ] + final_cmd = ' && '.join(cmds) + os.system(final_cmd) + # IMPORTANT NOTE: Make sure to switch to the correct switch before running the code. + os.system("opam switch simple_grp_theory && eval $(opam env)") + # Clean the project + os.system(f"cd {project_folder} && make clean") + # Build the project + with os.popen(f"cd {project_folder} && make") as proc: + print("Building Coq project...") + print('-'*15 + 'Build Logs' + '-'*15) + print(proc.read()) + print('-'*15 + 'End Build Logs' + '-'*15) + + def switch_to_current_switch(self): + import os + if self.current_switch is not None: + try: + proc = os.popen(f"opam switch {self.current_switch} && eval $(opam env)") + print(proc.read()) + finally: + proc.close() + +class Lean4Test(unittest.TestCase): + def test_simple_lean4(self): + from itp_interface.rl.proof_state import ProofState + from itp_interface.rl.proof_action import ProofAction + from itp_interface.rl.simple_proof_env import ProofEnv + from itp_interface.tools.proof_exec_callback import ProofExecutorCallback + from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy + project_folder = "src/data/test/lean4_proj" + file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean" + # Build the project + # cd src/data/test/lean4_proj && lake build + helper = Helper() + helper.build_lean4_project(project_folder) + language = ProofAction.Language.LEAN4 + theorem_name = "test3" + # theorem test3 (p q : Prop) (hp : p) (hq : q) + # : p ∧ q ∧ p := + proof_exec_callback = ProofExecutorCallback( + project_folder=project_folder, + file_path=file_path, + language=language, + always_use_retrieval=False, + keep_local_context=True + ) + always_retrieve_thms = False + retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK + env = ProofEnv("test_lean4", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms) + proof_steps = [ + 'apply And.intro', + 'exact hp', + 'apply And.intro', + 'exact hq', + 'exact hp' + ] + with env: + for proof_step in proof_steps: + state, _, next_state, _, done, info = env.step(ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, + tactics=[proof_step])) + if info.error_message is not None: + print(f"Error: {info.error_message}") + # This prints StateChanged, StateUnchanged, Failed, or Done + print(info.progress) + print('-'*30) + if done: + print("Proof Finished!!") + else: + s1 : ProofState = state + s2 : ProofState = next_state + print(f"Current Goal:") + print('-'*30) + for goal in s1.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) + print(f"Action: {proof_step}") + print(f"="*30) + print(f"Next Goal:") + print('-'*30) + for goal in s2.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) + + def test_lean4_backtracking(self): + from itp_interface.rl.proof_state import ProofState + from itp_interface.rl.proof_action import ProofAction + from itp_interface.rl.simple_proof_env import ProofEnv + from itp_interface.tools.proof_exec_callback import ProofExecutorCallback + from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy + import random + project_folder = "src/data/test/lean4_proj" + file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean" + # Build the project + helper = Helper() + helper.build_lean4_project(project_folder) + language = ProofAction.Language.LEAN4 + theorem_name = "test3" + # theorem test3 (p q : Prop) (hp : p) (hq : q) + # : p ∧ q ∧ p := + proof_exec_callback = ProofExecutorCallback( + project_folder=project_folder, + file_path=file_path, + language=language, + always_use_retrieval=False, + keep_local_context=True + ) + always_retrieve_thms = False + retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK + env = ProofEnv("test_lean4", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms) + proof_steps = [ + 'apply And.intro', + 'exact hp', + 'apply And.intro', + 'exact hq', + 'exact hp' + ] + with env: + prev_state = env.state + for idx, proof_step in enumerate(proof_steps): + if idx > 0 and random.random() <= 0.5: + print(f"Backtracking at step {idx + 1} i.e. {proof_step}") + state, _, next_state, _, done, info = env.step( + ProofAction( + ProofAction.ActionType.BACKTRACK, + language)) + assert next_state == prev_state, "Backtracking failed" + # Replay the last action + last_proof_step = proof_steps[idx-1] + state, _, next_state, _, done, info = env.step( + ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, + tactics=[last_proof_step])) + state, _, next_state, _, done, info = env.step( + ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, + tactics=[proof_step])) + prev_state = state + if done: + print("Proof Finished!!") + + def test_simple_coq(self): + from itp_interface.rl.proof_state import ProofState + from itp_interface.rl.proof_action import ProofAction + from itp_interface.rl.simple_proof_env import ProofEnv + from itp_interface.tools.proof_exec_callback import ProofExecutorCallback + from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy + project_folder = "src/data/test/coq/custom_group_theory/theories" + file_path = "src/data/test/coq/custom_group_theory/theories/grpthm.v" + # Build the project + # cd src/data/test/coq/custom_group_theory/theories && make + helper = Helper() + helper.build_coq_project(project_folder) + language = ProofAction.Language.COQ + theorem_name = "algb_identity_sum" + # Theorem algb_identity_sum : + # forall a, algb_add a e = a. + proof_exec_callback = ProofExecutorCallback( + project_folder=project_folder, + file_path=file_path, + language=language, + always_use_retrieval=False, + keep_local_context=True + ) + always_retrieve_thms = False + retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK + env = ProofEnv("test_coq", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms) + proof_steps = [ + 'intros.', + 'destruct a.', + '- reflexivity.', + '- reflexivity.' + ] + with env: + for proof_step in proof_steps: + state, _, next_state, _, done, info = env.step(ProofAction( + ProofAction.ActionType.RUN_TACTIC, + language, + tactics=[proof_step])) + if info.error_message is not None: + print(f"Error: {info.error_message}") + # This prints StateChanged, StateUnchanged, Failed, or Done + print(info.progress) + print('-'*30) + if done: + print("Proof Finished!!") + else: + s1 : ProofState = state + s2 : ProofState = next_state + print(f"Current Goal:") + print('-'*30) + for goal in s1.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) + print(f"Action: {proof_step}") + print(f"="*30) + print(f"Next Goal:") + print('-'*30) + for goal in s2.training_data_format.start_goals: + hyps = '\n'.join([hyp for hyp in goal.hypotheses]) + print(hyps) + print('|- ', end='') + print(goal.goal) + print(f"="*30) + helper.switch_to_current_switch() + +def main(): + unittest.main() + +if __name__ == '__main__': + main() \ No newline at end of file diff --git a/tacc_requirements.txt b/tacc_requirements.txt index 5ef89a9..a15bea4 100644 --- a/tacc_requirements.txt +++ b/tacc_requirements.txt @@ -1,5 +1,5 @@ dataclasses-json==0.5.7 -numpy==1.23.2 +numpy>=1.24.0 pexpect==4.8.0 sexpdata==1.0.0 pampy==0.3.0 @@ -14,7 +14,7 @@ hydra-core>=1.0.0 omegaconf>=2.0.1 jsonlines==4.0.0 soundfile==0.12.1 -editdistance==0.6.2 +editdistance==0.8.1 rank_bm25==0.2.2 parglare==0.16.1 psutil==5.9.8 @@ -22,4 +22,5 @@ urllib3>=2.0.7 mathlibtools==1.3.2 pyyaml==6.0.1 pylspclient==0.0.3 -protobuf==3.20.1 \ No newline at end of file +protobuf==3.20.1 +grpcio==1.51.3 \ No newline at end of file