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

Reply via email to