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 so we don't need to actually read the session itself but only type in.
This is an important feature of proofgeneral actually (that AFAIK still misses in coqtop, although I did not check recently). One that should be put at medium/high priority in your fork I would say. This can be supported without giving real access to the session though. 2016-05-11 14:24 GMT+02:00 Clément Pit--Claudel <clement....@gmail.com>: > 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 can then. possibly > based on the value of a debug flag, either remove or not that output from the > buffer after processing it. In general you want to remove it, since otherwise > lots of text will be accumulated, but in debug mode you can keep it, à la > comint-mode. > > Clément. > > On 2016-05-11 05:42, Paul A. Steckler wrote: >> 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 >> > > > _______________________________________________ > 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
