On 2016-06-11 15:29, Paul A. Steckler wrote:
> On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel 
> <clement....@gmail.com> wrote:
>> 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.
> 
> I'm with you, as long as none of the other provers mind that PG will 
> no longer be available to them.

Great. PG wouldn't stop being available; they would just use the 
latest-released tag. There hasn't been much progress on the generic side for a 
while.

>> If we can, I think it would be good to use it, actually :) What do
>> you mean by leaving CoqIDE in the cold?
> 
> If coqtop works with s-expressions, is the ability to use XML 
> maintained? If so, then CoqIDE can still work as it does. If not,
> then CoqIDE is orphaned, yes? Maybe not a great idea to have coqtop
> support two separate protocols.

Emilio's S-Expressions are built on top of Enrico's Stm, so it isn't really two 
separate parts. Additionally, Emilio's protocol comes as a plugin.

> Or are you suggesting that CoqIDE switch to using s-expressions,
> also?

Emilio is working on that, IIUC.

>> 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.
> 
> Right, if someone wants to stick with 8.5 and have parallelism, they 
> have CoqIDE available for that purpose.
> 
>> 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.
> 
> Sure. I think a shim should be written in OCaml, and it might be
> able to use some of the Coq code for printing that shows up in the
> REPL.
> 
> One decision here is whether to use coqtop's -emacs prompt, or the 
> vanilla prompt. If we could dump the -emacs prompt, that's another 
> desirable (if small) simplification.

Wouldn't that go away from PG anyway? Since PG would only support the XML or 
SEXP protocol.

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