[isabelle-dev] AFP devel broken
krauss at in.tum.de
Thu Dec 6 00:58:57 CET 2012
On 12/05/2012 10:50 PM, Gerwin Klein wrote:
> I am unsure how to proceed debugging these hangs. I will try some
> other machines and see if it is correlated with MacOS X or if it is
> something else.
> 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.
Recently I noticed strange effects when trying to read larger files from
NFS (larger meaning 1-2 GB). My situation was different. The reading was
from within an Isabelle session (using basically File.fold_lines), which
would eventually (and predictably) fail at some point during the
processing with an exception going back to a "bad file descriptor" from
This happened both on lxbroy7 and lxbroy10, and it went away when I
copied the file to the local file system and read it from there.
I don't know what this is, but I could imagine something strange
happening when the same occurs while polyml is loading an image. This is
just guessing though.
The fact that mira builds still work also suggests NFS issues: the mira
workbench sits under /tmp, which is local.
Could one think about moving isatests $ISABELLE_HOME_USER to a local disk?
More information about the isabelle-dev