[isabelle-dev] AFP devel broken

Gerwin Klein Gerwin.Klein at nicta.com.au
Fri Nov 30 04:04:39 CET 2012

On 29/11/2012, at 11:47 PM, Christian Sternagel <c-sterna at jaist.ac.jp> 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.


Start test for /home/isatest/afp/devel at Thu Nov 29 06:30:56 CET 2012, macbroy2

begin hg pull/update
pulling from ssh://isatest@afp.hg.sourceforge.net/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.

More information about the isabelle-dev mailing list