[isabelle-dev] ISABELLE_GHC/quickcheck

[Makarius]

On Mon, 21 Jul 2014, Gerwin Klein wrote:

> Right. Then something in the ISABELLE_GHC mechanism does not work, it’s 
> definitely set to the right path.
>
> On 21 Jul 2014, at 8:40 am, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>
>> The Native_Word entry in the AFP contains a number of 
>> quickcheck[narrowing] calls that are set up such that they are tested 
>> only if ISABELLE_GHC is set. Therefore, there cannot be an error 
>> message about quickcheck narrowing if ISABELLE_GHC is not set.

There is indeed something odd here, not to say non-canonical.


In order to make isatest work as before there is already this changeset:

changeset:   57584:155b7e3b729e
user:        wenzelm
date:        Sun Jul 20 22:05:35 2014 +0200
files:       src/HOL/ROOT
description:
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);


The [condition = ISABELLE_GHC] was already there before, but with a 
different scope of theories.  I did not know that ISABELLE_GHC is checked 
dynamically by the tool.


Generally, since GHC is not an official Isabelle component, many odd 
things can happen depending on the local system installation. I do not 
understand myself how GHC works, and if it is feasible to make its status 
more official.  It would probably require a bit more than the usual care 
to maintain such an Isabelle component on all platforms.


 	Makarius