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 <monn...@iro.umontreal.ca> 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 ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
