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
On Wed, May 11, 2016 at 4:46 PM, Clément Pit--Claudel
> 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.
> 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
>>> 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.
>> ProofGeneral-devel mailing list
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list