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
> 

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

Reply via email to