[isabelle-dev] NEWS -> Redundant lemmas
krauss at in.tum.de
Thu Sep 22 20:34:00 CEST 2011
On 09/22/2011 05:00 PM, Brian Huffman wrote:
> 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
Well... taking this seriously would mean to do this not only for facts
but for all sorts of name space entries. Packages would then have to
make sure that the legacy flag is propagated, e.g., from a constant to
its characteristic theorems (unless otherwise indicated by the user, I
suppose). This is the same as for the "concealed" flag, which is still
not handled uniformly throughout the system. Like with conceal, one
would want to make sure that legacy stuff does not show up in search, or
is not otherwise suggested to users by the system, e.g. via
sledgehammer. There is in fact quite a bit of similarity with "concealed".
If one has both "legacy" and "concealed", and possibly more once we get
serious about modular namespaces (e.g., "private" to limit visibility to
some scope), it might be worth trying to generalize those to some sort
of general namespace annotation concept...
>> My impression is that the traditional
>> approach is to clear out old material quickly, so that the issue only arises
>> in a weak sense.
For mere renamings or simple generalizations, we should just go ahead,
making sure that the conversion table is in the NEWS. Having an extra
legacy phase here only creates extra work with no benefit for anyone.
With a new release, people usually have to upgrade their theories
anyway, so a few search/replace items can piggy-back on that work easily
and postponing them is no better.
The longer legacy process should be only for things that are not as
trivial for users to replace...
More information about the isabelle-dev