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