I think Stefan's original suggestion to use pipes saves a bit of work,
because start-process gives you pipes that connect to coqtop's
stdin/stdout. So we could use the pipes for the "main-channel", and
sockets for the OOB stuff.

We're going to have to call start-process in any case to start coqtop.
We can make it a configuration option whether to use sockets for the
main-channel comms.

-- Paul









On Wed, May 11, 2016 at 4:46 PM, Clément Pit--Claudel
<clement....@gmail.com> wrote:
> I think you just want two (well four, with the control channel) 
> `make-network-process'es, actually :)
>
> You can `cl-define-struct' a pair of network process (and possibly wrap 
> relevant function to work on pairs of half-channels) for convenience, too.
>
> Interestingly, you probably don't need a filter function on the two Emacs-> 
> Coq ones.
>
> Clément.
>
> On 2016-05-11 10:09, Paul A. Steckler wrote:
>> 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
>>
>
>
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to