OK, you'll need to explain the binding between plug-ins and PG to me. -- Paul
On Sat, May 7, 2016 at 3:38 PM, Clément Pit--Claudel <clement....@gmail.com> wrote: > 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 >> > > > _______________________________________________ > 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
