On Sat, Jun 11, 2016 at 3:12 PM, Clément Pit--Claudel <[email protected]> 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
