Skip to content

Commit 268404d

Browse files
author
Amitayush Thakur
committed
Fixed README.
1 parent d789010 commit 268404d

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

README.md

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -195,18 +195,18 @@ action = ProofAction(
195195

196196
1.a. You need to run the following command to generate sample proof step data for Lean 4:
197197
```
198-
python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name simple_lean_data_gen
198+
run-itp-data-gen --config-dir src/itp_interface/main/configs --config-name simple_lean_data_gen
199199
```
200-
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/)).
200+
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/)).
201201

202202
1.b. You need to run the following command to generate sample proof step data for Coq:
203203
```
204-
python run-itp-data-gen --config-dir src/itp_interface/main/config --config-name simple_coq_data_gen
204+
run-itp-data-gen --config-dir src/itp_interface/main/configs --config-name simple_coq_data_gen
205205
```
206-
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.
206+
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.
207207

208208
## Important Note:
209-
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.
209+
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.
210210

211211
## Our Paper:
212212

0 commit comments

Comments
 (0)