Using CoqGym on my own files

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 But I have encounter an error:

Traceback (most recent call last):
File “”, line 94, in
File “”, line 62, in process_file
file_data = check_file(filename, sexp_cache, args)
File “”, 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:

And how did all the .meta files created?

coqgym has its own discussion forum. I’d suggest you ask your questions there:

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

1 Like

@brando90 thank you!