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

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

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

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

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.

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

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.

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

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 >>

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

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