[isabelle-dev] status (AFP)

[Gerwin Klein]

The problem seems to be HyperCTL. From the log:

Run out of store - interrupting threads
Failed to recover - exiting
/tmp/isabelle-isatest/isabelle_script3270098471353362986: line 8: /mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/timestop.bash: No such file or directory
HyperCTL FAILED
[..]
Running Launchbury ...
*** I/O error: Cannot run program "/mnt/nfsbroy/home/isatest/afp/isadist/Isabelle_04-May-2014/lib/scripts/process" (in directory "/home/isatest/afp/devel/thys/Launchbury"): error=2, No such file or directory


It looks like the test for HyperCTL is running so long before it fails that half the execution environment has disappeared (possibly because it is being deleted for the test on the next day).

I have added a time out to the session now so the other ones at least get a chance to run. We should introduce a more systematic check that all AFP sessions have a time out set.

Cheers,
Gerwin


On 05.05.2014, at 7:49 pm, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> Am 05.05.2014 um 11:17 schrieb Johannes Hölzl <hoelzl at in.tum.de>:
>
>> Has anybody an idea why the AFP test for Probabilistic_Noninterference
>> fails?
>>
>> When I build it on my machine
>
> Same on my machine, and same for Selection_Heap_Sort, Native_Word, and Launchbury: All work fine on my machine.
>
> (HyperCTL has been broken since it has been introduced. We need Andrei to look at it.)
>
> Jasmin
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

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.