On 2016-06-15 17:41, Stefan Monnier wrote: >> There might be a tiny minority of Isabelle users who did not follow new >> releases in the last 2 years and are still using Isabelle2014 with Proof >> General. I don't see a problem with that: they just won't be able to >> upgrade Proof General and remain stable on both. > > In an ideal world, the new PG Coq code should make it easier to support > the "new" Isabelle API. It would be good for someone somewhat familiar > with the "new" Isabelle API to keep an eye on the new PG Coq code (or for > those working on the new PG Coq code to take a look at the "new" > Isabelle API).
Thanks Stefan :) I share that hope; I think the new code will be a good basis for such a development. I've looked at a few other protocols over the last year, including the Isabelle protocol/PIDE, Dafny's and F*'s protocols, and some of the stuff that David wrote about PGIP; extending the new code to support these things should be much easier than it would have been previously. Cheers, Clément.
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
