[isabelle-dev] NEWS -> Redundant lemmas

[Makarius]

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