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
<> 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 <>:
>> 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
>>> <> 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 <>:
>>>>> 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 mailing list
>> _______________________________________________
>> ProofGeneral-devel mailing list
> _______________________________________________
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list

Reply via email to