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
