Re: [isabelle-dev] ISABELLE_GHC/quickcheck
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
Re: [isabelle-dev] ISABELLE_GHC/quickcheck
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
[isabelle-dev] ISABELLE_GHC/quickcheck
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
