Am 16.12.2013 16:52, schrieb Makarius: > On Sun, 15 Dec 2013, Christian Urban wrote: > >> My guess is that I notice this message already for at least a year. It >> is in fact so frequent that I assumed this is normal behaviour of >> Isabelle. > > So just one more thing on the long list of open problems that nobody > dared to report or cared about. > > The big problem of Isabelle2013-1 was a lack of serious testing towards > a truly stable release, but I misinterpreted the lack of problem reports > as absence of problems. Isabelle2013-2 is a bit better, but not really > there -- right *after* the release I've got again further observations > about certain oddities that were already there at the start of the RC > phase 8 weeks ago.
Just a quick idea of mine: Could it be worthwhile to decouple the releases of the logic from the releases of the system-/user interaction? That is, have Isabelle-yyyy-x and Isabelle/Tools-yyyy-x.z with the invariant that for every z Isabelle-yyyy-x and Isabelle/Tools-yyyy-x.z work well together. Then changes like 'missing dialog in Isabelle/jEdit' and 'better termination of stray processes' are easier to push and are in another category than 'new datatype system'. Again: This is just a quick idea, and I have no insight into how feasible the differentiation is, especially on the very low levels. - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
