[isabelle-dev] ISABELLE_GHC/quickcheck

[Gerwin Klein]

Hi Florian,

On 20 Jul 2014, at 7:18 am, Florian Haftmann <florian.haftmann at 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.