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 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 wrote: >> 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 that >> is where ghc is installed on this machine (macbroy2). ghc also happens to be >> in the PATH on macbroy2 (pointing to the same /opt/local/bin/ghc), so in an >> act of desperation I tried locally removing the above line on the isatest >> account. Voila, Native_Word builds fine. >> >> This was on isabelle 2bfbeb0e69cd and afp 4ea6558c319c. >> >> However: on my laptop, with ISABELLE_GHC=/usr/bin/ghc, everything works >> fine. Either it’s something about the path or something about the macbroyX >> machines. >> >> Any ideas what could be going on? >> >> Cheers, >> Gerwin >> >> >> ________________________________ >> >> The information in this e-mail may be confidential and subject to legal >> professional privilege and/or copyright. National ICT Australia Limited >> accepts no liability for any damage caused by this email or its attachments. >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
