Additionally, it would be nice to remain compatible with plugins :) On 2016-05-07 09:33, Clément Pit--Claudel wrote: > 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 >> > > > > _______________________________________________ > 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
