Re: [isabelle] new quick check expriment


Thanks. It asks me to set  'Environment variable ISABELLE_GHC '. So I uncomment the line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc'

Now it gives me another error message "Compilation with GHC failed". Any suggestion ?

PS, I work in a mac version of Isabelle 2012


On 17 Jun 2012, at 09:23, Tobias Nipkow wrote:

> This works:
> quickcheck[narrowing]
> Admittedly, it would be nice if that option were not necessary.
> Tobias
> Am 17/06/2012 02:20, schrieb Yuhui Lin:
>> HI all,
>> I'm playing the Isabelle 2012 to test the enhanced quickcheck. According to the paper "The New Quickcheck for Isabelle", quick check should be able to find a counter example for the lemma "xs = rev xs ==> EX ys. xs = ys @ rev ys". I failed to get this result, but an error message complaining about 
>> "*** Wellsortedness error:
>> *** Type Enum.finite_1 list not of sort enum
>> *** No type arity list :: enum
>> Do I miss any config to enable the narrowing-based testing ? How can I get the counter example with narrowing-based testing? Thanks.
>> Best,
>> Yuhui

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.