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
> 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
