Re: [PG-devel] PG and Coq ideslave mode
On 2016-05-07 14:37, Paul A. Steckler wrote: > On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel > wrote: >> I'm all for a cleanup of the PG codebase, of course. But I think we can do >> it slightly differently: starting with the current code, we can: >> >> * Tag a last-known good version (the current HEAD) for obsolete provers >> * Remove obsolete provers >> * Rename the "generic/" folder to "REPL/" >> * Ensure that the separation between the "coq/" subfolder and the "generic/" >> subfolder is clean; that is, check which functions in "generic/" the "coq/" >> part calls (this is our "implicit API"), and ensure that nothing on the >> "coq/" side depends on the REPL model; anything that does is probably a >> mistake. > > Yes, there is some code there that depends on the REPL model. See, for > example, coq-last-prompt-info in coq/coq.el. I see, thanks. Although for this particular example, it's mostly last-prompt-info not having an ideal name; in a sense, this is just a function that returns the current state of the proof (how many proofs are currently pending, etc). >> It other words, my claim is that as part of a hypothetical fork we would >> already have to clean up the "coq/" subdirectory. Once this is done, it >> should be relatively easy to have support for both the REPL and the XML >> model in the same codebase. My hunch is that a very significant majority of >> the "coq/" subfolder does not depend on PG internals, since it uses clean >> interface functions to ask questions to the prover. > > A lot of the code in there uses regexps to work out what the prover > has sent, which is not so clean, IMHO. Just a thought, it might be > better if that information was explicit in the XML, by using > particular tags or attributes to flag items of interest. We could > abstract over these approaches, and use regexp-matching for the REPL > approach, and XML parsing in the other approach. That would give a > clean, representation independent interface. The current XML > essentially just wraps the textual output, and so we'd still use > regexp-matching for now. That would be great, and I think your last point is the key. We can just strip the XML code from responses for now. > I think the approach you've outline is do-able, but again, I do have > concerns about the complexity that it brings. Anything that brings in complexity only for backwards compatibility we should avoid. However, if ensuring some level of backwards compatibility helps us reduce our technical debt, then that's good :) Ideally, we'd end up with multiple mostly-independent components: a tree-window display layer with text spans, a generic driver layer that implements basic UI functionality (moving around, etc), an implementation of the Coq API, and coq-specific package that implements syntax highlighting, indentation, and other Coq-only things. Concretely, this won't happen all at once, of course. Cheers, Clément. 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
Re: [PG-devel] PG and Coq ideslave mode
On Sat, May 7, 2016 at 8:05 PM, Clément Pit--Claudel wrote: > I'm all for a cleanup of the PG codebase, of course. But I think we can do it > slightly differently: starting with the current code, we can: > > * Tag a last-known good version (the current HEAD) for obsolete provers > * Remove obsolete provers > * Rename the "generic/" folder to "REPL/" > * Ensure that the separation between the "coq/" subfolder and the "generic/" > subfolder is clean; that is, check which functions in "generic/" the "coq/" > part calls (this is our "implicit API"), and ensure that nothing on the > "coq/" side depends on the REPL model; anything that does is probably a > mistake. Yes, there is some code there that depends on the REPL model. See, for example, coq-last-prompt-info in coq/coq.el. > It other words, my claim is that as part of a hypothetical fork we would > already have to clean up the "coq/" subdirectory. Once this is done, it > should be relatively easy to have support for both the REPL and the XML model > in the same codebase. My hunch is that a very significant majority of the > "coq/" subfolder does not depend on PG internals, since it uses clean > interface functions to ask questions to the prover. A lot of the code in there uses regexps to work out what the prover has sent, which is not so clean, IMHO. Just a thought, it might be better if that information was explicit in the XML, by using particular tags or attributes to flag items of interest. We could abstract over these approaches, and use regexp-matching for the REPL approach, and XML parsing in the other approach. That would give a clean, representation independent interface. The current XML essentially just wraps the textual output, and so we'd still use regexp-matching for now. I think the approach you've outline is do-able, but again, I do have concerns about the complexity that it brings. There may still be a generic directory, for PG-wide features that are independent of the REPL approach. -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] PG and Coq ideslave mode
On 2016-05-07 13:44, Paul A. Steckler wrote: > OK, you'll need to explain the binding between plug-ins and PG to me. I think this connects to my previous email. Company-coq uses PG as an interface to Coq (thus very little in it depends on how PG communicates with Coq, and I could fix anything that does: it only depends on the interface that PG exposes). In terms of functions, the only ones that it uses from PG itself are these: (fun proof-shell-invisible-command "ext:proof-shell.el" cmd) (fun proof-shell-available-p "ext:proof-shell.el") (fun proof-shell-live-buffer "ext:proof-shell.el") (fun proof-shell-ready-prover "ext:proof-shell.el") (fun proof-unprocessed-begin "ext:proof-script.el") (fun proof-goto-point "ext:pg-user.el") 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
Re: [PG-devel] PG and Coq ideslave mode
On 2016-05-07 13:44, Paul A. Steckler wrote: > Well, we're asking Proof General to work in a fundamentally > different way than it has so far. Adding support for the XML mode > significantly increases the complexity of the software, and that mode > would not be used by other provers. Imagine that we fork PG, remove > its prompt mode stuff, and we strip out the legacy support for the > -emacs mode in Coq. I think this is a good plan in the long run. However, most of the complexity in the Coq part of proof-general is protocol-agnostic; ideally, I don't want to be fixing bugs in two separate copies of that code. In addition, being able to update people in place is a significant win for us, given the current installation medium (git clones). > (...) If someone is using an old version of Coq, the old versions of > PG are still available, of course. The problem here is that switching between both versions is going to be unpleasant at best, and that we'll make the lives of people porting 8.4 software to 8.5 much more painful. I'm all for a cleanup of the PG codebase, of course. But I think we can do it slightly differently: starting with the current code, we can: * Tag a last-known good version (the current HEAD) for obsolete provers * Remove obsolete provers * Rename the "generic/" folder to "REPL/" * Ensure that the separation between the "coq/" subfolder and the "generic/" subfolder is clean; that is, check which functions in "generic/" the "coq/" part calls (this is our "implicit API"), and ensure that nothing on the "coq/" side depends on the REPL model; anything that does is probably a mistake. * Create an "XML/" folder and implement support for the new Coq API there, implementing the implicit API that we identified on the previous step. * Make sure that the "coq/" folder loads one or the other depending on the version of Coq that it is being used with. It other words, my claim is that as part of a hypothetical fork we would already have to clean up the "coq/" subdirectory. Once this is done, it should be relatively easy to have support for both the REPL and the XML model in the same codebase. My hunch is that a very significant majority of the "coq/" subfolder does not depend on PG internals, since it uses clean interface functions to ask questions to the prover. What do you think? 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
Re: [PG-devel] PG and Coq ideslave mode
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 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 >>> 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 > 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 >>> 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 : > > 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 >> wrote: >>> >>> Not entirely clear to me :) I think there'd be some amount of design >>> work there as well. >>
Re: [PG-devel] PG and Coq ideslave mode
On Sat, May 7, 2016 at 3:33 PM, Clément Pit--Claudel wrote: > 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. Well, we're asking Proof General to work in a fundamentally different way than it has so far. Adding support for the XML mode significantly increases the complexity of the software, and that mode would not be used by other provers. Imagine that we fork PG, remove its prompt mode stuff, and we strip out the legacy support for the -emacs mode in Coq. Then we have simpler code at both ends. I'm told that PG become de facto Coq-only, so if Coq commits to XML, there's little reason to support the prompt mode in PG for the sake of other provers. If someone is using an old version of Coq, the old versions of PG are still available, of course. I see your points, of course. > Regarding the other part (coqserver), I think a coqdev thread would be more > appropriate. Yes, just musing out loud on related topics. -- Paul ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] PG and Coq ideslave mode
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 >> 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 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 >> 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 >>> : 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 > 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
Re: [PG-devel] PG and Coq ideslave mode
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 > 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 >>> 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 > 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 >> : >>> >>> 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 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 >> wrote: >>> >>> Hi Paul, >>> >>> Here's another approach that I forgot to mention: we could build a >>> separate Emacs toploop as a plugin, wh
