# Using CoqGym on my own files

**URL:** <https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099>\
**Category:** Using Rocq\
**Created:** [October 29, 2020, 3:59am UTC](https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099 "2020-10-29T03:59:58Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![jinxing1990](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jinxing1990/32/522_2.png) [@jinxing1990](https://discourse.rocq-prover.org/u/jinxing1990)\
**Post date:** [October 29, 2020, 3:59am UTC](https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099/1 "2020-10-29T03:59:58Z")

</div>

Hi, may I ask how could I run ASTactic on the proofs from my own .v files? From what I understand is that, I need to extract the proofs from my own coq files to .json format. I tried to follow the steps in Section 1.3 from [https://github.com/princeton-vl/CoqGym#13-extracting-the-proofs-from-coq-code-optional](https://github.com/princeton-vl/CoqGym#13-extracting-the-proofs-from-coq-code-optional). But I have encounter an error:

Traceback (most recent call last):  
File “check\_proofs.py”, line 94, in   
process\_file(filename)  
File “check\_proofs.py”, line 62, in process\_file  
file\_data = check\_file(filename, sexp\_cache, args)  
File “check\_proofs.py”, line 13, in check\_file  
loc2code = get\_code(open(coq\_filename, ‘rb’).read())  
FileNotFoundError: [Errno 2] No such file or directory: …

My goal is to apply the ASTactic to automate the proofs from my Coq file. How could I do it? Anyone has any advice? Thank you. 🙂

---

<div class="post-metadata">

**Author:** ![jinxing1990](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jinxing1990/32/522_2.png) [@jinxing1990](https://discourse.rocq-prover.org/u/jinxing1990)\
**Post date:** [October 29, 2020, 4:39am UTC](https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099/2 "2020-10-29T04:39:39Z")

</div>

And how did all the .meta files created?

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [January 6, 2021, 7:23pm UTC](https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099/3 "2021-01-06T19:23:01Z")

</div>

coqgym has its own discussion forum. I’d suggest you ask your questions there: [https://github.com/princeton-vl/CoqGym/discussions](https://github.com/princeton-vl/CoqGym/discussions)

* * *

you might also be interested in the tactician system (and IDE) to help you choose tactics while you write your proofs scripts.

---

<div class="post-metadata">

**Author:** ![jinxing1990](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jinxing1990/32/522_2.png) [@jinxing1990](https://discourse.rocq-prover.org/u/jinxing1990)\
**Post date:** [January 7, 2021, 1:45am UTC](https://discourse.rocq-prover.org/t/using-coqgym-on-my-own-files/1099/4 "2021-01-07T01:45:43Z")

</div>

@brando90 thank you!