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.

Attachment: 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

Reply via email to