[isabelle-dev] [isabelle] new quick check expriment
Lukas Bulwahn
bulwahn at in.tum.de
Mon Jun 18 09:13:20 CEST 2012
On 06/17/2012 06:36 PM, Florian Haftmann wrote:
>> 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
> Maybe we have to find a way to provide ghc as a component also…
Although Haskell is an essential part for Quickcheck in Isabelle and it
would simplify the installation process for Quickcheck, I am not in
favour to provide ghc contributed with the Isabelle distribution.
So GHC must be installed by the usual means of the operating system,
e.g., through some package manager.
Providing GHC as a component might try to help to install GHC on the
operating system, or could try to detect the path of GHC automagically,
but I do not have a clear vision how this should work.
Lukas
More information about the isabelle-dev
mailing list