[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
andreas.lochbihler at inf.ethz.ch
Fri Jul 11 15:54:44 CEST 2014
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.
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