The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

> On Jan 28, 2016, at 11:23 PM, Clément Pit--Claudel 
> <clement.pit AT gmail.com>
>  wrote:
> 
> Hi Ken,
> 
> On 01/28/2016 10:01 PM, Kenneth Roe wrote:
>> On Jan 24th, I gave a demo of my CoqPIE UI to a group of people many
>> of whom were also developing IDEs for Coq.  Out of the discussions,
>> we concluded that it would be good to put together a unified list of
>> enhancements.  Present in the group were Jesper Bengston, Greg
>> Malecha, Clément Pit—Claudel, (Valentin Robert?), and briefly, Andrew
>> Appel.  Is there anyone else I forgot?  We had representatives from
>> four major IDE efforts, CoqPIE, Company Coq, Peacoq and Coqoon.
> 
> Company-Coq is not an IDE ;) Proof General is, but I hardly count as a 
> representative for it :)
> Valentin wasn't there, but a few others joined this discussion. Anyhow, 
> regardless of who was there on that day, I'd be happy to get feedback from 
> anyone. 
> 
I should probably say “IDE enhancement efforts” rather than IDEs.  Coqoon by 
the way is built on top of Eclipse and is not really an IDE on its own.

>> My suggestion is that as a community, we create a detailed design
>> document of all the enhancements requested to better support the
>> various IDEs.  Each UI had its own unique set of features and will
>> likely require different enhancements.
> 
> That doesn't sound too good:
> 
> * Each IDE having its own unique set of features isn't good; if we want to 
> make it easy for users to switch editors, we should strive for feature 
> parity.
> * Coq devs are already very busy with other requests (performance is a big 
> one); we can't afford to ask them for different enhancements for each 
> editor. Instead, we should identify a small, consistent interface that we'd 
> like Coq to expose so that we can all build upon it. And we should also 
> consider re-using existing community efforts, such as Valentin's excellent 
> plugin or the great work that the PIDE people have done (Coqoon uses that, 
> and it looks very good)
> 
My intent is to come up with one unified spec document with everything that 
is needed.  Each enhancement effort has its own unique set of features.  
However, we should start by writing up the features that would be useful for 
our own efforts and then merge them into a unified document.  I also would 
like to see a few iterations of reviews of the unified spec.  This will make 
things much easier for the developers.  They will have a document describing 
exactly what needs to be implemented and will reduce the number of iterations 
at implementation time.

>> (...)
>> In about a week or two, I plan to write up and post to this group a
>> more detailed specification document.  I hope people involved with
>> other IDE projects can do the same.
> 
> I'm not sure whether every IDE developer coming up with a different spec is 
> a good thing :) And in fact, I'm not even sure whether we really know what 
> we want to be asking Coq developers for (a full new API? A bunch of extra 
> commands? New ways to talk to Coq?). In fact, I don't have enough 
> experience even with the new Coq XML protocol to know what it can and 
> cannot do, so I'm not necessarily in a good position to design such a 
> specification document. 
> 
The ideal thing would be to use as much of the existing APIs.  We should try 
and minimize the number of requests being made.  However, we should make sure 
that enhancements are requested to fully support all the features being 
developed in all of the IDE efforts.

> As a side note, we should probably move this discussion to coqdev, as it 
> mostly focuses on Coq's development.
> 
> Cheers,
> Clément.
> 

                       - Ken