check_proofs.py raise exception or errors

[smirnoffalexx]

Hello!
I am sorry for disturbing you again, but I have problems while producing .json files. I tried to do it with my coq files and with your coq_projects, it always raise exception or errors. For example, I compiled ramsey folder (there are .meta file and etc) and I ran:
python check_proofs.py --file coq_projects/ramsey/Ramsey.meta , below I send logs:
(base) root@ed5fcdca75c7:/CoqGym# python check_proofs.py --file coq_projects/ramsey/Ramsey.meta
1 Coq files to process

coq_projects/ramsey/Ramsey.meta
Traceback (most recent call last):
  File "check_proofs.py", line 116, in <module>
    process_file(filename)
  File "check_proofs.py", line 66, in process_file
    file_data = check_file(filename, sexp_cache, args)
  File "check_proofs.py", line 23, in check_file
    with SerAPI(args.timeout, args.debug) as serapi:
  File "/CoqGym/serapi.py", line 82, in __init__
    "(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))\0"
  File "/root/miniconda3/lib/python3.7/site-packages/pexpect/spawnbase.py", line 421, in expect_exact
    return exp.expect_loop(timeout)
  File "/root/miniconda3/lib/python3.7/site-packages/pexpect/expect.py", line 179, in expect_loop
    return self.eof(e)
  File "/root/miniconda3/lib/python3.7/site-packages/pexpect/expect.py", line 122, in eof
    raise exc
pexpect.exceptions.EOF: End Of File (EOF).
<pexpect.popen_spawn.PopenSpawn object at 0x7f54af11e1d0>
searcher: searcher_string:
    0: '(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))\x00'

Also, I tried to run this:
python check_proofs.py --file /coq_projects/ramsey/Ramsey.meta (what changed: I add / before path_to_meta_file)
What I have got:

(base) root@ed5fcdca75c7:/CoqGym# python check_proofs.py --file /coq_projects/ramsey/Ramsey.meta
1 Coq files to process

/coq_projects/ramsey/Ramsey.meta
Traceback (most recent call last):
  File "check_proofs.py", line 116, in <module>
    process_file(filename)
  File "check_proofs.py", line 66, 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: '/coq_projects/ramsey/Ramsey.v'

How to solve this problem?

[yangky11]

I'll take a look this weekend.

[yangky11]

Update: sorry it was a busy week and I wasn't able to work on it last weekend. I'll try this weekend.

[smirnoffalexx]

I tried to rebuild everything including modified coq, now it works. (maybe there were some incompatibilities, but coq generated *meta files after compilation)
And correct use of this command: python check_proofs.py --file coq_projects/ramsey/Ramsey.meta (otherwise it raises errors)

[yangky11]

Glad to hear that