[isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)



Dear Jeremy,

All the worries you describe are definitely serious problems, and most
people on this list have probably experienced this in one or the other
way. Different releases of Isabelle are hardly compatible on the ML
level and even the theory level requires a fair amount of changes from
one release to the next. This is especially true for the transition
2005->2007, due to the many accumulated changes.

These issues seem to be capable of causing massive and unnecessary difficulties.

However, I cannot agree that these difficulties were unnecessary. How
could they be avoided? Not making any incompatible changes to Isabelle
anymore would essentially stop history and carve the current state of
the art into stone.

The alternative - maintaining various compatibility layers that
implement all interfaces and functionality present in some old versions
- demands a large amount of resources which we surely don't have. And it
scales badly: Legacy code accumulates over time and leads to a linear
(or worse) increase in maintenance costs, but development resources are
(probably) constant. Companies with lots of money may be able to support
this, but even then the results are not always satisfactory (think of
the compatibility problems between different versions of Microsoft
Office files).

So the only realistic chance is that users keep up with the development
and update their theories. Sticking to some old version may seem
convenient for some time but, as you describe, it locks you into a
closed world, where you cannot use other people's work and do not profit
from new developments. Updating your theories is an investment that pays
off finally. I agree that the 2005->2007 transition is undesirably
painful but we are trying to make releases frequent enough to avoid this
in the future. 2007->2008 is in fact not such a big deal (even with the
somewhat radical removal of sets as a separate type).

Embrace change!

Alex


PS.  Anyway, what aspects of the documentation are actually tested?

The (old) Isabelle Reference Manual and the various "Logics" descriptions are still plain latex documents and hence cannot be tested. Everything else is generated from theories.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.