[isabelle-dev] NEWS -> Redundant lemmas

[Lawrence Paulson]

I think we are taking this idea too far.

The original suggestion was simply to move deprecated theorem bindings into a separate file, where they could be loaded if necessary to save people the trouble of having to edit their theories. We could generalise the idea of a little so that other deleted material could be moved into a legacy area. But no more than that. I don't think it's practical or appropriate to implement any sort of sophisticated mechanisms for ensuring upwards compatibility. People who have a big project and need to keep an eye on this can always download development snapshots from time to time. We could also warn users of big changes using the mailing list.

Larry

On 22 Sep 2011, at 19:34, Alexander Krauss wrote:

> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev