[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
nipkow at in.tum.de
Fri Jul 11 18:27:05 CEST 2014
On 11/07/2014 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.
Thank you for that.
> 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,
> 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.
> 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.
>>> On 11/07/14 13:22, Lawrence Paulson wrote:
>>>> I’m afraid that I don’t even know what it is.
>>>> On 11 Jul 2014, at 12:21, Florian Haftmann
>>>> <florian.haftmann at 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-dev at in.tum.de
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
More information about the isabelle-dev