Error running example.py as is?

[brando90]

@HazardousPeach I was trying to run the examply.py as is without modifications but it doesn't seem to work?

Didn't find _CoqProject or Make for .
Problem running statement: Theorem t: forall n: nat, 1 + n > n.
((CoqGoal((goals(((info((evar(Ser_Evar 1))(name())))(ty(Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Peano)(Id Init)(Id Coq))))(Id gt))(Instance())))((App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(Id add))(Instance())))((App(Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)2)(Instance())))((Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)1)(Instance())))))(Rel 1)))(Rel 1)))))(hyp()))))(stack())(bullet())(shelf())(given_up()))))
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 645, in run_stmt
    self._get_proof_context(update_nonfg_goals=False)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1278, in _get_proof_context
    raise BadResponse(context_str)
coq_serapy.BadResponse: ((CoqGoal((goals(((info((evar(Ser_Evar 1))(name())))(ty(Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Peano)(Id Init)(Id Coq))))(Id gt))(Instance())))((App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(Id add))(Instance())))((App(Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)2)(Instance())))((Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)1)(Instance())))))(Rel 1)))(Rel 1)))))(hyp()))))(stack())(bullet())(shelf())(given_up()))))
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1126, in _get_message_text
    msg = self.message_queue.get(timeout=self.timeout)
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/queue.py", line 179, in get
    raise Empty
_queue.Empty
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1169, in _get_message_text
    after_interrupt_msg = loads(self.message_queue.get(
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/queue.py", line 179, in get
    raise Empty
_queue.Empty
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/contextlib.py", line 137, in __exit__
    self.gen.throw(typ, value, traceback)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1458, in SerapiContext
    yield coq
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/example.py", line 35, in main
    cmds_left, cmds_run = coq.run_into_next_proof(
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1363, in run_into_next_proof
    self.run_stmt(command, timeout=60)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 674, in run_stmt
    self._handle_exception(e, stmt)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 754, in _handle_exception
    self._get_completed()
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 948, in _get_completed
    completed = self._get_message()
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1107, in _get_message
    msg_text = self._get_message_text(complete=complete)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1172, in _get_message_text
    raise CoqAnomaly("Timing out")
coq_serapy.CoqAnomaly: Timing out

Also, what is the make file suppose to be like? (first error line)

[brando90]

similar error with a different set up:

Problem running statement: Theorem add_easy_0:
forall n:nat,
  0 + n = n.
((CoqGoal((goals(((info((evar(Ser_Evar 2))(name())))(ty(Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Ind(((MutInd(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(Id eq))0)(Instance())))((Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(Id add))(Instance())))((Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)1)(Instance())))(Rel 1)))(Rel 1)))))(hyp()))))(stack())(bullet())(shelf())(given_up()))))
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 645, in run_stmt
    self._get_proof_context(update_nonfg_goals=False)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1278, in _get_proof_context
    raise BadResponse(context_str)
coq_serapy.BadResponse: ((CoqGoal((goals(((info((evar(Ser_Evar 2))(name())))(ty(Prod((binder_name(Name(Id n)))(binder_relevance Relevant))(Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Ind(((MutInd(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(Id eq))0)(Instance())))((Ind(((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(Id add))(Instance())))((Construct((((MutInd(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(Id nat))0)1)(Instance())))(Rel 1)))(Rel 1)))))(hyp()))))(stack())(bullet())(shelf())(given_up()))))
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1126, in _get_message_text
    msg = self.message_queue.get(timeout=self.timeout)
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/queue.py", line 179, in get
    raise Empty
_queue.Empty
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1169, in _get_message_text
    after_interrupt_msg = loads(self.message_queue.get(
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/queue.py", line 179, in get
    raise Empty
_queue.Empty
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
  File "/Users/brandomiranda/miniconda/envs/coq_serapy/lib/python3.9/contextlib.py", line 137, in __exit__
    self.gen.throw(typ, value, traceback)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1458, in SerapiContext
    yield coq
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/example_showing_proof_term.py", line 63, in main
    cmds_left, cmds_run = coq.run_into_next_proof(proof_commands)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1363, in run_into_next_proof
    self.run_stmt(command, timeout=60)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 674, in run_stmt
    self._handle_exception(e, stmt)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 754, in _handle_exception
    self._get_completed()
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 948, in _get_completed
    completed = self._get_message()
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1107, in _get_message
    msg_text = self._get_message_text(complete=complete)
  File "/Users/brandomiranda/coq_serapy/src/coq_serapy/__init__.py", line 1172, in _get_message_text
    raise CoqAnomaly("Timing out")
coq_serapy.CoqAnomaly: Timing out
python-BaseException

[brando90]

I think I am now running the right cop and ocaml version. So why do I still have issues @HazardousPeach?

See my opam setup:

# - create switch with right coq version
# install opam
#brew install opam
# conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
eval $(opam env)

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create debug_proj_4.09.1 4.09.1
opam switch debug_proj_4.09.1
opam repo add coq-released https://coq.inria.fr/opam/released
# install the right version of coq and pins it to it so that future opam installs don't change the coq version
opam pin add coq 8.11.0

# - install coq-serapi
opam install coq-serapi

I can't have the example file run. Is there something I am missing?

[HazardousPeach]

Oops sorry it took me so long to get to this issue, for some reason I didn't get a notification or anything. You say that "now" you're running on the right coq and ocaml versions, so I assume you weren't when you posted the first two error message? Those errors look very much like ones you would get from an improper coq version (they are failing to parse the goal string, which changed formats between 8.12 and 8.13). So, now that you have the correct Coq version, is the error any different?