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

Reply via email to