The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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. 

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

> (...)
> 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. 

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

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature