The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Thu, 4 Jul 2013, Abhishek Anand wrote:

> I'm trying to develop a Coq plugin for my fav. IDE(https://netbeans.org/)
> as a hobby project.
> The plugin needs programmatically talk to coqtop.
> Is there some description of a "protocol" one should follow while
> programmatically talking to coqtop?

Here is a report of an experiment of mine from last year:

  PIDE as front-end technology for Coq
  http://arxiv.org/abs/1304.6626

It explains how to avoid many well-known problems of prover connectivity 
stemming from old-fashioned TTY communication, even problems that are 
newly introduced by adding XML to it.  Instead, the prover itself is 
augmented by some OCaml code for more direct document-oriented 
interaction.  This allows Coq to connect to Scala, and thus anything else 
that runs on the JVM (not for free, but with some reasonable extra work).

The experiment shows how easy it is to apply these techniques to Coq -- 
they are used in production elsewhere for some years already.

Of course, I am not in a position to maintain any Coq-specific things. It 
is merely meant as an incentive for the prover guys to standardize on 
simple and clear interaction beyond the TTY loop and its complications.


        Makarius