makarius at sketis.net
Mon Jul 21 13:21:01 CEST 2014
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:
date: Sun Jul 20 22:05:35 2014 +0200
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.
More information about the isabelle-dev