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
> 

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to