On 15/06/16 23:17, Clément Pit--Claudel wrote:

> It would be useful to hear from current users of PG for proof assistants 
> other than Coq, to see if we could think of a transition plan for them (in 
> particular, if there exists a newer, asynchronous protocol for that proof 
> assistant, it would be good to hear more about it with the hope of supporting 
> is as well once the Coq port is completed).  It would also be useful to hear 
> from users of less-commonly-used features of PG, so that we can make sure 
> that they remain compatible.

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.

One could formally ask on the isabelle-users mailing list, if anybody
wants to join pg-devel for further discussion, although I wouldn't
expect much from it.


        Makarius


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