The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi Abhishek,

While waiting for some more in-depth answer to your question, you can check the Eclipse plugin:

http://provereditor.gforge.inria.fr/

Best,

Beta

On Thu, Jul 4, 2013 at 5:10 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Hi,

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?

So far, I did some reverse engineering and found out:

(please correct me if I am wrong)

1) Coqtop prints "coq<" on stderr when ready to accept an input. I guess I need to wait until prints "coq < " on stderr before writing to coq's inputstream.

2) If coqtop didn't like the previous command, the last line is of the form "error ...". 

   So, while sending the contents of user's editor window to coqtop, I need to stop as soon

   as I encounter one of these and prompt the user about the error.

I need more information so that I can reliably parse coqtop's output, especially proof state and present them to the user in a more intuitive way. I can try to reverse engineering most of these, but would appreciate if some description of a protocol that coqtop follows is available somewhere.

Some brief description of how CoqIDE works might also be useful.

Thanks,

-- Abhishek

https://github.com/aa755/nbcoq