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 differen
Hi Paul,
AFAICT this seems a good way to go. Does scomint support the read and
write on sockets?
The ability to "see" the coq session is very helpful for debugging and
maybe you should try to replace it by something else. Like a Logging
buffer where xml noise is removed as much as possible. I don
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 1
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 c
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 s
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
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
> "Debug On" mode for Ltac debu
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 so
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 filte
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
10 matches
Mail list logo
