[isabelle-dev] NEWS -> Redundant lemmas

[Brian Huffman]

On Thu, Sep 22, 2011 at 6:10 AM, Makarius <makarius at sketis.net> wrote:
> 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.

Yes, there are definitely some limitations with the Legacy.thy idea,
particularly the issue of dependencies: We obviously can't put the
legacy theorems from HOL-Plain, HOL, HOLCF, HOL-Multivariate_Analysis,
etc. all in the same place. I thought it might be useful just because
it would be trivial to implement.


>>> 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.

I actually like Peter's idea of a "deprecated" flag better than my
Legacy.thy idea. We might implement it by adding a new "deprecated"
flag to each entry in the "naming" type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
identically to non-deprecated names, except that looking up a
deprecated name would cause a legacy warning message to be printed. I
don't think it would be necessary to modify any other tools or
packages.

Of course, we'd also need to invent some interface for marking names
as deprecated in the first place. It might also be nice to associate a
text string to each deprecated name (perhaps saying what other
name/feature to use instead) instead of just using a boolean flag.


> 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.

Several theories in Isabelle/HOL have "legacy theorem" sections, so in
some sense we are already maintaining some annotations. I guess the
motivation for marking theorems as "legacy" (instead of deleting them
immediately) is to make it easier for users to adapt to their removal:
Deleting a theorem that has already been marked as "legacy" for a
release or two should be less disruptive than just deleting a theorem
suddenly. The problem is that this is currently not true! Users have
no indication (unless they read the sources) of whether they are using
a legacy theorem name. So right now, it seems like the "legacy
theorem" annotations are only useful as "TODO" comments to the other
developers, saying "someone ought to delete these, eventually".

> 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.)

I don't think that anyone intends theorems marked as "legacy" to stay
around forever. Perhaps we should start a tradition of keeping legacy
theorems for one release only, completely purging all "legacy"
theorems from the libraries shortly after each release. If we
implemented a legacy-theorem warning message, then one release would
still be enough time to make the transition easier for users. (And
without a legacy-theorem warning, keeping legacy theorems around
longer before eventually removing them doesn't make things any easier,
so there should be no reason to wait longer than one release.)

- Brian