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
