Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of Library/Quickcheck_Types. Andreas On 18/08/14 18:44, Peter Lammich wrote: However, the constructions might still be useful, as the following comment from Peter Lammich's AFP entry Refine_Monadic shows. (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides an isomorphic contruction. *) At this point I duplicated the flat complete lattice construction locally, as I did not want to use rely on a construction from such a special and unrelated thing as quickcheck. So, should we keep Quickcheck_Types (maybe under a different name, say Lattice_Constructions) or drop it? I think, at least the standard constructions, like flat complete lattice, should be preserved and either directly go into Complete_Lattice or, as you proposed, into HOL/Library/Lattice_Constructions. -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
On 15/08/2014 09:30, Andreas Lochbihler wrote: In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected, this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126). This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within the Isabelle distribution and the AFP, this theory is no longer used anywhere. I expect that almost nobody relies on the quickcheck setup in there. From the quickcheck point of view, we can therefore drop this theory. Anyone who needs it can keep their own local copy. However, the constructions might still be useful, as the following comment from Peter Lammich's AFP entry Refine_Monadic shows. (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides an isomorphic contruction. *) Peter, does that mean you could replace your specific construction by something in Quickcheck_Types.thy? In that case I would recomment to keep Quickcheck_Types.thy (or some part of it) alive, maybe under a less specific name, and Peter uses it in his AFP entry. Tobias So, should we keep Quickcheck_Types (maybe under a different name, say Lattice_Constructions) or drop it? Andreas On 11/07/14 15:54, Andreas Lochbihler wrote: Quickcheck does not use these types, because it is currently configures to only use the types finite_1 to finite_3 from Enum, because the finite_types parameter is set by default. Quickcheck internally also seems to work differently depending on whether the finite_types flag is set. I have only little insight how the parameters affect the performance of quickcheck, but I remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is from that time. However, int is an infinite type and therefore, quantifiers, set comprehensions and function equality are not executable. Later, he switched to the finite_X types, which instantiate enum, but not the other type classes. Therefore, I recommend the following: 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library. Then, anyone who wants to use quickcheck with infinite types can do so. This way, the Quickcheck_Examples session can also be reactivated. 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types instances of the lattice type class hierarchy. Probably most of the stuff in Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the test cases in Quickcheck_Lattice_Examples work with the Enum types, too. I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for step 2 before the fork of the release branch. Andreas On 11/07/14 14:28, Tobias Nipkow wrote: On 11/07/2014 13:43, Andreas Lochbihler wrote: Quickcheck_Types defines a number of artificial types that quickcheck can use to instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them with int provided that the sort constraints do not prevent this. In Enum.thy, there are already the types finite_X that quickcheck uses for enumerable types (type class enum) such that quantifiers can be unfolded into conjunctions or disjunctions. The types in Quickcheck_Types now do the same for the lattices type class hierarchy, because int and the finite_X types cannot be used for type variables with sort lattice (or top/bot/...). I believe that it should be fairly simple to adjust Quickcheck_Types to Isabelle2014. However, this only makes sense if it becomes part of Main. Otherwise, it will remain just a library theory that hardly anyone knows about and no one uses. Moreover, we should make sure that Quickcheck_Types fits to the current code generator setup for lattices. IIRC, Florian has reworked a lot there over the past years. At the very least, we should have some test cases (e.g. in HOL/ex) to check that Quickcheck_Types works as expected. If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. It looks mildly useful. But then Qickcheck would need to use it, which it currently obviously does not. If you (or somebody) is able to make that happen, then I am in favour of reviving that theory. Tobias Andreas On 11/07/14 13:22, Lawrence Paulson wrote: I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it.
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected, this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126). This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within the Isabelle distribution and the AFP, this theory is no longer used anywhere. I expect that almost nobody relies on the quickcheck setup in there. From the quickcheck point of view, we can therefore drop this theory. Anyone who needs it can keep their own local copy. However, the constructions might still be useful, as the following comment from Peter Lammich's AFP entry Refine_Monadic shows. (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides an isomorphic contruction. *) So, should we keep Quickcheck_Types (maybe under a different name, say Lattice_Constructions) or drop it? Andreas On 11/07/14 15:54, Andreas Lochbihler wrote: Quickcheck does not use these types, because it is currently configures to only use the types finite_1 to finite_3 from Enum, because the finite_types parameter is set by default. Quickcheck internally also seems to work differently depending on whether the finite_types flag is set. I have only little insight how the parameters affect the performance of quickcheck, but I remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is from that time. However, int is an infinite type and therefore, quantifiers, set comprehensions and function equality are not executable. Later, he switched to the finite_X types, which instantiate enum, but not the other type classes. Therefore, I recommend the following: 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library. Then, anyone who wants to use quickcheck with infinite types can do so. This way, the Quickcheck_Examples session can also be reactivated. 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types instances of the lattice type class hierarchy. Probably most of the stuff in Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the test cases in Quickcheck_Lattice_Examples work with the Enum types, too. I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for step 2 before the fork of the release branch. Andreas On 11/07/14 14:28, Tobias Nipkow wrote: On 11/07/2014 13:43, Andreas Lochbihler wrote: Quickcheck_Types defines a number of artificial types that quickcheck can use to instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them with int provided that the sort constraints do not prevent this. In Enum.thy, there are already the types finite_X that quickcheck uses for enumerable types (type class enum) such that quantifiers can be unfolded into conjunctions or disjunctions. The types in Quickcheck_Types now do the same for the lattices type class hierarchy, because int and the finite_X types cannot be used for type variables with sort lattice (or top/bot/...). I believe that it should be fairly simple to adjust Quickcheck_Types to Isabelle2014. However, this only makes sense if it becomes part of Main. Otherwise, it will remain just a library theory that hardly anyone knows about and no one uses. Moreover, we should make sure that Quickcheck_Types fits to the current code generator setup for lattices. IIRC, Florian has reworked a lot there over the past years. At the very least, we should have some test cases (e.g. in HOL/ex) to check that Quickcheck_Types works as expected. If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. It looks mildly useful. But then Qickcheck would need to use it, which it currently obviously does not. If you (or somebody) is able to make that happen, then I am in favour of reviving that theory. Tobias Andreas On 11/07/14 13:22, Lawrence Paulson wrote: I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it. ___ 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 ___ isabelle-dev mailing list
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
On Fri, 11 Jul 2014, Andreas Lochbihler wrote: If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. I can't say anything myself how it would impact the bootstrap of Main HOL. As long as this question does not arise for the Isabelle2014 release, I would say: go ahead and renovate it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Quickcheck does not use these types, because it is currently configures to only use the types finite_1 to finite_3 from Enum, because the finite_types parameter is set by default. Quickcheck internally also seems to work differently depending on whether the finite_types flag is set. I have only little insight how the parameters affect the performance of quickcheck, but I remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is from that time. However, int is an infinite type and therefore, quantifiers, set comprehensions and function equality are not executable. Later, he switched to the finite_X types, which instantiate enum, but not the other type classes. Therefore, I recommend the following: 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library. Then, anyone who wants to use quickcheck with infinite types can do so. This way, the Quickcheck_Examples session can also be reactivated. 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types instances of the lattice type class hierarchy. Probably most of the stuff in Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the test cases in Quickcheck_Lattice_Examples work with the Enum types, too. I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for step 2 before the fork of the release branch. Andreas On 11/07/14 14:28, Tobias Nipkow wrote: On 11/07/2014 13:43, Andreas Lochbihler wrote: Quickcheck_Types defines a number of artificial types that quickcheck can use to instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them with int provided that the sort constraints do not prevent this. In Enum.thy, there are already the types finite_X that quickcheck uses for enumerable types (type class enum) such that quantifiers can be unfolded into conjunctions or disjunctions. The types in Quickcheck_Types now do the same for the lattices type class hierarchy, because int and the finite_X types cannot be used for type variables with sort lattice (or top/bot/...). I believe that it should be fairly simple to adjust Quickcheck_Types to Isabelle2014. However, this only makes sense if it becomes part of Main. Otherwise, it will remain just a library theory that hardly anyone knows about and no one uses. Moreover, we should make sure that Quickcheck_Types fits to the current code generator setup for lattices. IIRC, Florian has reworked a lot there over the past years. At the very least, we should have some test cases (e.g. in HOL/ex) to check that Quickcheck_Types works as expected. If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. It looks mildly useful. But then Qickcheck would need to use it, which it currently obviously does not. If you (or somebody) is able to make that happen, then I am in favour of reviving that theory. Tobias Andreas On 11/07/14 13:22, Lawrence Paulson wrote: I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it. ___ 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 ___ 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] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Te discussion has faded out here a few months ago. Again, shall we attempt a serious repair effort? Florian -- 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
