coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] questions about using search command in coqtop ideslave

From: zjhsdtc <zjhsdtc AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] questions about using search command in coqtop ideslave
Date: Wed, 5 Oct 2016 09:49:07 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=zjhsdtc AT gmail.com; spf=Pass smtp.mailfrom=zjhsdtc AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
Ironport-phdr: 9a23:sG8HeRb2xpTQWCuL9oafmuH/LSx+4OfEezUN459isYplN5qZpc64bnLW6fgltlLVR4KTs6sC0LuM9fqwEjFeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3p7xjbD5psObSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWXwmP/XcAWS1CgBhIGATZ5zn1W57wtm3xse8ri3rSBtH/Ub1hAWfq1KxsUhK90Co=

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,

[Coq-Club] questions about using search command in coqtop ideslave, zjhsdtc, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
  - Re: [Coq-Club] questions about using search command in coqtop ideslave, zjhsdtc, 10/05/2016
    - Re: [Coq-Club] questions about using search command in coqtop ideslave, James Smith, 10/05/2016
      - Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
        
        Re: [Coq-Club] questions about using search command in coqtop ideslave, James Smith, 10/06/2016