[isabelle-dev] ISABELLE_GHC/quickcheck

Gerwin Klein Gerwin.Klein at nicta.com.au
Sat Jul 19 21:30:37 CEST 2014

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

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?



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.

More information about the isabelle-dev mailing list