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 _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
