On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
"Legacy.thy" that would not be imported by default, and would be
cleared out after each release. When upgrading Isabelle, users could
import Legacy.thy as needed to get their theories working, and then
work gradually to eliminate the dependencies on it. What do you think?
If one tries to follow Brian's idea, even with the Legacy.thy, there is still
no guarantees that by importing the theory, everything works as with the
release before.
For some incompatible changes, retaining compatibility within another theory
is larger than the change itself.
But for the special case of phasing out legacy theorems, it might work, but
then I would only restrict this Legacy theory to selected theories (maybe
everything within HOL-Plain or even less).
This is an old problem, and we have some partial solutions to it that are
reasonably established in Isabelle/ML at the least.
It is generally hard to assemble all legacy stuff in a single central
"Legacy" module (or theory), because legacy stuff also needs to observe
certain dependencies. In ML structure Misc_Legacy is close to that idea
of central collection point, but it is only used maybe for 30% of the hard
legacy stuff from Isabelle/Pure. Apart from that, naming conventions like
"legacy_foo" and the well-known legacy warnings are used to make clear
what is the situation.
For theory content we occasionally have "Old_Foo" entries for larger
modules. For smaller collection it was up to the discretion of the
maintainer what to do, and this is probably the case here. So the people
behind this lattice modernization effort should have a feeling if it is
worth to introduce some HOL/Library/Old_Lattices.thy or similar.
In Java, there is a "deprecated" flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the "legacy"-warnings
it already issues when using some deprecated features (recdef, etc.)
You are assuming that you could flag theorems, and all tools know what these
flags should actually mean, and if they use them.
That's technically quite difficult to achieve.
In principle we have similar flags for name space entries already, e.g.
"concealed". Having an official legacy status (also in the Proper IDE) is
probably easy to implement, but the main work is maintaining the actual
annotations in the libraries. My impression is that the traditional
approach is to clear out old material quickly, so that the issue only
arises in a weak sense. (In contrast, the Java standard library is famous
for being strictly monotonic, where deprecated stuff is never disposed.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
