You're comparing make-network-process, then, with start-process?

When using sockets, coqtop works in a funny way, using two half-duplex
sockets. So if you used make-network-process, I think you'd get just
one of those sockets, and have to use Elisp's other network facilities
to manage the other socket, ugh. That reinforces the idea that pipes
would be the way to go.

There are also the "command channels" used by coqtop. I think those
would have to be manually-managed network sockets.

-- Paul



On Wed, May 11, 2016 at 3:40 PM, Stefan Monnier
<monn...@iro.umontreal.ca> wrote:
>> You mean here the pipes that are created when running Elisp's start-process?
>
> Yes.  In either case, the Elisp code will start Coq and get a an Elisp
> process object in return.  This is the only part that should
> be different.  After that, whether you're using a pipe or a socket won't
> affect your Elisp code.
>
>> It looks like you'd setup a filter function for the Coq process to get
>> its output, and use process-send-string to send input to Coq.
>
> Yes, and that applies to either case.
>
>
>         Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to