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