[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