Re: [isabelle-dev] NEWS -> Redundant lemmas
Hi Johannes,
>> 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.
Thanks a lot.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
Hi Johannes, > I tried to reduce the runtime requirement of HOL-Probability by removing > some of the sublocale instantiations. As a lot of time is spend in > locale interpretation inside proofs. Is the same interpretation repeated over and over? In that case the corresponding proposition can be factored out into a lemma which is then reused over and over. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ 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
Re: [isabelle-dev] NEWS -> Redundant lemmas
On Thu, 22 Sep 2011, 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. 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. This would be the basic plan, but it also needs to be wired up with the Prover IDE protocol and stylesheets (which are still only half finished). The part about the name space is relatively easy, but the "annotation" part in the source text requires some further thoughts. Concerning the extra text, the attitude in PIDE is to point to the original source for additional information. There could be a semi-formal comment telling the user, maybe as simple as the existing "-- cmt" form. (Some people in Edinburgh have proposed "social tagging" :-) Anyway, I am the one who is responsible for these parts of the system. It is old wisdom in Isabelle develoment (with its 25 years) that it is more efficient to consult the experts and main responsable persons for each particular component, instead of tinkering oneself. (The latter has occasionally happened, either leading to code in terminal condition that nobody undertstands anymore, or forcing some poor fellow to re-engineer it from the ground up. For the name space module both has happened in variations several times already.) 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 09/22/2011 09:00 PM, Lawrence Paulson wrote: 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. But people will have to edit their theories anyway, for other reasons (changed commands, changed theory names, changed tool behaviour/setup, disappearing or reappearing type constructors :-) ). So this was not meant as a means for upwards compatibility, but rather of supporting the upgrade process. But you are probably right that it is more work than it is worth, at least at the current state of infrastructure. Completely different idea: An automated way of checking which theorems have disappeared from important places (e.g., HOL image) from one Isabelle version to the next, such that we don't forget them in the NEWS. This should be straightforward to script. 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, Sep 22, 2011 at 11:34 AM, Alexander Krauss wrote: > 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... This is a good point. There is only one benefit I can see for having a legacy phase for renamed theorems: This enables users to make theory files that are simultaneously compatible with two Isabelle releases. But this is probably not a big deal. 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). - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS -> Redundant lemmas
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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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 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, Sep 22, 2011 at 6:10 AM, Makarius 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
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On Tue, 20 Sep 2011, Makarius wrote: In the meantime I have investigated this a little bit. It seems that HOL-Probability requires quite some memory even in minimalistic batch mode -- approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB for the editor process and the same (and more) for the fully persistent document state within ML. So it adds up to something > 4 GB such that it becomes infeasible to edit the full session live on a "small" laptop with "only" 4 GB. I tried to reduce the runtime requirement of HOL-Probability by removing some of the sublocale instantiations. As a lot of time is spend in locale interpretation inside proofs. For example currently I had: locale A = ... locale B = A + ... (0) locale C = A + th sublocale C < B I assume replacing (0) by: locale C = B + th lemma [Pure.intros!]: "C <-> A /\ th" should fasten up locale interpretation? But how is it in the following case: locale prodA = A M1 + A M2 (1) locale prodB = B M1 + B M2 sublocale prodB < prodA locale prodC = C M1 + C M2 sublocale prodC < prodB locale prodD = D M1 + D M2 sublocale prodD < prodA Or should this be: (2) locale prodB = prodA + B M1 + B M2 locale prodC = prodB + C M1 + C M2 locale prodD = prodC + D M1 + D M2 as a user the difference should not be visible, and I thought (1) would be slower than (2) but after updating Probability it seams like (2) is slower than (1). - 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
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 Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban 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
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 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
>> 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
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
