Hi Florian, On 20 Jul 2014, at 7:18 am, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote: > On 19.07.2014 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? > > Btw. I personally prefer something like > > ISABELLE_GHC="$(type -p ghc)" > ISABELLE_OCAML="$(type -p ocaml)" > ISABELLE_SWIPL="$(type -p swipl)" > > for all those external those, in order not to have to much to think > about different locations.
Not a bad idea, but works only when the program is in the path, which ghc didn’t use to be (now is, though). > My suspicion is that some libraries cannot be found due to missing > environment settings (the classical cronjob problem). I could reproduce the error by logging into the isatest account and running isabelle build from the command line. With the settings in ~/afp/isadist/Isabelle/ it failed, with the standard settings of ~/hg-isabelle/ it worked. When I left out the ISABELLE_GHC line in ~/afp/isadist/Isabelle/ it worked there as well. We’ll see today if it works from cron also. > How exactly does the error look like? Part of the problem is that we don’t get a real error message: Native_Word FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.2_x86-darwin/log/Native_Word) *** Compilation with GHC failed *** At command "quickcheck" (line 725 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Native_Word/Uint32.thy") (repeated for different quickcheck commands) 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