I did something like this once to support PGIP, which was a sort of
pre-cursor of PIDE based on exchanging XML messages. You can find the
source in the CVS repo PG Kit repo (Kit/src/pgemacs).  But it probably
isn't useful: it's about 10 years old and the case we wanted to allow
was input coming voluntarily from the prover to PG (think
progress/annotations etc), rather than the other way around.  - David

On 06/05/2016 11:48, Paul A. Steckler wrote:
> Proof General defines a shell mode, proof-shell, and an associated
> message filter. My thought now is to define an alternate-universe
> shell mode, proof-shell-noprompt and an associated message filter.
> 
> -- Paul
> 
> 
> 
> On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu <pierre.court...@cnam.fr> 
> wrote:
>> I am sorry to say that I already asked myself about everything you
>> asked here, and, despite you suggest more smart answers than I did
>> myself I don't see any good enough idea yet. About the prompt: a *lot*
>> of things (everything really) in pg depend on the fact that 1 command
>> = 1 prompt exactly.
>>
>> Once again, don't dismiss starting from scratch without thinking a
>> while about it. Actually large parts of pg could be reused.
>>
>> P.
>>
>>
>> 2016-05-05 19:59 GMT+02:00 Clément Pit--Claudel <clement....@gmail.com>:
>>> I entirely agree with this point; I argued in this direction on a recent 
>>> coq-dev thread.
>>>
>>> On 2016-05-05 12:24, Paul A. Steckler wrote:
>>>> I'm not a fan of this idea. The IDE and the prover should be only
>>>> loosely-coupled, with a clearly-defined communication protocol between
>>>> them.
>>>>
>>>> A plugin introduces a tight coupling between these components. Yes,
>>>> it's only a plugin, so the scope of the coupling is limited. But it
>>>> still seems undesirable to me.
>>>>
>>>> -- Paul
>>>>
>>>> On Thu, May 5, 2016 at 4:58 PM, Clément Pit--Claudel
>>>> <clement....@gmail.com> wrote:
>>>>> Not entirely clear to me :) I think there'd be some amount of design work 
>>>>> there as well.
>>>>>
>>>>> On 2016-05-05 10:39, Paul A. Steckler wrote:
>>>>>> With that toploop plugin installed on the coqtop side installed, what
>>>>>> does Proof General see from its shell?
>>>>>>
>>>>>> -- Paul
>>>>>>
>>>>>> On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel
>>>>>> <clement....@gmail.com> wrote:
>>>>>>> Hi Paul,
>>>>>>>
>>>>>>> Here's another approach that I forgot to mention: we could build a 
>>>>>>> separate Emacs toploop as a plugin, which would inherit most of 
>>>>>>> CoqIDE's toploop (you know that I have mixed feelings about that, but 
>>>>>>> it may be the most pragmatic approach).
>>>>>>>
>>>>>>> Clément.
>>>>>>>
>>>>>>> On 2016-05-05 10:17, Clément Pit--Claudel wrote:
>>>>>>>> Hi Paul,
>>>>>>>>
>>>>>>>> You could indeed modify PG to handle the first prompt differently, or 
>>>>>>>> even Coq.
>>>>>>>> In the long run, though, I don't think the approach is sustainable. PG 
>>>>>>>> is very much hardcoded to expect one prompt for every query it sends: 
>>>>>>>> thus, even though you may get something working pretty quickly by 
>>>>>>>> hacking around this prompt thing, I think we'll see more breakages 
>>>>>>>> with every evolution of the new protocol.
>>>>>>>>
>>>>>>>> Here's a slightly different idea. Right now, PG adds an abstraction 
>>>>>>>> layer on top of a REPL model. What you could do is reimplement the 
>>>>>>>> same abstraction, but on top of Coq's new asynchronous model. 
>>>>>>>> Concretely, my suggestion is to make a separate library to talk to 
>>>>>>>> Coq's new API, which would provide the same interface 
>>>>>>>> (proof-shell-invisible-command, proof-shell-ready-prover, 
>>>>>>>> proof-shell-invisible-cmd-get-result, etc.).
>>>>>>>>
>>>>>>>> I think this would make your life easier. You would:
>>>>>>>>
>>>>>>>> 1. Identify a small (hopefully) collection of functions that 
>>>>>>>> Coq-ProofGeneral actually depends on (some sort of semi-explicit 
>>>>>>>> interface, essentially).
>>>>>>>> 2. Implement support for these functions using Coq's new API model
>>>>>>>> 3. Modify the current implementation to call these functions or the 
>>>>>>>> legacy ones depending on the version of Coq.
>>>>>>>>
>>>>>>>> What do you think?
>>>>>>>> Clément.
>>>>>>>>
>>>>>>>> On 2016-05-05 09:48, Paul A. Steckler wrote:
>>>>>>>>> I've already mentioned the issue described below to Clément 
>>>>>>>>> Pit-Claudel
>>>>>>>>> and Pierre Courtieu, maybe others on this list have thoughts on it.
>>>>>>>>>
>>>>>>>>> Proof General is welded to a model of receiving prompts from a prover.
>>>>>>>>> After it's received a prompt, PG can send something back to the
>>>>>>>>> prover.
>>>>>>>>>
>>>>>>>>> The ideslave (politically incorrectly-named) mode in Coq, developed
>>>>>>>>> for CoqIDE abandons that model. In that mode, Coq just waits for XML
>>>>>>>>> from an IDE, without first offering a prompt.
>>>>>>>>>
>>>>>>>>> In ideslave mode, it seems that Coq sends back responses wrapped in
>>>>>>>>> <value> tags, so you can use that as a pseudo-prompt. Hmm, I think the
>>>>>>>>> prompt regexp would have to look for both the closing tag, and the
>>>>>>>>> single-tag version, <value ... />.
>>>>>>>>>
>>>>>>>>> Even with that, there's still a bootstrapping issue, because there's
>>>>>>>>> no prompt to s start with. I could probably modify PG to not look for
>>>>>>>>> that first prompt.
>>>>>>>>>
>>>>>>>>> Is there some good way to handle this?
>>>>>>>>>
>>>>>>>>> -- 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
> 

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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

Reply via email to