The Coq mailing list

[Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz>]

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.