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
