Using CoqGym on my own files

Using Coq
1

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. 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. :slight_smile:

2

And how did all the .meta files created?

3

coqgym has its own discussion forum. I’d suggest you ask your questions there: 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.

1 Like
4

@brando90 thank you!