The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Hello,

One solution I see is to have two processes: one for your interface, the
other for Coq.
The idea is that the coq process is executed by your interface (with th fork
and exec system calls).
The communication is then done using two pipes. One allows the interface to
send datas to Coq on his standard input, the other one is used to fetch
messages sent by Coq on his standard output.

I guess this is the technique use by Emacs and proof-general...

Hope this helps,
Sébastien.