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.blanche...@gmail.com> wrote: > Am 05.05.2014 um 11:17 schrieb Johannes Hölzl <hoe...@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-...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
