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 difference of opinion on that score in the Coq
When operating using a REPL, communication with the prover uses an
Emacs mode derived from PG's scomint mode, which is a simplified
version of the Emacs-standard comint mode. The original comint mode
was designed for interactive use, such as when running an interpreter.
Having a similar mode for PG makes sense, because provers have
historically worked in a similar way, taking input via stdin and
printing output on stdout. When running Coq via PG, I can even open
the *coq* buffer that uses its shell mode and interact directly with
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,
instead of using a shell mode, we'd run Elisp code that would read and
write over the sockets. After it's read something, the XML would be
interpreted, calling other code when needed (writing out a response or
goal, for example). There would still need to be code that's
currently done by the shell mode, such as firing up the prover, and
maybe some of the non-prompt-related regexp matching.
Does a socket-based approach make sense? What am I losing if I don't
use a shell mode?
ProofGeneral-devel mailing list