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
