[isabelle-dev] HOL-Predicate_Compile_Examples

[Andreas Lochbihler]

Hi Makarius,

I had a brief look at the unchecked files in Predice_Compile_Examples. I have never worked 
with these theories, so take my comments with a grain of salt.

Predicate_Compile_Quickcheck_Examples:

In dc2236b19a3d, Lukas removed the testers which are used in this theory and replaced them 
with smart_exhaustive. Moreover, this theory stems from the time when 'a set was a synonym 
for 'a => bool. The predicate compiler was never adjusted to the separation of predicates 
and sets in Isabelle2012 and can only handle predicates.

I replaced the old generators with the new testers and the examples which do not involve 
sets work again. Those with sets are completely broken.

Hotel_Example_Small_Generator:

The examples in this file involve sets, so I have no hope to get this working without 
addressing the problem with sets.


IMP_3 and IMP_4: These two theories also fail due to sets. However, sets are only used 
with the function List.set, so this can be easily avoided.


I've committed some changes in 78ece168f5b5 such that most of the examples work again. 
Only Hotel_Example_Small_Generator remains completely broken.

Unfortunately, quickcheck and the predicate compiler have been essentially unmaintained 
since Lukas has left. The predicate compiler works fine for inductive predicates, but most 
of the extensions that Lukas has implemented (in particular inductify) have not been 
maintained are therefore break in many cases. Similarly, Quickcheck internally has a huge 
number of compilation modes most of which I consider as untested. The above changeset 
activates a few tests again, but as can be seen, the compliation modes break in corner 
cases. Ideally, we'd need a thorough clean-up of quickcheck and the predicate compiler, 
but I guess nobody is willing to invest the time.

Cheers,
Andreas


On 09/09/15 11:37, Makarius wrote:
> Doing some routine maintenance, I've rediscovered this very odd changeset:
>
> changeset:   40055:1f7cc5357d96
> user:        bulwahn
> date:        Thu Oct 21 20:26:35 2010 +0200
> files:       src/HOL/Predicate_Compile_Examples/ROOT.ML
> description:
> temporary removed Predicate_Compile_Quickcheck_Examples from tests
>
> The comment in the source says "should be added again soon", but that was 5 years ago.
>
>
> The session HOL-Predicate_Compile_Examples has a few more dead and half-rotten bits, see
> http://isabelle.in.tum.de/repos/isabelle/file/f9fd43d8981d/src/HOL/ROOT#l973
>
> Any ideas what can be done about it?  Even just removing rubbish requires some basic
> understanding of the situation.
>
>
>      Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev