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
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?
ProofGeneral-devel mailing list