Brando Miranda (Jun 10 2022 at 18:38): 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.
Paolo Giarrusso (Jun 10 2022 at 19:22):why do you think that's an error? That looks like a successful result?
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.
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()))))
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
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.
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
@Brando Miranda it seems to me that the problem here is that you are using a coq-serapy version with an unsupported coq-serapi version
Brando Miranda (Jun 11 2022 at 12:31):@Emilio Jesús Gallego Arias Curious, how did you know that was the issue?
Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):The error message says it, doesn't it?
Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):is that the issue by the way?
Emilio Jesús Gallego Arias (Jun 11 2022 at 12:46):I don't really know, that was an hypothesis
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?
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?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:28):I guess you can:
Goal query(Print ...) later on? Emilio Jesús Gallego Arias (Jun 23 2022 at 17:28):yes I think Print should work for you
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?
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:11):Open an issue yes, that seems useful
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 )
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
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:12):that's an extra roundtrip
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?
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):There are some docs
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi/Serapi_protocol/
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:56):not super great
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):but they are a starting pont
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):point
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):tho you may be better with pyCoq
Brando Miranda (Jun 23 2022 at 19:57):is the ocaml code better?
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):doc is based on the OCaml code
Brando Miranda (Jun 23 2022 at 19:57):pycoq you mean https://github.com/ejgallego/pycoq ?
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:57):yes
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):tho it is very experimental, depending how you are YMMV
Brando Miranda (Jun 23 2022 at 19:58):curious, how is it better?
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
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):it saves you a round trip
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):and it is python
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):it is the same underlying stuff
Emilio Jesús Gallego Arias (Jun 23 2022 at 19:58):YMMV
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
Emilio Jesús Gallego Arias (Jun 23 2022 at 20:07):but on the other hand is way more immature
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?
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?
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?
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
Emilio Jesús Gallego Arias (Jun 29 2022 at 19:36)::(
Last updated: Jun 01 2023 at 13:01 UTC