Stream: SerAPI

Topic: debugging interactions with serapi


view this post on Zulip Brando Miranda (Jun 10 2022 at 18:38):

Hi, I'm not sort of new with zulip so hope this is the right way to start a discussion. I got a ser_api error (Answer 6 (Added 5 ((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 3) (bol_pos_last 34) (bp 0) (ep 46)) NewAddTip)) someone knows what it means? The command I sent was pretty simple '(Add () "Theorem add_easy_0:\nforall n:nat,\n 0 + n = n.\n")\n' but it failed. I sent it using coq_serapy.

view this post on Zulip Paolo Giarrusso (Jun 10 2022 at 19:22):

why do you think that's an error? That looks like a successful result?

view this post on Zulip Brando Miranda (Jun 11 2022 at 01:00):

actually I think I made a mistake. I can't remember why I said that right now. Sorry let me go back to check what I was doing. Apologies.

view this post on Zulip Brando Miranda (Jun 11 2022 at 01:07):

the error I have is a little longer in the context of python but this I think a better summary ((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()))))

view this post on Zulip Paolo Giarrusso (Jun 11 2022 at 01:30):

I’m not very familiar with SerAPI, but can you say why you think that is an error? This message seems an internal representation of a Coq goal; the goal seems to contain fragments such as \forall n : Coq.Init.Datatypes.nat, …, Coq.Init.Logic.eq and Coq.Init.Nat.add. For some reason those paths are encoded not at Coq.Init.Logic.eq but as Logic.Init.Coq, eq

view this post on Zulip Paolo Giarrusso (Jun 11 2022 at 01:32):

but mine are only educated guesses, and there are quite a few details of the internal representation that seem more mysterious.

view this post on Zulip Brando Miranda (Jun 11 2022 at 02:12):

this came form the tool coq_serapy (from prover bot). The first thing it says is problem running statement, but this is the full message. It is also in red making me think it's an error and calling a bunch of python's exception catchers:

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 09:32):

@Brando Miranda it seems to me that the problem here is that you are using a coq-serapy version with an unsupporte coq-serapi version

view this post on Zulip Brando Miranda (Jun 11 2022 at 12:31):

@Emilio Jesús Gallego Arias Curious, how did you know that was the issue?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):

The error message says it, doesn't it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):

is that the issue by the way?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):

I don't really know, that was an hypothesis

view this post on Zulip Brando Miranda (Jun 23 2022 at 16:52):

@Emilio Jesús Gallego Arias can serapi give me each separate goal as an actual coq string? like currently it gives the entire local context

  >   "\
  >    \n  n : nat\
  >    \n============================\
  >    \nn + 0 = n"

without separating each thing. I suppose one could try to parse it oneself using the \n new line char?

view this post on Zulip Brando Miranda (Jun 23 2022 at 16:55):

Or in a related note -- given a single goal as a serapi s-exp string, is it possible to transform it into a normal human coq string?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:28):

I guess you can:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:28):

yes I think Print should work for you

view this post on Zulip Brando Miranda (Jun 23 2022 at 18:57):

for your second option do you mean to get the pretty string from serapi and parse it myself e.g. through a \n character? (hopefully if the term is to large it doesn't decide to add random \n or some weird edge case)

For the first option I don't know what I'd write in my PR since if I knew how to implement this I'd be doing it perhaps...perhaps you menat gitissue?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:11):

Open an issue yes, that seems useful

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:11):

For the second option I mean you can get the goals, then send the sexp to serapi with (Print )

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:12):

so you 1. get all the goals in sepx format 2. print the one you'd like

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:12):

that's an extra roundtrip

view this post on Zulip Brando Miranda (Jun 23 2022 at 19:56):

Thanks Emilio That was helpful.

Is there a precise grammar specifying the way to talk to SerApi? Or do I have to infer it from the OCaml code https://github.com/ejgallego/coq-serapi?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):

There are some docs

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):

http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi/Serapi_protocol/

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):

not super great

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):

but they are a starting pont

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):

point

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):

tho you may be better with pyCoq

view this post on Zulip Brando Miranda (Jun 23 2022 at 19:57):

is the ocaml code better?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):

doc is based on the OCaml code

view this post on Zulip Brando Miranda (Jun 23 2022 at 19:57):

pycoq you mean https://github.com/ejgallego/pycoq ?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

tho it is very experimental, depending how you are YMMV

view this post on Zulip Brando Miranda (Jun 23 2022 at 19:58):

curious, how is it better?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

it is basically the same, but you can inspect things a bit better with the Python interface

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

it saves you a round trip

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

and it is python

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

it is the same underlying stuff

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

YMMV

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):

I mean maybe the doc is better as you can inspect things in python

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 20:07):

but on the other hand is way more immature

view this post on Zulip Brando Miranda (Jun 23 2022 at 20:28):

The instructions for building your PyCoq are confusing. After doing the opam commands you recommend the instructions say to do $ make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py but its confusing if I have to git clone your pycoq or what to do...why don't the instructions have a single pip install like any normal python package? Anyway, after the opam stuff what do I do to install your pycoq?

view this post on Zulip Brando Miranda (Jun 23 2022 at 20:29):

There is this git command git submodule update --init --recursive. Where do I run that -- if at all?

view this post on Zulip Brando Miranda (Jun 28 2022 at 20:50):

@Emilio Jesús Gallego Arias what is the difference between these two: user-level AST and kernel terms? Is a kernel term the ones that expose the PL modling like App (id f) (id x) but that uses see as f x?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2022 at 19:36):

Actually i wrote a document answering this question but I can't locate it right now

view this post on Zulip Emilio Jesús Gallego Arias (Jun 29 2022 at 19:36):

:(


Last updated: Feb 06 2023 at 07:03 UTC