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.


Attachment: signature.asc
Description: OpenPGP digital signature

ProofGeneral-devel mailing list

Reply via email to