Maybe that mode could be reproduced using a separate buffer that takes user input, which gets wrapped in XML and sent to coqtop.
-- Paul On Wed, May 11, 2016 at 3:14 PM, Pierre Courtieu <pierre.court...@cnam.fr> wrote: > 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 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
