Hi Paul, Here's another approach that I forgot to mention: we could build a separate Emacs toploop as a plugin, which would inherit most of CoqIDE's toploop (you know that I have mixed feelings about that, but it may be the most pragmatic approach).
Clément. On 2016-05-05 10:17, Clément Pit--Claudel wrote: > Hi Paul, > > You could indeed modify PG to handle the first prompt differently, or even > Coq. > In the long run, though, I don't think the approach is sustainable. PG is > very much hardcoded to expect one prompt for every query it sends: thus, even > though you may get something working pretty quickly by hacking around this > prompt thing, I think we'll see more breakages with every evolution of the > new protocol. > > Here's a slightly different idea. Right now, PG adds an abstraction layer on > top of a REPL model. What you could do is reimplement the same abstraction, > but on top of Coq's new asynchronous model. Concretely, my suggestion is to > make a separate library to talk to Coq's new API, which would provide the > same interface (proof-shell-invisible-command, proof-shell-ready-prover, > proof-shell-invisible-cmd-get-result, etc.). > > I think this would make your life easier. You would: > > 1. Identify a small (hopefully) collection of functions that Coq-ProofGeneral > actually depends on (some sort of semi-explicit interface, essentially). > 2. Implement support for these functions using Coq's new API model > 3. Modify the current implementation to call these functions or the legacy > ones depending on the version of Coq. > > What do you think? > 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 >> > > > > _______________________________________________ > 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
