Skip to content

Commit 83a77f5

Browse files
amit9octamit9oct
authored
Merge pull request #13 from trishullab/usr/amit9oct/adding-usecase-to-readme
Updated the README, added tests
2 parents 06ee04e + cf414c6 commit 83a77f5

File tree

5 files changed

+434
-28
lines changed

5 files changed

+434
-28
lines changed

‎README.md‎

Lines changed: 145 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -39,13 +39,155 @@ export PATH="/home/$USER/.opam/default/bin:$PATH"
3939

4040
5. Run the commands for installing the Lean 4 interface as mentioned in [Quick Setup for Lean 4](#quick-setup-for-lean-4).
4141

42-
6. Change to the project root directory, and run the setup script i.e. `./src/scripts/setup.sh` from the root directory.
43-
44-
7. Add the following to your `.bashrc` file for Lean:
42+
6. Add the following to your `.bashrc` file for Lean:
4543
```
4644
export PATH="/home/$USER/.elan/bin:$PATH"
4745
```
4846

47+
## Running Simple Interactions:
48+
1. Simple example for Lean 4 interaction:
49+
```python
50+
import os
51+
from itp_interface.rl.proof_state import ProofState
52+
from itp_interface.rl.proof_action import ProofAction
53+
from itp_interface.rl.simple_proof_env import ProofEnv
54+
from itp_interface.tools.proof_exec_callback import ProofExecutorCallback
55+
from itp_interface.rl.simple_proof_env import ProofEnvReRankStrategy
56+
57+
project_folder = "src/data/test/lean4_proj"
58+
file_path = "src/data/test/lean4_proj/Lean4Proj/Basic.lean"
59+
# Code for building the Lean project
60+
# cd src/data/test/lean4_proj && lake build
61+
with os.popen(f"cd {project_folder} && lake build") as proc:
62+
print("Building Lean4 project...")
63+
print('-'*15 + 'Build Logs' + '-'*15)
64+
print(proc.read())
65+
print('-'*15 + 'End Build Logs' + '-'*15)
66+
# Skip the above code if the project is already built
67+
language = ProofAction.Language.LEAN4
68+
theorem_name = "test3"
69+
# theorem test3 (p q : Prop) (hp : p) (hq : q)
70+
# : p ∧ q ∧ p :=
71+
proof_exec_callback = ProofExecutorCallback(
72+
project_folder=project_folder,
73+
file_path=file_path,
74+
language=language,
75+
always_use_retrieval=False,
76+
keep_local_context=True
77+
)
78+
always_retrieve_thms = False
79+
retrieval_strategy = ProofEnvReRankStrategy.NO_RE_RANK
80+
env = ProofEnv("test_lean4", proof_exec_callback, theorem_name, retrieval_strategy=retrieval_strategy, max_proof_depth=10, always_retrieve_thms=always_retrieve_thms)
81+
proof_steps = [
82+
'apply And.intro',
83+
'exact hp',
84+
'apply And.intro',
85+
'exact hq',
86+
'exact hp'
87+
]
88+
with env:
89+
for proof_step in proof_steps:
90+
action = ProofAction(
91+
ProofAction.ActionType.RUN_TACTIC,
92+
language,
93+
tactics=[proof_step])
94+
state, _, next_state, _, done, info = env.step(action)
95+
if info.error_message is not None:
96+
print(f"Error: {info.error_message}")
97+
# This prints StateChanged, StateUnchanged, Failed, or Done
98+
print(info.progress)
99+
print('-'*30)
100+
if done:
101+
print("Proof Finished!!")
102+
else:
103+
s1 : ProofState = state
104+
s2 : ProofState = next_state
105+
print(f"Current Goal:")
106+
print('-'*30)
107+
for goal in s1.training_data_format.start_goals:
108+
hyps = '\n'.join([hyp for hyp in goal.hypotheses])
109+
print(hyps)
110+
print('|- ', end='')
111+
print(goal.goal)
112+
print(f"="*30)
113+
print(f"Action: {proof_step}")
114+
print(f"="*30)
115+
print(f"Next Goal:")
116+
print('-'*30)
117+
for goal in s2.training_data_format.start_goals:
118+
hyps = '\n'.join([hyp for hyp in goal.hypotheses])
119+
print(hyps)
120+
print('|- ', end='')
121+
print(goal.goal)
122+
print(f"="*30)
123+
```
124+
125+
2. One can also backtrack the last proof action using the following code:
126+
```python
127+
action = ProofAction(ProofAction.ActionType.BACKTRACK, language)
128+
state, _, next_state, _, done, info = env.step(action)
129+
```
130+
131+
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:
132+
```python
133+
project_folder = "src/data/test/coq/custom_group_theory/theories"
134+
file_path = "src/data/test/coq/custom_group_theory/theories/grpthm.v"
135+
136+
# IMPORTANT NOTE: The Coq project must be built before running the code.
137+
# Create a switch for building the Coq project
138+
if os.system("opam switch simple_grp_theory") != 0:
139+
cmds = [
140+
'opam switch create simple_grp_theory 4.14.1',
141+
'opam switch simple_grp_theory',
142+
'eval $(opam env)',
143+
'opam repo add coq-released https://coq.inria.fr/opam/released',
144+
'opam pin add -y coq 8.18.0',
145+
'opam pin add -y coq-lsp 0.1.8+8.18'
146+
]
147+
final_cmd = ' && '.join(cmds)
148+
os.system(final_cmd)
149+
# IMPORTANT NOTE: Make sure to switch to the correct switch before running the code.
150+
os.system("opam switch simple_grp_theory && eval $(opam env)")
151+
# Clean the project
152+
os.system(f"cd {project_folder} && make clean")
153+
# Build the project
154+
with os.popen(f"cd {project_folder} && make") as proc:
155+
print("Building Coq project...")
156+
print('-'*15 + 'Build Logs' + '-'*15)
157+
print(proc.read())
158+
print('-'*15 + 'End Build Logs' + '-'*15)
159+
# Skip the above code if the project is already built
160+
language = ProofAction.Language.COQ # IMPORTANT NOTE: The language will change here to COQ
161+
theorem_name = "algb_identity_sum"
162+
# ....
163+
164+
# IMPORTANT NOTE: As a result of language change, the `ProofExecutorCallback` object will also change.
165+
proof_exec_callback = ProofExecutorCallback(
166+
project_folder=project_folder,
167+
file_path=file_path,
168+
language=language, # The language will change here to COQ
169+
always_use_retrieval=False,
170+
keep_local_context=True
171+
)
172+
173+
# IMPORTANT NOTE: The proof steps will also change for Coq.
174+
proof_steps = [
175+
'intros.',
176+
'destruct a.',
177+
'- reflexivity.',
178+
'- reflexivity.'
179+
]
180+
181+
# IMPORTANT NOTE: As a result of language change, the `action` object will also change.
182+
action = ProofAction(
183+
ProofAction.ActionType.RUN_TACTIC,
184+
language, # The language will change here to COQ
185+
tactics=[proof_step]
186+
)
187+
```
188+
189+
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.
190+
49191
## Generating Proof Step Data:
50192

51193
1.a. You need to run the following command to generate sample proof step data for Lean 4:

‎pyproject.toml‎

Lines changed: 25 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,27 @@
11
[build-system]
22
requires = [
3-
"hatchling",
3+
"hatchling"
4+
]
5+
build-backend = "hatchling.build"
6+
[project]
7+
name = "itp_interface"
8+
version = "1.1.0"
9+
authors = [
10+
{ name="Amitayush Thakur", email="[email protected]" },
11+
]
12+
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."
13+
readme = "README.md"
14+
requires-python = ">=3.10, <3.13"
15+
classifiers = [
16+
"Programming Language :: Python :: 3",
17+
"License :: OSI Approved :: MIT License",
18+
"Operating System :: POSIX :: Linux",
19+
]
20+
21+
dependencies = [
422
"dataclasses-json==0.5.7",
5-
"numpy==1.23.2",
23+
"editdistance==0.8.1",
24+
"numpy>=1.24.0",
625
"pexpect==4.8.0",
726
"sexpdata==1.0.0",
827
"pampy==0.3.0",
@@ -17,27 +36,14 @@ requires = [
1736
"omegaconf>=2.0.1",
1837
"jsonlines==4.0.0",
1938
"soundfile==0.12.1",
20-
"editdistance==0.6.2",
2139
"rank_bm25==0.2.2",
2240
"parglare==0.16.1",
2341
"psutil==5.9.8",
2442
"urllib3>=2.0.7",
25-
"mathlibtools==1.3.2"
26-
]
27-
build-backend = "hatchling.build"
28-
[project]
29-
name = "itp_interface"
30-
version = "1.0.0"
31-
authors = [
32-
{ name="Amitayush Thakur", email="[email protected]" },
33-
]
34-
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."
35-
readme = "README.md"
36-
requires-python = ">=3.10"
37-
classifiers = [
38-
"Programming Language :: Python :: 3",
39-
"License :: OSI Approved :: MIT License",
40-
"Operating System :: POSIX :: Linux",
43+
"mathlibtools==1.3.2",
44+
"pylspclient==0.0.3",
45+
"protobuf==3.20.1",
46+
"grpcio==1.51.3"
4147
]
4248

4349
[project.urls]

‎requirements.txt‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
dataclasses-json==0.5.7
2-
numpy==1.23.2
2+
numpy>=1.24.0
33
pexpect==4.8.0
44
sexpdata==1.0.0
55
pampy==0.3.0
@@ -14,12 +14,13 @@ hydra-core>=1.0.0
1414
omegaconf>=2.0.1
1515
jsonlines==4.0.0
1616
soundfile==0.12.1
17-
editdistance==0.6.2
17+
editdistance==0.8.1
1818
rank_bm25==0.2.2
1919
parglare==0.16.1
2020
psutil==5.9.8
2121
urllib3>=2.0.7
2222
mathlibtools==1.3.2
2323
pyyaml==6.0.1
2424
pylspclient==0.0.3
25-
protobuf==3.20.1
25+
protobuf==3.20.1
26+
grpcio==1.51.3

0 commit comments

Comments
 (0)