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

Reply via email to