The Coq mailing list

[CJ Bell <siegebell+coq AT gmail.com>]

Speaking of the CoqIDE XML protocol, I've partially documented it here:

https://github.com/siegebell/vscoq/blob/master/CoqProtocol.md

and I will add more as I play around with it.

To Jason: the XML protocol sends status updates for each processed sentence, but Proof General uses emacs mode...

-cj

On Fri, Jan 29, 2016 at 3:23 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Thu, Jan 28, 2016 at 10:01:54PM -0500, Kenneth Roe wrote:
> 1) parsing support—Input a Coq command or _expression_ and in response,
> Coq returns an xml representation of the parse tree is returned with
> line/column information.  (Is this already present)?

Yes.  It is available via the CoqIDE XML protocol IIRC.  The AST pretty
printer requires some work, possibly it should be rewritten using the modern
ppx technology OCaml provides.  Right now it is written by hand, hence
it lags behind (not all AST nodes are supported).

> 3) Extensions to the asynchronous (PIDE) interface to support multiple
> source files.  Is this already present?

It is not, and Coq itself can hardly do that.  So I'm afraid you'd need
to simulate that on the UI side.

I like your initiative, writing down the requirements of modern IDEs is
a good step forward IMO.

It has not been announced yet, but we are organizing a week long
hackaton (last year was called Coding Sprint) around the end of May or
beginning of June.  It would be nice to have all the user interface guys
and the Coq developers in the same room.

Best,
--
Enrico Tassi