Dear all,
Isabelle2011-1 (October 2011) was notable as the release of the first
usable PIDE application: Isabelle/jEdit 1.0 according to retrospective
version numbering. 3 years have passed since then.
Isabelle2014 (August 2014) already has Isabelle/jEdit at version 5.0,
which is the comfortable and powerful Prover IDE that we know today. We
can be also glad to see some alternative PIDE front-ends emerging, namely
Clide and Isabelle/Eclipse.
Since the TTY and PG legacy in Isabelle is a significant burden on the
system architecture, I have started to think about the conseqences of its
removal this spring/summer. Quite some old rubble will get out of the
way, once that is disentangled and garbage-collected from the code base;
important reforms will have a better chance to get through eventually.
Back to the canonical question about "remainig uses of Proof General".
After talking to many people at VSL 2014 Vienna (July 2014) and in the
months afterwards, my conclusion is that nothing is left to hold us back.
So I am leaving a time window of 1-2 weeks, to put forward reasons to
postpone the removal of TTY / Proof General support in Isabelle once more.
If nothing happens, I will start dismantling legacy code before the end of
October 2014.
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
