Some more explanations on the meta-model of this thread:
* We have about 1 week left on isabelle-dev, to discuss whatever might
prevent using Isabelle/jEdit smoothly, and why people fall-back on PG
as a reflex.
* Then there will be Isabelle2014-RC0, as a published release candidate,
but *without* forking the Isabelle repository yet. The same question
and discussion will continue on isabelle-users, for that version, and
as anticipation for Isabelle2014.
* Then there will be VSL 2014 at Vienna, with the Isabelle workshop,
ITP, UITP and more. I am myself around 13..18-Jul-2014 (inclusive
interval). People can show me things personally, to see where the
remaining snags are.
* Then we are heading towards the Isabelle2014 release, with the normal
Isabelle2014-RC1 and *with* forked repository, shortly after the
ITP/UITP week of VSL.
People who are staying themselves longer at VSL and are involved in
the Isabelle2014 lift-off need to keep this in mind: after the fork
changes need to be sent to me, not pushed onto the main Isabelle
repository.
Some time after the release fork, we can look again what the present
answer to the ultimate question is: Are there remaining uses of Proof
General, or is Isabelle2014 the last release that supports it?
(Hopefully not: Is Isabelle2014 the last release ever?)
The Isar TTY loop and its Proof General add-on has become a big burden in
recent years -- both are essentially legacy. So it is worth spending
extra time to deal with this seriously.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
