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.
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneralfirstname.lastname@example.org http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel