As Thomas said, you are probably encountering this use of temporary files for the first time. In particular, I suppose you may not have tried to cut and paste large regions of your script file in the past. You could confirm that this is the problem by seeing if smaller regions of text do transfer to the HOL session successfully.
You might also edit the hol-mode file to change the constant on line 803 from 500 to something larger. It’s possible the need for this limit has entirely disappeared, but SML sessions within emacs-comint buffers have in the past failed to consume large inputs all at once. Michael From: Yassmeen Derhalli <derhal...@gmail.com> Date: Friday, 21 September 2018 at 08:11 To: Thomas Tuerk <tho...@tuerk-brechen.de> Cc: "hol-info@lists.sourceforge.net" <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] Exception raised while using HOL in hol-mode Hi, thank you for your reply. I am using an oracle virtual machine on my laptop running ubuntu-16.04.4-desktop-i386. I have been using this machine for about three months now, and I have not had any problem until yesterday. Best Regards, Yassmeen On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk <tho...@tuerk-brechen.de<mailto:tho...@tuerk-brechen.de>> wrote: Hi, I believe this is due to how hol-mode copies input from emacs buffers to HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff. (https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800). If a chunk of text you want to send exceeds a certain size, it is written to a temp-file instead and "use tempfile" is send to HOL. I fear this is going wrong for some reason. hol-mode tries to write the chunk of text to the file "/tmp/hol2207zVM" and then sends "use "/tmp/hol2207zVM" to HOL. However, for some reason HOL cannot find this file. This results in the error message you posted. How to fix it is a good question. I have seen this error before when working remotely with HOL. When using HOL via ssh or in some virtual environment like a docker container, I had the problem before that the communication with HOL worked just fine, but HOL and emacs saw different "/tmp" directories (e.g. the ones on the local and remote machine). Are you using anything like this? What environment are you running HOL in? Best Thomas On 20.09.2018 17:40, Yassmeen Derhalli wrote: Hi, Sorry for sending this email again, but it seems that there was a problem with the first email I am using HOL4, yesterday I started receiving this error message Exception raised Io {cause = SysErr ("No such file or directory", SOME ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"} I am using HOL4 in the hol-mode, but when I use HOL directly using the shell, my script runs fine, this only happens in the hol-mode, any clue why this could happen and how can I fix it? thanks _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
