>> 2. Refactor PG to delimit new interfaces, and somehow support both the old
>> REPL mode and the new async mode.
>> 3. Refactor PG to use the new async mode, dropping the REPL and support for
>> old proof assistants on the way.
Actually, I think the best way to do 2 is to first do 3 and then see how
to merge the new and the old.
> 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).
Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
