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.

> 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.

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

> 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.

-- Paul
ProofGeneral-devel mailing list

Reply via email to