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.