[isabelle-dev] AFP devel broken

Makarius makarius at sketis.net
Thu Dec 6 12:57:49 CET 2012


On Thu, 6 Dec 2012, Tobias Nipkow wrote:

>> Since no log file gets produced and no information comes out of tty 
>> mode, it's not even clear to me which stage exactly hangs. It's 
>> entirely possible that it's just hanging trying to load the parent 
>> image, for instance. It doesn't seem to have anything to do with the 
>> content of the theories.
>
> As far as I can see, the poly process always hangs after just a few 
> secs, but there is still a java process which keeps running and uses 
> small amounts of time, like some kind of busy wait.

The Poly/ML process doing nothing useful could be a deadlock in its 
multithreading.  The Java process is part of the build management, and 
oversees several processes, polling every 0.5 seconds.  Problems with ML 
and Scala/JVM have happened before and were resolved.  Also note that Java 
7 on Mac OS X is still not 100% right, but Java 6 already in its N-th 
extension of the end-of-live.


The issues on this thread first came up some weeks ago, when I was on 
vacation.  In the meantime I've run several tests myself, but failed to 
reproduce the problem.  Last time even as "isatest" on macbroy2 with 
exactly the same settings as one of the reported hangs.

This does not say anything yet.  We need to collect further details and 
hypotheses and test them.  I will also try again to reproduce it myself.


 	Makarius



More information about the isabelle-dev mailing list