Dear All,
I am using polyml to run hol.
From within emacs, I normally use "C-c C-r" to send a region to the
hol process. This involves emacs writing out to a tmp file, and the hol process attempting to "use" the file back in.
After a lot of proof, I get the following error:
"Unable to allocate immutable area"
which occurs in the "use" command. Immediately after the above error, I get the following two lines: eg
Failed to translate file: /tmp/sml26128UHN Exception- Fail "use" raised
The result is that I can no longer use "C-c C-r" to send a file (nor, presumably, "use" any other file).
I can still cut and paste into the hol process buffer.
What does the error mean? Can I do anything to improve things?
Thanks
Tom
I noticed my memory was mostly used.
I invoked PolyML.fullGC(), which freed 3 G (out of 6 total). Unfortunately my hol was no longer in a usable state (some top level bindings seemed to have been lost).
However, on restarting, all now seems well.
In future, I will watch my memory usage, and call fullGC() when it is almost all used.
Thanks
Tom
2008/11/17 Tom Ridge thomas.ridge@cl.cam.ac.uk:
Dear All,
I am using polyml to run hol.
From within emacs, I normally use "C-c C-r" to send a region to the hol process. This involves emacs writing out to a tmp file, and the hol process attempting to "use" the file back in.
After a lot of proof, I get the following error:
"Unable to allocate immutable area"
which occurs in the "use" command. Immediately after the above error, I get the following two lines: eg
Failed to translate file: /tmp/sml26128UHN Exception- Fail "use" raised
The result is that I can no longer use "C-c C-r" to send a file (nor, presumably, "use" any other file).
I can still cut and paste into the hol process buffer.
What does the error mean? Can I do anything to improve things?
Thanks
Tom
Tom Ridge wrote:
I am using polyml to run hol.
From within emacs, I normally use "C-c C-r" to send a region to the
hol process. This involves emacs writing out to a tmp file, and the hol process attempting to "use" the file back in.
After a lot of proof, I get the following error:
"Unable to allocate immutable area"
which occurs in the "use" command. Immediately after the above error, I get the following two lines: eg
Failed to translate file: /tmp/sml26128UHN Exception- Fail "use" raised
The result is that I can no longer use "C-c C-r" to send a file (nor, presumably, "use" any other file).
I can still cut and paste into the hol process buffer.
What does the error mean? Can I do anything to improve things?
When Poly/ML starts up it makes a request to the operating system for memory to allocate its heap. The size of the request is related to the value of the '-H' option. If the request fails it produces this message and exits. The usual cause of this is running out of swap space so it's quite possible that simply re-running the command will work depending on what else is running on the machine at the same time. Closing down unnecessary processes will definitely help.
David
-
David.Matthews＠prolingua.co.uk -
thomas.ridge＠cl.cam.ac.uk