The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Fri, 5 Jul 2013, t x wrote:

> What is required to merge these changes into the main Coq branch? I had 
> stumbled across this project earlier, wanted to use it, but did not want 
> to be forced to choose between "being able to use Pide" vs "being able 
> to have new Coq bug fixes / features."

I do not understand the Coq development process, so I can't tell.  Maybe 
some of the French colleagues can explain this (who are also collaborating 
in a joint project).

Technically, CoqPIDE is doing the main (generic) protocol connectivity, 
and demonstrates it by some toy protocol functions for CoqIde-style syntax 
highlighting.  This was reasonably easy to do with minor changes on Coq 
8.4 sources.  Anybody experimenting with further functionality could start 
by making local patches that are re-adjusted everytime Coq changes, using 
one of its git clones.

I have seen this technique of following upstream changes systematically in 
the Eclipse front-end for PIDE, which was done by Andrius Velykis (see 
also https://github.com/andriusvelykis). Note that is for alternative PIDE 
front-ends, not prover back-ends.


The basic CoqPIDE connectivity layer merely liberates the prover from old 
problems of TTY-style communication of plain text via stdin/stdout/stderr, 
and avoids common mistakes in using XML naively. Substantial work would be 
required to improve the Coq back-end to support actual document-oriented 
interaction, as required for a realistic Prover IDE.

I would like to encourage that nonetheless: it greatly helps to open up 
arcane interactive provers towards a wider audience.  (Although users of 
vi or emacs actually like arcane things.)


        Makarius