Re: [isabelle-dev] NEWS - Redundant lemmas
I think this is a good idea. Larry On 22 Sep 2011, at 03:08, Brian Huffman 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? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
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? 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.) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
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). 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. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban urb...@in.tum.de wrote:
I was able to put together replacement theorems for a few of these lemmas:
Inf_singleton ~ Inf_insert [where A={}, unfolded Inf_empty inf_top_right]
Sup_singleton ~ Sup_insert [where A={}, unfolded Sup_empty sup_bot_right]
INTER_eq_Inter_image ~ INF_def
UNION_eq_Union_image ~ SUP_def
INF_subset ~ INF_superset_mono [OF _ order_refl]
[..]
I added this information to the NEWS entry.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
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.) I think theory developers are happy with maintaining the annotations. Some theories in the distribution already contain a Legacy section (just grep for Legacy in the *.thy files), adding a deprecation flag would simplify the maintainance of this and allow us to remove them in a couple of releases. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
On Thu, Sep 22, 2011 at 6:10 AM, Makarius makar...@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 ___
Re: [isabelle-dev] NEWS - Redundant lemmas
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
Re: [isabelle-dev] NEWS - Redundant lemmas
On Thu, 22 Sep 2011, Brian Huffman wrote: Anyway, if we are decided that the legacy phase for renamed/generalized theorems is not useful, then there is no point in preserving the legacy theorems sections in the libraries, is there? We might as well go ahead and start removing all of these right now (documenting the removals in the NEWS file, of course). My observation is that the (informal) legacy phase for the theory libraries is a bit longer than for the ML code base, but that is not a big deal. The cycle for marking things (as done normally in Isabelle/ML) is do add the legacy hints *before* a release, and do the purge *after* a release. (Big cleanup is general best done in the 2-4 months after a liftoff -- it gives a second chance to detect the flaws in the reasoning about legacy status in the first place.) Anyway, for this release I think we are getting close to convergence pretty soon. So only the really important things should be finished now. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
