Email Gateway (Aug 18 2022 at 20:26): Email Gateway (Aug 18 2022 at 20:26):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
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
Email Gateway (Aug 18 2022 at 20:26):From: Tobias Nipkow <nipkow@in.tum.de>
This works:
quickcheck[narrowing]
Admittedly, it would be nice if that option were not necessary.
Tobias
Email Gateway (Aug 18 2022 at 20:26):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Hi,
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
Yuhui
Email Gateway (Aug 18 2022 at 20:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,
Now it gives me another error message "Compilation with GHC failed". Any suggestion ?
first, you need a Glasgow Haskell Compiler installed (don't know which
version, but if you are working on a system which a package management
system, try the one recommend by it first).
Then adjust your settings (the global ones or the user-specific ones in
~/.isabelle/etc/settings) to point ISABELLE_GHC to the appropriate
location of ghc.
Hope this helps,
Florian
signature.asc
Last updated: May 06 2024 at 12:29 UTC