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
