Yes, I'm afraid that adding workarounds would be brittle and
counter-productive in the long run (as always).

If I understand the PG architecture, there's the generic layer that
provides core abstractions, plus customizations and instantiations for
each prover. The problem I'm facing now is that the implementation of
the abstractions in the generic layer make assumptions that don't hold
for Coq in ideslave mode.

So you're suggesting that the abstractions in the generic layer could
be re-implemented. I wonder if this could done by providing a switch
in the generic layer that says, "use prompts", or "use async
messages", and then using the appropriate implementation. Maybe that's
too optimistic. It might be that the abstractions in the generic layer
just aren't a good fit for async messages, but I don't yet have a
sense of that one way or the other.

In any case, just getting the ideslave stuff to work is a bigger job
than I first thought, without even considering background processing.

-- Paul


On Thu, May 5, 2016 at 4:17 PM, Clément Pit--Claudel
<clement....@gmail.com> 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
>> ProofGeneral-devel@inf.ed.ac.uk
>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>>
>
>
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to