[isabelle-dev] ISABELLE_GHC/quickcheck

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Jul 20 07:18:36 CEST 2014

Hi Gerwin,

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.

My suspicion is that some libraries cannot be found due to missing
environment settings (the classical cronjob problem).  How exactly does
the error look like?



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140720/9ae88283/attachment.sig>

More information about the isabelle-dev mailing list