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
>>>
>>
> 

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