[isabelle-dev] AFP devel broken

Alexander Krauss 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 
the OS.

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?

Alex





More information about the isabelle-dev mailing list