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.
Andreas
On 19/07/14 21:30, Gerwin Klein
Right. Then something in the ISABELLE_GHC mechanism does not work, it’s
definitely set to the right path.
Cheers,
Gerwin
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
Just had a very strange experience with ISABELLE_GHC.
You will have noticed that the AFP test failed the last few days with GHC
compilation errors.
The AFP test settings included the line
ISABELLE_GHC=/opt/local/bin/ghc
Apparently, this caused sessions like Native_Word to fail, even though
