Hey Paul,

On 2016-06-11 15:02, Paul A. Steckler wrote:
> I don't think it would be too difficult (although I'm still confused
> about some of how the XML protocol works).  In some (Pickwickian)
> sense, we already have an implementation of that in coqtop itself.
>
> PG already detects the version of coqtop, so it could fire up a shim
> when needed.

Yup, I wrote that code :)

> Of course, this approach increases system complexity, and substitutes
> new code for code known to work adequately.
> 
> OTOH, such a project would allow us to remove the proof shell code
> specifically for Coq in PG. Then the question would become whether to
> keep any of the generic proof shell code around for other provers. I
> just looked into Lean, which appears to hijack emacs in its own way,
> so probably there isn't interest in using PG w/ Lean.
> 
> If the decision is to dump the proof shell entirely, PG becomes much simpler.

My proposal was to dump the entire proof-shell part, indeed. I agree with you 
that it would make everything much easier, and I think that would be nice. We'd 
write a semi-working shim to not leave out 8.4 entirely, and drop the generic 
aspects. It would probably make your/our lives simpler, at no significant loss, 
I think.

> Then there's the question of how Emilio's new s-expression protocol
> fits in the picture. Embracing that would fit well with PG, and
> s-expressions are warmer/fuzzier than XML, but doing so might leave
> CoqIDE out in the cold, and also require an s-expression to XML shim
> for 8.5 and 8.6. So probably a non-starter.

If we can, I think it would be good to use it, actually :) What do you mean by 
leaving CoqIDE in the cold?
Also, if we have an S-expression to REPL shim, we can use it with 8.5 as well, 
and only get fancy (parallelism and all that) in 8.6, or whatever comes next.

Maybe we should discuss this at the meeting on Tuesday. In the meantime, I can 
run a small experiment with Emilio's code, if you want.

Clément.

> On Sat, Jun 11, 2016 at 12:48 PM, Clément Pit--Claudel
> <clement....@gmail.com> wrote:
>> 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
>>>
>>
>>
>> _______________________________________________
>> 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