[isabelle-dev] AFP devel broken

[Gerwin Klein]

On 06/12/2012, at 10:58 AM, Alexander Krauss <krauss at in.tum.de> wrote:

> 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 seems to be slightly different to the hangs observed on the AFP test. The poly process will happily sit there for days doing nothing, never producing an error message (that I can see at least).


> 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.

It's my best guess at the moment as well.

It can't just be NFS, though, if Tobias is experiencing the same problem on his laptop.


> 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?

At least for the AFP test that should be relatively easy to do, I've re-written large parts last year to make it more independent of the rest of isatest anyway. 

I'll try running it on /tmp for a while and see if that at changes some of the behaviour.

Cheers,
Gerwin