Re: [PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

Maybe that mode could be reproduced using a separate buffer that takes user input, which gets wrapped in XML and sent to coqtop. -- Paul On Wed, May 11, 2016 at 3:14 PM, Pierre Courtieu wrote: > Another use of a direct access to the coq session in pg is when using >

Re: [PG-devel] Using sockets instead of shell

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

Re: [PG-devel] Using sockets instead of shell

Another use of a direct access to the coq session in pg is when using "Debug On" mode for Ltac debugging. In this mode we need to issue commands directly into the session mostly like with gdb (return, f, etc). With current pg the debugging info is then dispatched in *goals* and *response* buffers

Re: [PG-devel] Using sockets instead of shell

Hey Paul, I don't think it will make much of a difference, so you should feel free to go for sockets. They are very similar to processes in Emacs, so in practice you'll do essentially the same, namely accumulate the output that you get from Coq into a buffer until you have a full message. You

Re: [PG-devel] Using sockets instead of shell

Elisp has primitives for network reading and writing, so the actual Emacs mode where code runs can be anything. Yes, I had meant to mention a logging facility. There could be a dedicated buffer showing the traffic, or a simplified version of it could be sent to *Messages*. -- Paul On Wed, May

[PG-devel] Using sockets instead of shell

Per the earlier discussion here, I'm developing a branch (not fork) of PG that operates in two ways, either the old REPL way where the prover offers a prompt, and a new server way, where PG and the prover exchange messages. I'm being coy about whether PG or the prover is the server, due to