On 29/11/2012, at 11:47 PM, Christian Sternagel <[email protected]> wrote:
> On 11/09/2012 12:26 AM, Christian Sternagel wrote: >> Just follow the "Browse theories" link of any devel entry, e.g., >> http://afp.sourceforge.net/browser_info/devel/HOL/Bondy/index.html > As far as I can tell the problem still remains. Is it known in the meantime > what the problem is? Not really. It now overlaps less with isatest, but the log still mostly ends in the middle of HOL-Probability (e.g. see below). It appears those processes all just get stuck and sit there. I've moved the afp test 2h later to eliminate any overlap with isatest, but that's probably not it. I have some more ideas what to look at, but was away last week and at SSV'12 this week. Next week is looking better for progress on this. Cheers, Gerwin Start test for /home/isatest/afp/devel at Thu Nov 29 06:30:56 CET 2012, macbroy2 begin hg pull/update pulling from ssh://[email protected]/hgroot/afp/afp searching for changes adding changesets adding manifests adding file changes added 2 changesets with 42 changes to 42 files 42 files updated, 0 files merged, 0 files removed, 0 files unresolved remote: Running preoutgoing hook remote: Use of uninitialized value in concatenation (.) or string at /etc/mercurial/preoutgoing line 36. end hg pull/update AFP version: development -- hg id 40ecbad14077 Isabelle version: devel -- hg id 902ccccf2efa Building HOLCF ... Finished HOLCF (0:00:43 elapsed time, 0:01:10 cpu time, factor 1.62) Building HOL-Nominal ... Finished HOL-Nominal (0:00:15 elapsed time, 0:00:25 cpu time, factor 1.66) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:02:21 elapsed time, 0:06:46 cpu time, factor 2.87) Building HOL-Word ... Finished HOL-Word (0:00:33 elapsed time, 0:01:16 cpu time, factor 2.30) Building Jinja ... Finished Jinja (0:04:44 elapsed time, 0:14:27 cpu time, factor 3.05) Building LatticeProperties ... Finished LatticeProperties (0:00:16 elapsed time, 0:00:24 cpu time, factor 1.50) Building HOL-Probability ... ________________________________ 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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
