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
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
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
>
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
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
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
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
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