The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Building on the request for parsing support, one issue that I've had, in writing my bug-minimizer, is that it's generally not clear when Coq is waiting for more input and when Coq is busy computing on the input I've given it.  Having a way to get Coq to tell me what the boundaries of expressions/commands are would be useful.  (In newer Coqs, I use `coqc -time` to get this.)

-Jason

On Thu, Jan 28, 2016 at 10:01 PM, Kenneth Roe <kendroe AT hotmail.com> 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.

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