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

Reply via email to