Hi Alex, I think it's possible that this could be as a result of the storage management changes but to do with a different part of it. If it's what I think it is then the changes needed will be quite small. Perhaps the easiest way to do this would be to discuss this off-list. I can send you some patches to try and it may be simpler to do that than for you to try to cut the problem down further.
Best regards, David
On 21/01/2013 23:33, Alexander Krauss wrote:
Dear list,
In an Isabelle session that reads a large file containing a proof trace, I am regularly getting a funny low-level filehandle error when using polyml 5.5.0:
*** exception Io {name = "/home/krauss/src/nimport/HOL_VOL/proofsN-VOL", cause = SysErr ("Bad file descriptor", SOME EBADF), function = "TextIO.fillBuffer"} raised (line 476 of "./basis/TextIO.sml")
I am doing nothing low-level with filehandles, just reading a file using basis library APIs (wrapped by Isabelle).
It does not happen completely reliably but quite often, and seems to be correlated with low-memory situations. If I restrict the memory drastically using --maxheap, then it always happens. But it also sometimes happens when (I think) enough memory should be available.
My suspicion is that this could be an issue with the new memory management, but this is just guessing.
This happens across various linuxes. I am seeing it with polyml 5.5.0 but not with 5.4.1. It happens both on 32bit and 64bit. I can exclude things like NFS, since I also see it on regular ext3 volumes.
My questions:
- Can any of the new memory management features be switched off (e.g.,
the sharing phase)? Are there other flags I could play with to narrow this issue down further?
- Any other ideas?
I can provide source code to reproduce this, but it is not quite minimal at the moment...
Thanks for any help Alex _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml