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.lochbih...@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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
