The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks everyone for the quick and detailed responses. These were really helpful, specially Pierre's examples.

-- Abhishek

On Fri, Jul 5, 2013 at 4:55 PM, t x <txrev319 AT gmail.com> wrote:

Hi Makarius,

  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."

On Fri, Jul 5, 2013 at 4:22 AM, Makarius <makarius AT sketis.net> wrote:

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