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> 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 > listhol-info@lists.sourceforge.nethttps://lists.sourceforge.net/lists/listinfo/hol-info > > > > > _______________________________________________ > hol-info mailing list > 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
