Hi Paul, I don't think we should give it a different name yet; I think it would create a lot of confusion.
We can phrase this differently: what you are currently writing is a library that implements the protocol spoken by Coq. Ideally, we would be able to plug that library straight into proof general. Unfortunately, that isn't the case today. So, we'll have to modify PG. That's fine :) One particular strong point of proof general is its ability to talk to multiple versions of Coq. A full fork would be problematic, because it would loose this ability. Regarding the other part (coqserver), I think a coqdev thread would be more appropriate. Clément. On 2016-05-07 02:48, Paul A. Steckler wrote: > After hacking on PG all yesterday, and working out how to dispatch > between two shell modes, I think a forked, Coq-only version is the > better solution. Name suggestions? :-) > > At the other end, I think that there should be a separate binary for > the XML (or whatever it turns out to be) protocol, say `coqserver'. > It's operating in a different way than coqtop-as-a-REPL. That would be > simplify the codebase for coqtop. Although I haven't yet dealt with > the extra channels that the toploop-coqide mode gives, I'm still > liking the idea of using HTTP and a REST API as the basic > communication mechanism. > > -- Paul > > > On Fri, May 6, 2016 at 3:51 PM, David Aspinall <david.aspin...@ed.ac.uk> > wrote: >> That sounds right (but could lead to confusion!). What I did was to fork a >> version of PG and cut it down to something fairly minimal. - D. >> >> >> On 06/05/2016 14:34, Paul A. Steckler wrote: >>> >>> The proof-shell mode comes with a lot of associated state, like >>> regexps, buffers, etc. Some bits of that state would be useful in the >>> new mode I'm creating, others not. >>> >>> I'm thinking that I can share the same state variables for the new >>> mode, because I'll never have an active proof shell mode and the new >>> mode active at the same time. Yes? >>> I'd hate to have to duplicate state. >>> >>> If I load two .v files in emacs, it seems I can only work on one at a >>> time using Proof General, and there's only one proof-shell mode window >>> active. >>> >>> -- Paul >>> >>> >>> On Fri, May 6, 2016 at 3:15 PM, David Aspinall <david.aspin...@ed.ac.uk> >>> wrote: >>>> >>>> I did something like this once to support PGIP, which was a sort of >>>> pre-cursor of PIDE based on exchanging XML messages. You can find the >>>> source in the CVS repo PG Kit repo (Kit/src/pgemacs). But it probably >>>> isn't useful: it's about 10 years old and the case we wanted to allow >>>> was input coming voluntarily from the prover to PG (think >>>> progress/annotations etc), rather than the other way around. - David >>>> >>>> On 06/05/2016 11:48, Paul A. Steckler wrote: >>>>> >>>>> 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 >>>>> >>>> >>>> -- >>>> The University of Edinburgh is a charitable body, registered in >>>> Scotland, with registration number SC005336. >>>> >>>> _______________________________________________ >>>> ProofGeneral-devel mailing list >>>> ProofGeneral-devel@inf.ed.ac.uk >>>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >>> >>> >> >> -- >> The University of Edinburgh is a charitable body, registered in >> Scotland, with registration number SC005336. >> > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
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
