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, this approach increases system complexity, and substitutes new code for code known to work adequately. OTOH, such a project would allow us to remove the proof shell code specifically for Coq in PG. Then the question would become whether to keep any of the generic proof shell code around for other provers. I just looked into Lean, which appears to hijack emacs in its own way, so probably there isn't interest in using PG w/ Lean. If the decision is to dump the proof shell entirely, PG becomes much simpler. Then there's the question of how Emilio's new s-expression protocol fits in the picture. Embracing that would fit well with PG, and s-expressions are warmer/fuzzier than XML, but doing so might leave CoqIDE out in the cold, and also require an s-expression to XML shim for 8.5 and 8.6. So probably a non-starter. -- Paul On Sat, Jun 11, 2016 at 12:48 PM, Clément Pit--Claudel <clement....@gmail.com> wrote: > 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 > replicate all of the functionality, of course; just a small subset of it > would probably be fine. > > This could allow for a more radical paradigm shift inside of PG: instead of > maintaining two code paths, one with and one without support for 8.5, we'd > have just one, with an extra compatibility layer inserted between PG and Coq > when using 8.4. > > Cheers, > 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
