On 15/06/16 23: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).
I have tried to activate people still interested in Emacs over many
years, in order to take a look what is going on in Isabelle/PIDE. I
don't think anybody will suddenly show up, although one could give such
a hypothetical person a last chance by posting on isabelle-users.
Concerning the "new" prover APIs of Coq and Isabelle in general: I was
in contact with Enrico Tassi when he introduced this for Coq -- it was
part of our Paral-ITP project at that time. My general impression is
that the new Coq API is more conservative than the PIDE protocol of
Isabelle: PIDE is quite demanding on the other side to process a lot of
information in real-time.
This is actually the deeper reason, why I gave up the single-threaded
LISP machine of Emacs in 2007 and moved towards the multi-threaded JVM,
even though the JVM is a bit ugly.
BTW, I complained about the "master / slave" terminology of the new Coq
protocol when Enrico introduced that in 2012/2013, not for P.C. reasons
but for technological ones. In PIDE, the front-end and back-end are
peers that continuously exchange a lot of information in both directions.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
