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

Reply via email to