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
