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-...@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
