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 packages.
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...
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
