You mean here the pipes that are created when running Elisp's start-process?

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.

I guess that's as easy as, or easier than sending data over sockets.

Yes, I'd like to avoid the complexity of a comint-like mode, and have
only one process shell mechanism in PG.

-- Paul

On Wed, May 11, 2016 at 2:39 PM, Stefan Monnier
<> wrote:
>> For the new server way of working, it's possible to do something
>> similar for Coq, because coqtop can work with stdin and stdout using
>> the -main-channels argument. But maybe that's not a great way to go.
>> First, it's not likely that users will want to interact with the
>> prover in a shell, because it's too hard to use the XML syntax
>> manually. Second, the shell mode is fairly complex, in ways that maybe
>> we can avoid.
>> As an alternative, you can give coqtop's -main-channels argument port
>> options, that allow it to communicate over sockets. On the PG side,
> AFAICT the choice between stdin/out and sockets is actually independent
> from whether we make the resulting communication available to the user
> with some kind of comint-ish mode.
> IOW there are 2 questions:
> - use a socket or use a pipe?
> - use a comint-ish mode or not?
> My instinct tells me using a pipe will make the code slightly simpler.
> And it also tells me that using a comint-ish mode is not worth the hassle.
>         Stefan
ProofGeneral-devel mailing list

Reply via email to