The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

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.

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.

Here is a brief summary of the requests I have for CoqPIE:

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)?
2) Structured output support—Provide an XML version for Coq goal information 
that is printed after each proof step.  Also provide an XML version of the 
response to each command.  For example, when defining a Fixpoint.  It would 
be nice to have an XML response that can be parsed to determine wether the 
Fixpoint was accepted or if there was an error.
3) Extensions to the asynchronous (PIDE) interface to support multiple source 
files.  Is this already present?  One of the key features of CoqPIE is the 
ability to manage a whole project rather than just individual source files.

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 think that having a detailed design document 
will make it much easier (and much more likely) that the Coq development team 
will implement the enhancements.

                    - Ken