The Coq mailing list

[James Smith <jecs AT imperial.ac.uk>]

Hi,

I saw something come up the other week on this XML protocol, I'm very interested in it. I googled it at the time but came up empty handed.

Not being conversant in ML, can I ask whether there is any chance of some conventional documentation on this protocol any time soon?

Kind regards,

James

On 05/10/16 14:49, zjhsdtc wrote:

Hi CJ Bell,

Thanks for the detailed answer! and xmlprotocol.ml is pretty neat, i will try to search around the source code before my next question about Coq :D

​

2016-10-05 11:53 GMT+08:00 CJ Bell <siegebell+coq AT gmail.com>:

The code for encoding and decoding this call is here:

1. the type of the Search call is a list of pairs, the first being a constraint and the second a bool: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L464

2. the constraint type: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L25

3. the return type is a list of pairs of Coq objects and strings: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L488

Example search for regex "nat_rect.+":

<call val="Search"><list><pair><search_cst val="name_pattern"><string>nat_rect.+</string></search_cst><bool val="true"/></pair></list></call

Returns:

<value val="good"><list><coq_object><list><string>Coq</string><string>Init</string><string>Peano</string></list><list><string>nat_rect_plus</string></list><string>forall&nbsp;(n&nbsp;m&nbsp;:&nbsp;nat)&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(f&nbsp;:&nbsp;A&nbsp;-&gt;&nbsp;A)&nbsp;(x&nbsp;:&nbsp;A),
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;(n&nbsp;+&nbsp;m)&nbsp;=
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)
&nbsp;&nbsp;(nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;m)&nbsp;
&nbsp;&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;n</string></coq_object><coq_object><list><string>Coq</string><string>Init</string><string>Peano</string></list><list><string>nat_rect_succ_r</string></list><string>forall&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(f&nbsp;:&nbsp;A&nbsp;-&gt;&nbsp;A)&nbsp;(x&nbsp;:&nbsp;A)&nbsp;(n&nbsp;:&nbsp;nat),
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;(S&nbsp;n)&nbsp;=
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;(f&nbsp;x)&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;n</string></coq_object></list></value>

-cj

On Tue, Oct 4, 2016 at 9:49 PM, zjhsdtc <zjhsdtc AT gmail.com> wrote:

Hi all,

There is something that has confused me for quite a while. if we use coqtop -ideslave --help-XML-protocol, it will produce a list of commands available in the ideslave, e.g. the Goal command, so we can simply send <call val="Goal"><unit/></call> to ideslave, i can easily play around with these commands except the Search one.

According to the brief documentation, it seems have to send a list of search constraint and boolean value pairs inside <call val="Search">...</call>, but after trying and failing for many times, i still can not find a way to construct a qualified xml message to stand for a search command.

So is there any examples to use Search command in ideslave or anyone have an idea how to use it?

Thank you,

​