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
> 

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