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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
