Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Paul A. Steckler
On Sat, Jun 11, 2016 at 3:59 PM, Clément Pit--Claudel wrote: >> If coqtop works with s-expressions, is the ability to use XML >> maintained? If so, then CoqIDE can still work as it does. If not, >> then CoqIDE is orphaned, yes? Maybe not a great idea to have coqtop >> support two separate protocol

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Clément Pit--Claudel
On 2016-06-11 15:29, Paul A. Steckler wrote: > On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel > wrote: >> My proposal was to dump the entire proof-shell part, indeed. I >> agree with you that it would make everything much easier, and I >> think that would be nice. We'd write a semi-working

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Makarius
On 11/06/16 21:29, Paul A. Steckler wrote: > On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel > wrote: >> My proposal was to dump the entire proof-shell part, indeed. I agree with >> you that it would make everything much easier, and I think that would be >> nice. We'd write a semi-working

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Paul A. Steckler
On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel wrote: > My proposal was to dump the entire proof-shell part, indeed. I agree with you > that it would make everything much easier, and I think that would be nice. > We'd write a semi-working shim to not leave out 8.4 entirely, and drop the

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Clément Pit--Claudel
Hey Paul, On 2016-06-11 15:02, Paul A. Steckler wrote: > I don't think it would be too difficult (although I'm still confused > about some of how the XML protocol works). In some (Pickwickian) > sense, we already have an implementation of that in coqtop itself. > > PG already detects the version

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Paul A. Steckler
I don't think it would be too difficult (although I'm still confused about some of how the XML protocol works). In some (Pickwickian) sense, we already have an implementation of that in coqtop itself. PG already detects the version of coqtop, so it could fire up a shim when needed. Of course, th

Re: [PG-devel] PG and Coq ideslave mode

2016-06-11 Thread Clément Pit--Claudel
Hey Paul, I've been thinking about this. How hard do you think it would be to create an emulation layer that simulates the XML API on top of Coq 8.4? Essentially, how hard would it be to have a program in the middle that translates uses of the 8.5 API to use Coq 8.4's REPL? It wouldn't have to

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Clément Pit--Claudel
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 (th

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Paul A. Steckler
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 obsole

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Clément Pit--Claudel
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 th

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Clément Pit--Claudel
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 w

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Paul A. Steckler
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

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Paul A. Steckler
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,

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Clément Pit--Claudel
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 writ

Re: [PG-devel] PG and Coq ideslave mode

2016-05-07 Thread Clément Pit--Claudel
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

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread Paul A. Steckler
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 `

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread David Aspinall
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 stat

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread Clément Pit--Claudel
On 2016-05-06 09:34, Paul A. Steckler wrote: > 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. That's correct. signature.asc Description: OpenPGP digital signature __

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread Paul A. Steckler
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

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread David Aspinall
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 vol

Re: [PG-devel] PG and Coq ideslave mode

2016-05-06 Thread Paul A. Steckler
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 alre

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Pierre Courtieu
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. Onc

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread 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

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Paul A. Steckler
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 undesir

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Clément Pit--Claudel
On 2016-05-05 10:36, Paul A. Steckler wrote: > So you're suggesting that the abstractions in the generic layer could > be re-implemented. Yup, essentially :) > I wonder if this could done by providing a switch > in the generic layer that says, "use prompts", or "use async > messages", and then u

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Clément Pit--Claudel
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,

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Paul A. Steckler
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

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Paul A. Steckler
Yes, I'm afraid that adding workarounds would be brittle and counter-productive in the long run (as always). If I understand the PG architecture, there's the generic layer that provides core abstractions, plus customizations and instantiations for each prover. The problem I'm facing now is that th

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Clément Pit--Claudel
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--

Re: [PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Clément Pit--Claudel
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

[PG-devel] PG and Coq ideslave mode

2016-05-05 Thread Paul A. Steckler
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 (