The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

> coqide seems to invoke not coqtop, but coqidetop.  What is the difference?

I believe coqtop runs coqtop_bin.ml and coqidetop runs idetop.ml.  They both invoke Coqtop.start_coq.  You should be able to figure out the differences.  I don't know offhand.

> What is the protocol spoken between coqide and coqidetop?

dev/doc/xml-protocol.md in the Coq source tree is a better source for info on the protocol, though probably quite similar to the VSCode document.

> Is the protocol the same between Proof General and whatever coq program PG invokes?

PG communicates with `coqtop -emacs`.  It is not XML.

I understand there is also an "async" version of PG that uses the XML protocol, but I believe it is not in a usable state.

AFAIK the current plan for Coq is to create a new protocol, probably very similar to LSP (Language Server Protocol).

> I find PG to be a badly behaved Emacs package in several ways, so I'm tempted to do my own.

Why not discuss your concerns with the PG team and see if there's a way to work together and address your concerns?  That might get quicker results with less effort.  Creating another flavor of PG may just fragment Coq PG users.

Hope this helps,

Jim

On Thu, Oct 31, 2019 at 12:51 PM Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz> wrote:

2, 3. Some XML protocol. The official documentation is poor.

Relevant links:

Notes of VSCode extension's creator:

https://github.com/siegebell/vscoq/wiki/XML-protocol

Library for interaction with Coq in OCaml: 

https://github.com/ejgallego/coq-serapi

Kind regards,

Rustam

On Fri, Nov 1, 2019 at 1:26 AM Ian Zimmerman <itz AT very.loosely.org> wrote:

I have a series of related questions about coq user interfaces.

1. coqide seems to invoke not coqtop, but coqidetop.  What is the
difference?

2. What is the protocol spoken between coqide and coqidetop?  Is it
documented somewhere?

3. Is the protocol the same between Proof General and whatever coq
program PG invokes?

I am an Emacs user since forever (as some people here know, ahem) and I
would really very much prefer an Emacs interface to coq, but I find PG
to be a badly behaved Emacs package in several ways, so I'm tempted to
do my own.

--
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.