The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I am definitely available for traveling to France at the end of May.  It 
would, however, be nice if some organization in the research community could 
pay for the trip.  Traveling to Europe is expensive and it is unlikely that 
I’ll get money from Johns Hopkins.

                  - Ken

> On 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