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