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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
