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 11, 2016 at 11:32 AM, Pierre Courtieu <pierre.court...@cnam.fr> wrote: > 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't know. > > P. > > > 2016-05-11 11:11 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>: >> 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 >> community. >> >> 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 >> the prover. >> >> 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? >> >> -- Paul >> _______________________________________________ >> 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
