The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 23 jun 2004, Sébastien Hinderer wrote:

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


This is also the technique used in Pcoq (which is written in Java by the
way). Can you precise what kind of tool you are realising?

Pierre Courtieu